The rewrite relation of the following TRS is considered.
| 0(5(0(x1))) | → | 3(4(3(3(2(0(4(4(4(0(x1)))))))))) | (1) |
| 0(2(5(0(x1)))) | → | 0(2(1(1(5(2(1(4(1(3(x1)))))))))) | (2) |
| 0(5(0(5(x1)))) | → | 3(2(0(2(0(4(4(1(5(4(x1)))))))))) | (3) |
| 2(5(5(3(x1)))) | → | 4(3(0(2(1(0(1(3(4(3(x1)))))))))) | (4) |
| 5(5(5(0(x1)))) | → | 4(1(2(1(2(3(5(0(1(3(x1)))))))))) | (5) |
| 0(5(1(5(0(x1))))) | → | 3(4(0(1(4(5(2(2(3(1(x1)))))))))) | (6) |
| 3(0(0(5(3(x1))))) | → | 1(3(4(3(5(2(4(1(3(3(x1)))))))))) | (7) |
| 3(5(5(0(0(x1))))) | → | 1(4(1(0(0(4(4(0(4(1(x1)))))))))) | (8) |
| 0(2(5(1(5(0(x1)))))) | → | 2(1(0(1(5(2(4(0(2(0(x1)))))))))) | (9) |
| 0(2(5(5(1(4(x1)))))) | → | 4(0(1(1(1(1(0(4(1(5(x1)))))))))) | (10) |
| 0(5(3(1(2(5(x1)))))) | → | 0(2(3(1(1(2(4(4(5(5(x1)))))))))) | (11) |
| 0(5(5(1(5(1(x1)))))) | → | 0(5(1(1(3(3(4(2(1(0(x1)))))))))) | (12) |
| 4(5(5(4(2(0(x1)))))) | → | 2(4(0(1(3(4(4(4(1(0(x1)))))))))) | (13) |
| 5(0(0(3(5(2(x1)))))) | → | 4(4(2(3(0(1(2(0(5(2(x1)))))))))) | (14) |
| 5(1(5(0(2(5(x1)))))) | → | 5(0(0(1(4(2(3(2(1(5(x1)))))))))) | (15) |
| 5(2(0(2(5(5(x1)))))) | → | 5(5(4(4(4(5(4(4(1(4(x1)))))))))) | (16) |
| 5(5(0(2(5(0(x1)))))) | → | 2(0(5(0(2(1(0(0(3(0(x1)))))))))) | (17) |
| 5(5(0(3(4(5(x1)))))) | → | 2(0(5(5(2(1(3(2(3(2(x1)))))))))) | (18) |
| 5(5(3(5(0(5(x1)))))) | → | 5(4(4(3(5(1(3(3(4(5(x1)))))))))) | (19) |
| 0(4(4(0(0(5(1(x1))))))) | → | 1(3(2(0(4(1(5(1(1(2(x1)))))))))) | (20) |
| 0(4(4(2(5(5(5(x1))))))) | → | 0(2(4(5(5(4(2(0(1(1(x1)))))))))) | (21) |
| 1(0(2(5(2(0(0(x1))))))) | → | 3(1(4(4(0(3(0(1(2(2(x1)))))))))) | (22) |
| 1(2(0(4(2(5(0(x1))))))) | → | 4(2(4(0(3(2(2(4(1(0(x1)))))))))) | (23) |
| 1(2(5(5(0(3(3(x1))))))) | → | 3(4(1(2(0(3(3(1(0(3(x1)))))))))) | (24) |
| 1(5(5(3(3(3(4(x1))))))) | → | 1(5(1(0(0(2(2(2(3(5(x1)))))))))) | (25) |
| 2(5(4(5(2(5(1(x1))))))) | → | 4(3(2(1(4(2(2(4(5(2(x1)))))))))) | (26) |
| 3(2(3(5(1(5(2(x1))))))) | → | 2(0(3(2(3(2(1(5(5(1(x1)))))))))) | (27) |
| 3(3(4(2(5(5(2(x1))))))) | → | 1(2(3(3(4(4(1(4(0(1(x1)))))))))) | (28) |
| 3(5(0(5(5(5(0(x1))))))) | → | 0(0(3(0(3(5(0(3(2(0(x1)))))))))) | (29) |
| 4(3(1(2(5(2(4(x1))))))) | → | 2(3(1(1(4(3(4(4(2(4(x1)))))))))) | (30) |
| 4(5(5(3(1(0(5(x1))))))) | → | 1(1(5(2(0(3(3(3(2(1(x1)))))))))) | (31) |
| 5(0(5(3(1(0(5(x1))))))) | → | 5(2(4(4(2(1(3(5(1(5(x1)))))))))) | (32) |
| 5(0(5(3(5(1(5(x1))))))) | → | 5(1(1(2(4(0(0(3(2(5(x1)))))))))) | (33) |
| 5(1(5(3(3(0(5(x1))))))) | → | 4(4(3(2(2(2(5(0(1(1(x1)))))))))) | (34) |
| 5(2(0(2(5(3(3(x1))))))) | → | 5(2(0(5(1(1(3(2(0(3(x1)))))))))) | (35) |
| 0(5(0(x1))) | → | 0(4(4(4(0(2(3(3(4(3(x1)))))))))) | (36) |
| 0(5(2(0(x1)))) | → | 3(1(4(1(2(5(1(1(2(0(x1)))))))))) | (37) |
| 5(0(5(0(x1)))) | → | 4(5(1(4(4(0(2(0(2(3(x1)))))))))) | (38) |
| 3(5(5(2(x1)))) | → | 3(4(3(1(0(1(2(0(3(4(x1)))))))))) | (39) |
| 0(5(5(5(x1)))) | → | 3(1(0(5(3(2(1(2(1(4(x1)))))))))) | (40) |
| 0(5(1(5(0(x1))))) | → | 1(3(2(2(5(4(1(0(4(3(x1)))))))))) | (41) |
| 3(5(0(0(3(x1))))) | → | 3(3(1(4(2(5(3(4(3(1(x1)))))))))) | (42) |
| 0(0(5(5(3(x1))))) | → | 1(4(0(4(4(0(0(1(4(1(x1)))))))))) | (43) |
| 0(5(1(5(2(0(x1)))))) | → | 0(2(0(4(2(5(1(0(1(2(x1)))))))))) | (44) |
| 4(1(5(5(2(0(x1)))))) | → | 5(1(4(0(1(1(1(1(0(4(x1)))))))))) | (45) |
| 5(2(1(3(5(0(x1)))))) | → | 5(5(4(4(2(1(1(3(2(0(x1)))))))))) | (46) |
| 1(5(1(5(5(0(x1)))))) | → | 0(1(2(4(3(3(1(1(5(0(x1)))))))))) | (47) |
| 0(2(4(5(5(4(x1)))))) | → | 0(1(4(4(4(3(1(0(4(2(x1)))))))))) | (48) |
| 2(5(3(0(0(5(x1)))))) | → | 2(5(0(2(1(0(3(2(4(4(x1)))))))))) | (49) |
| 5(2(0(5(1(5(x1)))))) | → | 5(1(2(3(2(4(1(0(0(5(x1)))))))))) | (50) |
| 5(5(2(0(2(5(x1)))))) | → | 4(1(4(4(5(4(4(4(5(5(x1)))))))))) | (51) |
| 0(5(2(0(5(5(x1)))))) | → | 0(3(0(0(1(2(0(5(0(2(x1)))))))))) | (52) |
| 5(4(3(0(5(5(x1)))))) | → | 2(3(2(3(1(2(5(5(0(2(x1)))))))))) | (53) |
| 5(0(5(3(5(5(x1)))))) | → | 5(4(3(3(1(5(3(4(4(5(x1)))))))))) | (54) |
| 1(5(0(0(4(4(0(x1))))))) | → | 2(1(1(5(1(4(0(2(3(1(x1)))))))))) | (55) |
| 5(5(5(2(4(4(0(x1))))))) | → | 1(1(0(2(4(5(5(4(2(0(x1)))))))))) | (56) |
| 0(0(2(5(2(0(1(x1))))))) | → | 2(2(1(0(3(0(4(4(1(3(x1)))))))))) | (57) |
| 0(5(2(4(0(2(1(x1))))))) | → | 0(1(4(2(2(3(0(4(2(4(x1)))))))))) | (58) |
| 3(3(0(5(5(2(1(x1))))))) | → | 3(0(1(3(3(0(2(1(4(3(x1)))))))))) | (59) |
| 4(3(3(3(5(5(1(x1))))))) | → | 5(3(2(2(2(0(0(1(5(1(x1)))))))))) | (60) |
| 1(5(2(5(4(5(2(x1))))))) | → | 2(5(4(2(2(4(1(2(3(4(x1)))))))))) | (61) |
| 2(5(1(5(3(2(3(x1))))))) | → | 1(5(5(1(2(3(2(3(0(2(x1)))))))))) | (62) |
| 2(5(5(2(4(3(3(x1))))))) | → | 1(0(4(1(4(4(3(3(2(1(x1)))))))))) | (63) |
| 0(5(5(5(0(5(3(x1))))))) | → | 0(2(3(0(5(3(0(3(0(0(x1)))))))))) | (64) |
| 4(2(5(2(1(3(4(x1))))))) | → | 4(2(4(4(3(4(1(1(3(2(x1)))))))))) | (65) |
| 5(0(1(3(5(5(4(x1))))))) | → | 1(2(3(3(3(0(2(5(1(1(x1)))))))))) | (66) |
| 5(0(1(3(5(0(5(x1))))))) | → | 5(1(5(3(1(2(4(4(2(5(x1)))))))))) | (67) |
| 5(1(5(3(5(0(5(x1))))))) | → | 5(2(3(0(0(4(2(1(1(5(x1)))))))))) | (68) |
| 5(0(3(3(5(1(5(x1))))))) | → | 1(1(0(5(2(2(2(3(4(4(x1)))))))))) | (69) |
| 3(3(5(2(0(2(5(x1))))))) | → | 3(0(2(3(1(1(5(0(2(5(x1)))))))))) | (70) |
| [0(x1)] | = | 1 · x1 |
| [5(x1)] | = | 1 · x1 + 1 |
| [4(x1)] | = | 1 · x1 |
| [2(x1)] | = | 1 · x1 |
| [3(x1)] | = | 1 · x1 |
| [1(x1)] | = | 1 · x1 |
| 0(5(0(x1))) | → | 0(4(4(4(0(2(3(3(4(3(x1)))))))))) | (36) |
| 5(0(5(0(x1)))) | → | 4(5(1(4(4(0(2(0(2(3(x1)))))))))) | (38) |
| 3(5(5(2(x1)))) | → | 3(4(3(1(0(1(2(0(3(4(x1)))))))))) | (39) |
| 0(5(5(5(x1)))) | → | 3(1(0(5(3(2(1(2(1(4(x1)))))))))) | (40) |
| 0(5(1(5(0(x1))))) | → | 1(3(2(2(5(4(1(0(4(3(x1)))))))))) | (41) |
| 0(0(5(5(3(x1))))) | → | 1(4(0(4(4(0(0(1(4(1(x1)))))))))) | (43) |
| 0(5(1(5(2(0(x1)))))) | → | 0(2(0(4(2(5(1(0(1(2(x1)))))))))) | (44) |
| 4(1(5(5(2(0(x1)))))) | → | 5(1(4(0(1(1(1(1(0(4(x1)))))))))) | (45) |
| 1(5(1(5(5(0(x1)))))) | → | 0(1(2(4(3(3(1(1(5(0(x1)))))))))) | (47) |
| 0(2(4(5(5(4(x1)))))) | → | 0(1(4(4(4(3(1(0(4(2(x1)))))))))) | (48) |
| 2(5(3(0(0(5(x1)))))) | → | 2(5(0(2(1(0(3(2(4(4(x1)))))))))) | (49) |
| 5(2(0(5(1(5(x1)))))) | → | 5(1(2(3(2(4(1(0(0(5(x1)))))))))) | (50) |
| 0(5(2(0(5(5(x1)))))) | → | 0(3(0(0(1(2(0(5(0(2(x1)))))))))) | (52) |
| 5(4(3(0(5(5(x1)))))) | → | 2(3(2(3(1(2(5(5(0(2(x1)))))))))) | (53) |
| 5(0(5(3(5(5(x1)))))) | → | 5(4(3(3(1(5(3(4(4(5(x1)))))))))) | (54) |
| 5(5(5(2(4(4(0(x1))))))) | → | 1(1(0(2(4(5(5(4(2(0(x1)))))))))) | (56) |
| 0(0(2(5(2(0(1(x1))))))) | → | 2(2(1(0(3(0(4(4(1(3(x1)))))))))) | (57) |
| 0(5(2(4(0(2(1(x1))))))) | → | 0(1(4(2(2(3(0(4(2(4(x1)))))))))) | (58) |
| 3(3(0(5(5(2(1(x1))))))) | → | 3(0(1(3(3(0(2(1(4(3(x1)))))))))) | (59) |
| 1(5(2(5(4(5(2(x1))))))) | → | 2(5(4(2(2(4(1(2(3(4(x1)))))))))) | (61) |
| 2(5(5(2(4(3(3(x1))))))) | → | 1(0(4(1(4(4(3(3(2(1(x1)))))))))) | (63) |
| 0(5(5(5(0(5(3(x1))))))) | → | 0(2(3(0(5(3(0(3(0(0(x1)))))))))) | (64) |
| 4(2(5(2(1(3(4(x1))))))) | → | 4(2(4(4(3(4(1(1(3(2(x1)))))))))) | (65) |
| 5(0(1(3(5(5(4(x1))))))) | → | 1(2(3(3(3(0(2(5(1(1(x1)))))))))) | (66) |
| 5(1(5(3(5(0(5(x1))))))) | → | 5(2(3(0(0(4(2(1(1(5(x1)))))))))) | (68) |
| 5(0(3(3(5(1(5(x1))))))) | → | 1(1(0(5(2(2(2(3(4(4(x1)))))))))) | (69) |
| 0#(5(2(0(x1)))) | → | 3#(1(4(1(2(5(1(1(2(0(x1)))))))))) | (71) |
| 0#(5(2(0(x1)))) | → | 1#(4(1(2(5(1(1(2(0(x1))))))))) | (72) |
| 0#(5(2(0(x1)))) | → | 4#(1(2(5(1(1(2(0(x1)))))))) | (73) |
| 0#(5(2(0(x1)))) | → | 1#(2(5(1(1(2(0(x1))))))) | (74) |
| 0#(5(2(0(x1)))) | → | 2#(5(1(1(2(0(x1)))))) | (75) |
| 0#(5(2(0(x1)))) | → | 5#(1(1(2(0(x1))))) | (76) |
| 0#(5(2(0(x1)))) | → | 1#(1(2(0(x1)))) | (77) |
| 0#(5(2(0(x1)))) | → | 1#(2(0(x1))) | (78) |
| 3#(5(0(0(3(x1))))) | → | 3#(3(1(4(2(5(3(4(3(1(x1)))))))))) | (79) |
| 3#(5(0(0(3(x1))))) | → | 3#(1(4(2(5(3(4(3(1(x1))))))))) | (80) |
| 3#(5(0(0(3(x1))))) | → | 1#(4(2(5(3(4(3(1(x1)))))))) | (81) |
| 3#(5(0(0(3(x1))))) | → | 4#(2(5(3(4(3(1(x1))))))) | (82) |
| 3#(5(0(0(3(x1))))) | → | 2#(5(3(4(3(1(x1)))))) | (83) |
| 3#(5(0(0(3(x1))))) | → | 5#(3(4(3(1(x1))))) | (84) |
| 3#(5(0(0(3(x1))))) | → | 3#(4(3(1(x1)))) | (85) |
| 3#(5(0(0(3(x1))))) | → | 4#(3(1(x1))) | (86) |
| 3#(5(0(0(3(x1))))) | → | 3#(1(x1)) | (87) |
| 3#(5(0(0(3(x1))))) | → | 1#(x1) | (88) |
| 5#(2(1(3(5(0(x1)))))) | → | 5#(5(4(4(2(1(1(3(2(0(x1)))))))))) | (89) |
| 5#(2(1(3(5(0(x1)))))) | → | 5#(4(4(2(1(1(3(2(0(x1))))))))) | (90) |
| 5#(2(1(3(5(0(x1)))))) | → | 4#(4(2(1(1(3(2(0(x1)))))))) | (91) |
| 5#(2(1(3(5(0(x1)))))) | → | 4#(2(1(1(3(2(0(x1))))))) | (92) |
| 5#(2(1(3(5(0(x1)))))) | → | 2#(1(1(3(2(0(x1)))))) | (93) |
| 5#(2(1(3(5(0(x1)))))) | → | 1#(1(3(2(0(x1))))) | (94) |
| 5#(2(1(3(5(0(x1)))))) | → | 1#(3(2(0(x1)))) | (95) |
| 5#(2(1(3(5(0(x1)))))) | → | 3#(2(0(x1))) | (96) |
| 5#(2(1(3(5(0(x1)))))) | → | 2#(0(x1)) | (97) |
| 5#(5(2(0(2(5(x1)))))) | → | 4#(1(4(4(5(4(4(4(5(5(x1)))))))))) | (98) |
| 5#(5(2(0(2(5(x1)))))) | → | 1#(4(4(5(4(4(4(5(5(x1))))))))) | (99) |
| 5#(5(2(0(2(5(x1)))))) | → | 4#(4(5(4(4(4(5(5(x1)))))))) | (100) |
| 5#(5(2(0(2(5(x1)))))) | → | 4#(5(4(4(4(5(5(x1))))))) | (101) |
| 5#(5(2(0(2(5(x1)))))) | → | 5#(4(4(4(5(5(x1)))))) | (102) |
| 5#(5(2(0(2(5(x1)))))) | → | 4#(4(4(5(5(x1))))) | (103) |
| 5#(5(2(0(2(5(x1)))))) | → | 4#(4(5(5(x1)))) | (104) |
| 5#(5(2(0(2(5(x1)))))) | → | 4#(5(5(x1))) | (105) |
| 5#(5(2(0(2(5(x1)))))) | → | 5#(5(x1)) | (106) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 2#(1(1(5(1(4(0(2(3(1(x1)))))))))) | (107) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 1#(1(5(1(4(0(2(3(1(x1))))))))) | (108) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 1#(5(1(4(0(2(3(1(x1)))))))) | (109) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 5#(1(4(0(2(3(1(x1))))))) | (110) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 1#(4(0(2(3(1(x1)))))) | (111) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 4#(0(2(3(1(x1))))) | (112) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 0#(2(3(1(x1)))) | (113) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 2#(3(1(x1))) | (114) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 3#(1(x1)) | (115) |
| 1#(5(0(0(4(4(0(x1))))))) | → | 1#(x1) | (116) |
| 4#(3(3(3(5(5(1(x1))))))) | → | 5#(3(2(2(2(0(0(1(5(1(x1)))))))))) | (117) |
| 4#(3(3(3(5(5(1(x1))))))) | → | 3#(2(2(2(0(0(1(5(1(x1))))))))) | (118) |
| 4#(3(3(3(5(5(1(x1))))))) | → | 2#(2(2(0(0(1(5(1(x1)))))))) | (119) |
| 4#(3(3(3(5(5(1(x1))))))) | → | 2#(2(0(0(1(5(1(x1))))))) | (120) |
| 4#(3(3(3(5(5(1(x1))))))) | → | 2#(0(0(1(5(1(x1)))))) | (121) |
| 4#(3(3(3(5(5(1(x1))))))) | → | 0#(0(1(5(1(x1))))) | (122) |
| 4#(3(3(3(5(5(1(x1))))))) | → | 0#(1(5(1(x1)))) | (123) |
| 4#(3(3(3(5(5(1(x1))))))) | → | 1#(5(1(x1))) | (124) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 1#(5(5(1(2(3(2(3(0(2(x1)))))))))) | (125) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 5#(5(1(2(3(2(3(0(2(x1))))))))) | (126) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 5#(1(2(3(2(3(0(2(x1)))))))) | (127) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 1#(2(3(2(3(0(2(x1))))))) | (128) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(3(2(3(0(2(x1)))))) | (129) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 3#(2(3(0(2(x1))))) | (130) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(3(0(2(x1)))) | (131) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 3#(0(2(x1))) | (132) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 0#(2(x1)) | (133) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(x1) | (134) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 5#(1(5(3(1(2(4(4(2(5(x1)))))))))) | (135) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 1#(5(3(1(2(4(4(2(5(x1))))))))) | (136) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 5#(3(1(2(4(4(2(5(x1)))))))) | (137) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 3#(1(2(4(4(2(5(x1))))))) | (138) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 1#(2(4(4(2(5(x1)))))) | (139) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 2#(4(4(2(5(x1))))) | (140) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 4#(4(2(5(x1)))) | (141) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 4#(2(5(x1))) | (142) |
| 5#(0(1(3(5(0(5(x1))))))) | → | 2#(5(x1)) | (143) |
| 3#(3(5(2(0(2(5(x1))))))) | → | 3#(0(2(3(1(1(5(0(2(5(x1)))))))))) | (144) |
| 3#(3(5(2(0(2(5(x1))))))) | → | 0#(2(3(1(1(5(0(2(5(x1))))))))) | (145) |
| 3#(3(5(2(0(2(5(x1))))))) | → | 2#(3(1(1(5(0(2(5(x1)))))))) | (146) |
| 3#(3(5(2(0(2(5(x1))))))) | → | 3#(1(1(5(0(2(5(x1))))))) | (147) |
| 3#(3(5(2(0(2(5(x1))))))) | → | 1#(1(5(0(2(5(x1)))))) | (148) |
| 3#(3(5(2(0(2(5(x1))))))) | → | 1#(5(0(2(5(x1))))) | (149) |
| 3#(3(5(2(0(2(5(x1))))))) | → | 5#(0(2(5(x1)))) | (150) |
The dependency pairs are split into 3 components.
| 5#(5(2(0(2(5(x1)))))) | → | 5#(5(x1)) | (106) |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| 5#(5(2(0(2(5(x1)))))) | → | 5#(5(x1)) | (106) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| 1#(5(0(0(4(4(0(x1))))))) | → | 1#(x1) | (116) |
| [5(x1)] | = | 1 · x1 |
| [0(x1)] | = | 1 · x1 |
| [4(x1)] | = | 1 · x1 |
| [1#(x1)] | = | 1 · x1 |
Using size-change termination in combination with the subterm criterion one obtains the following initial size-change graphs.
| 1#(5(0(0(4(4(0(x1))))))) | → | 1#(x1) | (116) |
| 1 | > | 1 |
As there is no critical graph in the transitive closure, there are no infinite chains.
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(3(0(2(x1)))) | (131) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(3(2(3(0(2(x1)))))) | (129) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(x1) | (134) |
| [2#(x1)] | = | 1 · x1 |
| [5(x1)] | = | 1 + 1 · x1 |
| [1(x1)] | = | 1 · x1 |
| [3(x1)] | = | 1 · x1 |
| [2(x1)] | = | 1 · x1 |
| [0(x1)] | = | 1 · x1 |
| [4(x1)] | = | 1 · x1 |
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(3(0(2(x1)))) | (131) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(3(2(3(0(2(x1)))))) | (129) |
| 2#(5(1(5(3(2(3(x1))))))) | → | 2#(x1) | (134) |
There are no pairs anymore.