459 |
459 |
460 definition |
460 definition |
461 "rec_read = CN rec_ldec [Id 1 0, constn 0]" |
461 "rec_read = CN rec_ldec [Id 1 0, constn 0]" |
462 |
462 |
463 definition |
463 definition |
464 "rec_write = CN rec_penc [S, CN rec_pdec2 [Id 2 1]]" |
464 "rec_write = CN rec_penc [CN S [Id 2 0], CN rec_pdec2 [Id 2 1]]" |
465 |
465 |
466 definition |
466 definition |
467 "rec_newleft = |
467 "rec_newleft = |
468 (let cond0 = CN rec_eq [Id 3 2, constn 0] in |
468 (let cond0 = CN rec_eq [Id 3 2, constn 0] in |
469 let cond1 = CN rec_eq [Id 3 2, constn 1] in |
469 let cond1 = CN rec_eq [Id 3 2, constn 1] in |
528 let newleft = CN rec_newleft [left, right, action] in |
528 let newleft = CN rec_newleft [left, right, action] in |
529 let newright = CN rec_newright [left, right, action] |
529 let newright = CN rec_newright [left, right, action] |
530 in CN rec_conf [newstate, newleft, newright])" |
530 in CN rec_conf [newstate, newleft, newright])" |
531 |
531 |
532 definition |
532 definition |
533 "rec_steps = PR (Id 3 0) (CN rec_step [Id 4 1, Id 4 3])" |
533 "rec_steps = PR (Id 2 0) (CN rec_step [Id 4 1, Id 4 3])" |
534 |
534 |
535 definition |
535 definition |
536 "rec_stknum = CN rec_minus |
536 "rec_stknum = CN rec_minus |
537 [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0], |
537 [CN (rec_sigma1 (CN rec_ldec [Id 2 1, Id 2 0])) [CN rec_enclen [Id 1 0], Id 1 0], |
538 CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]" |
538 CN rec_ldec [Id 1 0, CN rec_enclen [Id 1 0]]]" |
539 |
539 |
540 definition |
540 definition |
541 "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in |
541 "rec_right_std = (let bound = CN rec_enclen [Id 1 0] in |
542 let cond1 = CN rec_le [constn 1, Id 2 0] in |
542 let cond1 = CN rec_le [CN (constn 1) [Id 2 0], Id 2 0] in |
543 let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in |
543 let cond2 = rec_all1_less (CN rec_eq [CN rec_ldec [Id 2 1, Id 2 0], constn 1]) in |
544 let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in |
544 let bound2 = CN rec_minus [CN rec_enclen [Id 2 1], Id 2 0] in |
545 let cond3 = CN (rec_all2_less |
545 let cond3 = CN (rec_all2_less |
546 (CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z])) |
546 (CN rec_eq [CN rec_ldec [Id 3 2, CN rec_add [Id 3 1, Id 3 0]], Z])) |
547 [bound2, Id 2 0, Id 2 1] in |
547 [bound2, Id 2 0, Id 2 1] in |