The rewrite relation of the following TRS is considered.
| a(x1) | → | x1 | (1) |
| o(x1) | → | x1 | (2) |
| l(x1) | → | x1 | (3) |
| S(x1) | → | x1 | (4) |
| +(x1,x2) | → | x2 | (5) |
| +(x1,x2) | → | x1 | (6) |
| P(x1,x2,x3) | → | x3 | (7) |
| P(x1,x2,x3) | → | x2 | (8) |
| P(x1,x2,x3) | → | x1 | (9) |
| M(x1,x2,x3) | → | x3 | (10) |
| M(x1,x2,x3) | → | x2 | (11) |
| M(x1,x2,x3) | → | x1 | (12) |
| J1(x1,x2) | → | x2 | (13) |
| J1(x1,x2) | → | x1 | (14) |
| J2(x1,x2,x3) | → | x3 | (15) |
| J2(x1,x2,x3) | → | x2 | (16) |
| J2(x1,x2,x3) | → | x1 | (17) |
| Q11(x1,x2) | → | x2 | (18) |
| Q11(x1,x2) | → | x1 | (19) |
| Q21(x1,x2,x3) | → | x3 | (20) |
| Q21(x1,x2,x3) | → | x2 | (21) |
| Q21(x1,x2,x3) | → | x1 | (22) |
| Q22(x1,x2,x3) | → | x3 | (23) |
| Q22(x1,x2,x3) | → | x2 | (24) |
| Q22(x1,x2,x3) | → | x1 | (25) |
| R1(x1,x2,x3) | → | x3 | (26) |
| R1(x1,x2,x3) | → | x2 | (27) |
| R1(x1,x2,x3) | → | x1 | (28) |
| R2(x1,x2,x3,x4) | → | x4 | (29) |
| R2(x1,x2,x3,x4) | → | x3 | (30) |
| R2(x1,x2,x3,x4) | → | x2 | (31) |
| R2(x1,x2,x3,x4) | → | x1 | (32) |
| P(0,0,0) | → | S(0) | (33) |
| +(x,S(y)) | → | S(+(x,y)) | (34) |
| a(l(x)) | → | l(a(a(x))) | (35) |
| l(o(x)) | → | o(l(l(x))) | (36) |
| o(x) | → | l(x) | (37) |
| l(x) | → | a(x) | (38) |
| a(S(x)) | → | S(l(x)) | (39) |
| a(+(x,y)) | → | +(l(x),y) | (40) |
| a(+(x,y)) | → | +(x,l(y)) | (41) |
| a(P(x1,x2,x3)) | → | P(x1,x2,l(x3)) | (42) |
| a(P(x1,x2,x3)) | → | P(x1,l(x2),x3) | (43) |
| a(P(x1,x2,x3)) | → | P(l(x1),x2,x3) | (44) |
| +(x,o(y)) | → | o(+(x,y)) | (45) |
| P(x1,x2,o(x3)) | → | o(P(x1,x2,x3)) | (46) |
| P(x1,o(x2),x3) | → | o(P(x1,x2,x3)) | (47) |
| P(o(x1),x2,x3) | → | o(P(x1,x2,x3)) | (48) |
| M(x1,x2,l(y)) | → | +(M(x1,x2,y),P(x1,x2,y)) | (49) |
| J2(x1,l(x2),y) | → | P(x1,J2(x1,x2,y),0) | (50) |
| J1(l(x1),y) | → | P(J1(x1,y),0,0) | (51) |
| a(S(x)) | → | o(x) | (52) |
| P(0,0,S(y)) | → | o(M(0,0,y)) | (53) |
| P(0,0,P(x1,x2,y)) | → | o(M(x1,x2,y)) | (54) |
| P(x1,S(x2),y) | → | o(J2(x1,x2,y)) | (55) |
| P(S(x1),0,y) | → | o(J1(x1,y)) | (56) |
| P(x1,S(x2),S(y)) | → | o(J2(x1,x2,P(x1,S(x2),y))) | (57) |
| P(S(x1),0,S(y)) | → | o(J1(x1,P(S(x1),0,y))) | (58) |
| a(P(x1,x2,0)) | → | Q22(x1,a(x2),x2) | (59) |
| a(P(x1,x2,0)) | → | Q21(x1,a(x2),x1) | (60) |
| a(P(x1,0,0)) | → | Q11(a(x1),x1) | (61) |
| Q22(x1,o(x2),y) | → | o(P(x1,x2,y)) | (62) |
| Q21(x1,o(x2),y) | → | o(P(x1,x2,y)) | (63) |
| Q11(o(x1),y) | → | o(P(x1,0,y)) | (64) |
| a(P(x1,x2,S(y))) | → | R2(x1,a(x2),x2,y) | (65) |
| a(P(x1,0,S(y))) | → | R1(a(x1),x1,y) | (66) |
| R2(x1,o(x2),y,z) | → | o(P(x1,x2,P(x1,y,z))) | (67) |
| R1(o(x1),y,z) | → | o(P(x1,0,P(y,0,z))) | (68) |
| t0 | = | J2(S(l(x116028)),l(x116028),0) |
| → | P(S(l(x116028)),J2(S(l(x116028)),x116028,0),0) | |
| → | P(S(l(x116028)),S(l(x116028)),0) | |
| → | o(J2(S(l(x116028)),l(x116028),0)) | |
| = | t3 |