The rewrite relation of the following TRS is considered.
0(0(0(x1))) | → | 0(0(1(0(1(x1))))) | (1) |
0(2(0(x1))) | → | 0(0(2(1(1(x1))))) | (2) |
0(3(2(x1))) | → | 2(1(3(0(x1)))) | (3) |
0(4(2(x1))) | → | 4(1(1(1(0(2(x1)))))) | (4) |
3(0(4(x1))) | → | 0(1(3(4(1(x1))))) | (5) |
3(2(0(x1))) | → | 0(2(1(3(x1)))) | (6) |
3(2(0(x1))) | → | 3(0(2(1(x1)))) | (7) |
3(2(0(x1))) | → | 0(1(2(1(3(x1))))) | (8) |
3(2(0(x1))) | → | 3(0(1(2(1(4(x1)))))) | (9) |
3(2(4(x1))) | → | 1(2(1(3(3(4(x1)))))) | (10) |
3(2(4(x1))) | → | 4(1(2(1(1(3(x1)))))) | (11) |
3(2(5(x1))) | → | 1(3(5(2(x1)))) | (12) |
3(2(5(x1))) | → | 3(1(4(5(2(x1))))) | (13) |
3(2(5(x1))) | → | 1(1(3(3(5(2(x1)))))) | (14) |
3(2(5(x1))) | → | 1(3(4(5(4(2(x1)))))) | (15) |
3(5(0(x1))) | → | 3(1(0(5(1(1(x1)))))) | (16) |
5(0(2(x1))) | → | 1(1(0(2(5(x1))))) | (17) |
5(0(4(x1))) | → | 0(5(4(1(1(x1))))) | (18) |
5(2(4(x1))) | → | 5(2(1(1(3(4(x1)))))) | (19) |
5(3(2(x1))) | → | 1(1(3(5(1(2(x1)))))) | (20) |
5(5(0(x1))) | → | 5(1(1(5(0(x1))))) | (21) |
0(0(2(4(x1)))) | → | 0(4(0(2(1(1(x1)))))) | (22) |
0(3(1(2(x1)))) | → | 1(1(3(0(2(x1))))) | (23) |
0(3(2(4(x1)))) | → | 2(1(3(0(4(4(x1)))))) | (24) |
0(4(3(2(x1)))) | → | 2(3(4(0(1(x1))))) | (25) |
3(0(2(4(x1)))) | → | 3(0(4(2(1(1(x1)))))) | (26) |
3(0(5(4(x1)))) | → | 3(4(0(5(1(3(x1)))))) | (27) |
3(1(0(0(x1)))) | → | 0(1(1(3(0(1(x1)))))) | (28) |
3(2(4(0(x1)))) | → | 3(1(0(4(2(x1))))) | (29) |
3(2(4(5(x1)))) | → | 3(1(4(2(1(5(x1)))))) | (30) |
3(2(5(4(x1)))) | → | 3(4(3(5(2(x1))))) | (31) |
3(5(3(2(x1)))) | → | 3(3(0(2(5(x1))))) | (32) |
4(0(4(2(x1)))) | → | 4(4(2(1(3(0(x1)))))) | (33) |
4(3(2(0(x1)))) | → | 0(2(1(3(4(x1))))) | (34) |
5(4(1(0(x1)))) | → | 5(1(1(4(0(1(x1)))))) | (35) |
5(5(0(0(x1)))) | → | 1(1(0(5(5(0(x1)))))) | (36) |
5(5(2(2(x1)))) | → | 5(5(1(1(2(2(x1)))))) | (37) |
0(0(1(2(4(x1))))) | → | 0(0(2(1(1(4(x1)))))) | (38) |
0(5(3(1(2(x1))))) | → | 5(2(1(3(1(0(x1)))))) | (39) |
0(5(5(1(0(x1))))) | → | 5(0(0(5(1(1(x1)))))) | (40) |
3(0(1(4(5(x1))))) | → | 3(4(0(5(1(1(x1)))))) | (41) |
3(0(3(1(2(x1))))) | → | 0(2(1(1(3(3(x1)))))) | (42) |
3(2(2(0(4(x1))))) | → | 3(2(2(0(1(4(x1)))))) | (43) |
3(5(1(4(0(x1))))) | → | 1(3(3(4(5(0(x1)))))) | (44) |
3(5(3(0(4(x1))))) | → | 3(0(1(5(3(4(x1)))))) | (45) |
5(1(0(2(4(x1))))) | → | 2(1(5(4(0(3(x1)))))) | (46) |
5(1(3(2(0(x1))))) | → | 2(3(5(0(1(1(x1)))))) | (47) |
5(4(2(0(2(x1))))) | → | 5(0(4(2(1(2(x1)))))) | (48) |
There are 132 ruless (increase limit for explicit display).
The dependency pairs are split into 1 component.
0#(3(2(x1))) | → | 3#(0(x1)) | (54) |
3#(2(0(x1))) | → | 3#(x1) | (62) |
3#(2(0(x1))) | → | 4#(x1) | (68) |
4#(0(4(2(x1)))) | → | 3#(0(x1)) | (132) |
3#(2(4(x1))) | → | 3#(3(4(x1))) | (69) |
3#(2(4(x1))) | → | 3#(4(x1)) | (70) |
3#(2(4(x1))) | → | 3#(x1) | (72) |
3#(2(5(x1))) | → | 3#(5(2(x1))) | (73) |
3#(2(5(x1))) | → | 5#(2(x1)) | (74) |
5#(2(4(x1))) | → | 3#(4(x1)) | (91) |
3#(2(5(x1))) | → | 4#(5(2(x1))) | (76) |
4#(0(4(2(x1)))) | → | 0#(x1) | (133) |
0#(3(2(x1))) | → | 0#(x1) | (55) |
0#(3(1(2(x1)))) | → | 3#(0(2(x1))) | (98) |
3#(2(5(x1))) | → | 3#(3(5(2(x1)))) | (77) |
3#(2(5(x1))) | → | 3#(4(5(4(2(x1))))) | (78) |
3#(2(5(x1))) | → | 4#(5(4(2(x1)))) | (79) |
4#(3(2(0(x1)))) | → | 3#(4(x1)) | (135) |
3#(2(5(x1))) | → | 5#(4(2(x1))) | (80) |
5#(4(2(0(2(x1))))) | → | 5#(0(4(2(1(2(x1)))))) | (178) |
5#(0(2(x1))) | → | 5#(x1) | (86) |
5#(5(0(0(x1)))) | → | 0#(5(5(0(x1)))) | (140) |
0#(3(2(4(x1)))) | → | 3#(0(4(4(x1)))) | (100) |
3#(0(2(4(x1)))) | → | 3#(0(4(2(1(1(x1)))))) | (106) |
3#(0(5(4(x1)))) | → | 3#(4(0(5(1(3(x1)))))) | (109) |
3#(0(5(4(x1)))) | → | 4#(0(5(1(3(x1))))) | (110) |
4#(3(2(0(x1)))) | → | 4#(x1) | (136) |
3#(0(5(4(x1)))) | → | 0#(5(1(3(x1)))) | (111) |
0#(3(2(4(x1)))) | → | 0#(4(4(x1))) | (101) |
0#(3(2(4(x1)))) | → | 4#(4(x1)) | (102) |
0#(5(3(1(2(x1))))) | → | 0#(x1) | (149) |
3#(0(5(4(x1)))) | → | 5#(1(3(x1))) | (112) |
5#(1(0(2(4(x1))))) | → | 5#(4(0(3(x1)))) | (171) |
5#(5(0(0(x1)))) | → | 5#(5(0(x1))) | (141) |
5#(5(0(0(x1)))) | → | 5#(0(x1)) | (142) |
5#(1(0(2(4(x1))))) | → | 4#(0(3(x1))) | (172) |
5#(1(0(2(4(x1))))) | → | 0#(3(x1)) | (173) |
5#(1(0(2(4(x1))))) | → | 3#(x1) | (174) |
3#(0(5(4(x1)))) | → | 3#(x1) | (113) |
3#(2(5(4(x1)))) | → | 3#(4(3(5(2(x1))))) | (122) |
3#(2(5(4(x1)))) | → | 4#(3(5(2(x1)))) | (123) |
3#(2(5(4(x1)))) | → | 3#(5(2(x1))) | (124) |
3#(2(5(4(x1)))) | → | 5#(2(x1)) | (125) |
3#(5(3(2(x1)))) | → | 3#(3(0(2(5(x1))))) | (126) |
3#(5(3(2(x1)))) | → | 3#(0(2(5(x1)))) | (127) |
3#(5(3(2(x1)))) | → | 5#(x1) | (129) |
3#(0(3(1(2(x1))))) | → | 3#(3(x1)) | (159) |
3#(0(3(1(2(x1))))) | → | 3#(x1) | (160) |
3#(5(1(4(0(x1))))) | → | 3#(3(4(5(0(x1))))) | (163) |
3#(5(1(4(0(x1))))) | → | 3#(4(5(0(x1)))) | (164) |
3#(5(1(4(0(x1))))) | → | 4#(5(0(x1))) | (165) |
3#(5(1(4(0(x1))))) | → | 5#(0(x1)) | (166) |
3#(5(3(0(4(x1))))) | → | 5#(3(4(x1))) | (169) |
3#(5(3(0(4(x1))))) | → | 3#(4(x1)) | (170) |
[0#(x1)] | = | 1 · x1 |
[3(x1)] | = | 1 · x1 |
[2(x1)] | = | 1 · x1 |
[3#(x1)] | = | 1 · x1 |
[0(x1)] | = | 1 · x1 |
[4#(x1)] | = | 1 · x1 |
[4(x1)] | = | 1 · x1 |
[5(x1)] | = | 1 + 1 · x1 |
[5#(x1)] | = | 1 + 1 · x1 |
[1(x1)] | = | 1 · x1 |
5#(2(4(x1))) | → | 3#(4(x1)) | (91) |
0#(5(3(1(2(x1))))) | → | 0#(x1) | (149) |
5#(5(0(0(x1)))) | → | 5#(0(x1)) | (142) |
5#(1(0(2(4(x1))))) | → | 4#(0(3(x1))) | (172) |
5#(1(0(2(4(x1))))) | → | 0#(3(x1)) | (173) |
5#(1(0(2(4(x1))))) | → | 3#(x1) | (174) |
3#(0(5(4(x1)))) | → | 3#(x1) | (113) |
3#(5(3(0(4(x1))))) | → | 3#(4(x1)) | (170) |
The dependency pairs are split into 1 component.
3#(2(0(x1))) | → | 3#(x1) | (62) |
3#(2(0(x1))) | → | 4#(x1) | (68) |
4#(0(4(2(x1)))) | → | 3#(0(x1)) | (132) |
3#(2(4(x1))) | → | 3#(3(4(x1))) | (69) |
3#(2(4(x1))) | → | 3#(4(x1)) | (70) |
3#(2(4(x1))) | → | 3#(x1) | (72) |
3#(2(5(x1))) | → | 3#(5(2(x1))) | (73) |
3#(2(5(x1))) | → | 4#(5(2(x1))) | (76) |
4#(0(4(2(x1)))) | → | 0#(x1) | (133) |
0#(3(2(x1))) | → | 3#(0(x1)) | (54) |
3#(2(5(x1))) | → | 3#(3(5(2(x1)))) | (77) |
3#(2(5(x1))) | → | 3#(4(5(4(2(x1))))) | (78) |
3#(2(5(x1))) | → | 4#(5(4(2(x1)))) | (79) |
4#(3(2(0(x1)))) | → | 3#(4(x1)) | (135) |
3#(2(5(x1))) | → | 5#(4(2(x1))) | (80) |
5#(4(2(0(2(x1))))) | → | 5#(0(4(2(1(2(x1)))))) | (178) |
5#(0(2(x1))) | → | 5#(x1) | (86) |
5#(5(0(0(x1)))) | → | 0#(5(5(0(x1)))) | (140) |
0#(3(2(x1))) | → | 0#(x1) | (55) |
0#(3(1(2(x1)))) | → | 3#(0(2(x1))) | (98) |
3#(0(2(4(x1)))) | → | 3#(0(4(2(1(1(x1)))))) | (106) |
3#(0(5(4(x1)))) | → | 3#(4(0(5(1(3(x1)))))) | (109) |
3#(0(5(4(x1)))) | → | 4#(0(5(1(3(x1))))) | (110) |
4#(3(2(0(x1)))) | → | 4#(x1) | (136) |
3#(0(5(4(x1)))) | → | 0#(5(1(3(x1)))) | (111) |
0#(3(2(4(x1)))) | → | 3#(0(4(4(x1)))) | (100) |
3#(0(5(4(x1)))) | → | 5#(1(3(x1))) | (112) |
5#(1(0(2(4(x1))))) | → | 5#(4(0(3(x1)))) | (171) |
5#(5(0(0(x1)))) | → | 5#(5(0(x1))) | (141) |
3#(2(5(4(x1)))) | → | 3#(4(3(5(2(x1))))) | (122) |
3#(2(5(4(x1)))) | → | 4#(3(5(2(x1)))) | (123) |
3#(2(5(4(x1)))) | → | 3#(5(2(x1))) | (124) |
3#(5(3(2(x1)))) | → | 3#(3(0(2(5(x1))))) | (126) |
3#(5(3(2(x1)))) | → | 3#(0(2(5(x1)))) | (127) |
3#(5(3(2(x1)))) | → | 5#(x1) | (129) |
3#(0(3(1(2(x1))))) | → | 3#(3(x1)) | (159) |
3#(0(3(1(2(x1))))) | → | 3#(x1) | (160) |
3#(5(1(4(0(x1))))) | → | 3#(3(4(5(0(x1))))) | (163) |
3#(5(1(4(0(x1))))) | → | 3#(4(5(0(x1)))) | (164) |
3#(5(1(4(0(x1))))) | → | 4#(5(0(x1))) | (165) |
3#(5(1(4(0(x1))))) | → | 5#(0(x1)) | (166) |
3#(5(3(0(4(x1))))) | → | 5#(3(4(x1))) | (169) |
0#(3(2(4(x1)))) | → | 0#(4(4(x1))) | (101) |
0#(3(2(4(x1)))) | → | 4#(4(x1)) | (102) |
[3#(x1)] | = | 1 + 1 · x1 |
[2(x1)] | = | 1 + 1 · x1 |
[0(x1)] | = | 1 · x1 |
[4#(x1)] | = | 1 · x1 |
[4(x1)] | = | 1 · x1 |
[3(x1)] | = | 1 · x1 |
[5(x1)] | = | 1 · x1 |
[0#(x1)] | = | 1 + 1 · x1 |
[5#(x1)] | = | 1 + 1 · x1 |
[1(x1)] | = | 1 · x1 |
3#(2(0(x1))) | → | 3#(x1) | (62) |
3#(2(0(x1))) | → | 4#(x1) | (68) |
3#(2(4(x1))) | → | 3#(3(4(x1))) | (69) |
3#(2(4(x1))) | → | 3#(4(x1)) | (70) |
3#(2(4(x1))) | → | 3#(x1) | (72) |
3#(2(5(x1))) | → | 4#(5(2(x1))) | (76) |
0#(3(2(x1))) | → | 3#(0(x1)) | (54) |
3#(2(5(x1))) | → | 4#(5(4(2(x1)))) | (79) |
5#(0(2(x1))) | → | 5#(x1) | (86) |
0#(3(2(x1))) | → | 0#(x1) | (55) |
3#(0(5(4(x1)))) | → | 4#(0(5(1(3(x1))))) | (110) |
4#(3(2(0(x1)))) | → | 4#(x1) | (136) |
0#(3(2(4(x1)))) | → | 3#(0(4(4(x1)))) | (100) |
5#(1(0(2(4(x1))))) | → | 5#(4(0(3(x1)))) | (171) |
3#(2(5(4(x1)))) | → | 4#(3(5(2(x1)))) | (123) |
3#(5(3(2(x1)))) | → | 5#(x1) | (129) |
3#(0(3(1(2(x1))))) | → | 3#(3(x1)) | (159) |
3#(0(3(1(2(x1))))) | → | 3#(x1) | (160) |
3#(5(1(4(0(x1))))) | → | 4#(5(0(x1))) | (165) |
0#(3(2(4(x1)))) | → | 0#(4(4(x1))) | (101) |
0#(3(2(4(x1)))) | → | 4#(4(x1)) | (102) |
The dependency pairs are split into 1 component.
3#(2(5(x1))) | → | 3#(3(5(2(x1)))) | (77) |
3#(2(5(x1))) | → | 3#(5(2(x1))) | (73) |
3#(2(5(x1))) | → | 3#(4(5(4(2(x1))))) | (78) |
3#(2(5(x1))) | → | 5#(4(2(x1))) | (80) |
5#(4(2(0(2(x1))))) | → | 5#(0(4(2(1(2(x1)))))) | (178) |
5#(5(0(0(x1)))) | → | 0#(5(5(0(x1)))) | (140) |
0#(3(1(2(x1)))) | → | 3#(0(2(x1))) | (98) |
3#(0(2(4(x1)))) | → | 3#(0(4(2(1(1(x1)))))) | (106) |
3#(0(5(4(x1)))) | → | 3#(4(0(5(1(3(x1)))))) | (109) |
3#(0(5(4(x1)))) | → | 0#(5(1(3(x1)))) | (111) |
3#(2(5(4(x1)))) | → | 3#(4(3(5(2(x1))))) | (122) |
3#(2(5(4(x1)))) | → | 3#(5(2(x1))) | (124) |
3#(5(3(2(x1)))) | → | 3#(3(0(2(5(x1))))) | (126) |
3#(5(3(2(x1)))) | → | 3#(0(2(5(x1)))) | (127) |
3#(5(1(4(0(x1))))) | → | 3#(3(4(5(0(x1))))) | (163) |
3#(5(1(4(0(x1))))) | → | 3#(4(5(0(x1)))) | (164) |
3#(5(1(4(0(x1))))) | → | 5#(0(x1)) | (166) |
5#(5(0(0(x1)))) | → | 5#(5(0(x1))) | (141) |
3#(5(3(0(4(x1))))) | → | 5#(3(4(x1))) | (169) |
[3#(x1)] | = | 0 |
[2(x1)] | = | 0 |
[5(x1)] | = | 0 |
[3(x1)] | = | 1 |
[4(x1)] | = | 0 |
[5#(x1)] | = | 0 |
[0(x1)] | = | 0 |
[1(x1)] | = | 0 |
[0#(x1)] | = | 1 · x1 |
5(2(4(x1))) | → | 5(2(1(1(3(4(x1)))))) | (19) |
5(4(2(0(2(x1))))) | → | 5(0(4(2(1(2(x1)))))) | (48) |
5(0(2(x1))) | → | 1(1(0(2(5(x1))))) | (17) |
5(0(4(x1))) | → | 0(5(4(1(1(x1))))) | (18) |
5(3(2(x1))) | → | 1(1(3(5(1(2(x1)))))) | (20) |
5(5(0(x1))) | → | 5(1(1(5(0(x1))))) | (21) |
5(4(1(0(x1)))) | → | 5(1(1(4(0(1(x1)))))) | (35) |
5(5(0(0(x1)))) | → | 1(1(0(5(5(0(x1)))))) | (36) |
5(5(2(2(x1)))) | → | 5(5(1(1(2(2(x1)))))) | (37) |
5(1(0(2(4(x1))))) | → | 2(1(5(4(0(3(x1)))))) | (46) |
5(1(3(2(0(x1))))) | → | 2(3(5(0(1(1(x1)))))) | (47) |
0#(3(1(2(x1)))) | → | 3#(0(2(x1))) | (98) |
The dependency pairs are split into 2 components.
3#(2(5(x1))) | → | 3#(5(2(x1))) | (73) |
3#(2(5(x1))) | → | 3#(3(5(2(x1)))) | (77) |
3#(2(5(x1))) | → | 3#(4(5(4(2(x1))))) | (78) |
3#(0(2(4(x1)))) | → | 3#(0(4(2(1(1(x1)))))) | (106) |
3#(0(5(4(x1)))) | → | 3#(4(0(5(1(3(x1)))))) | (109) |
3#(2(5(4(x1)))) | → | 3#(4(3(5(2(x1))))) | (122) |
3#(2(5(4(x1)))) | → | 3#(5(2(x1))) | (124) |
3#(5(3(2(x1)))) | → | 3#(3(0(2(5(x1))))) | (126) |
3#(5(3(2(x1)))) | → | 3#(0(2(5(x1)))) | (127) |
3#(5(1(4(0(x1))))) | → | 3#(3(4(5(0(x1))))) | (163) |
3#(5(1(4(0(x1))))) | → | 3#(4(5(0(x1)))) | (164) |
[3#(x1)] | = | 1 · x1 |
[2(x1)] | = | 1 |
[5(x1)] | = | 0 |
[3(x1)] | = | 0 |
[4(x1)] | = | 0 |
[0(x1)] | = | 0 |
[1(x1)] | = | 0 |
5(2(4(x1))) | → | 5(2(1(1(3(4(x1)))))) | (19) |
3(0(4(x1))) | → | 0(1(3(4(1(x1))))) | (5) |
3(2(0(x1))) | → | 0(2(1(3(x1)))) | (6) |
3(2(0(x1))) | → | 3(0(2(1(x1)))) | (7) |
3(2(0(x1))) | → | 0(1(2(1(3(x1))))) | (8) |
3(2(0(x1))) | → | 3(0(1(2(1(4(x1)))))) | (9) |
3(2(4(x1))) | → | 1(2(1(3(3(4(x1)))))) | (10) |
3(2(4(x1))) | → | 4(1(2(1(1(3(x1)))))) | (11) |
3(2(5(x1))) | → | 1(3(5(2(x1)))) | (12) |
3(2(5(x1))) | → | 3(1(4(5(2(x1))))) | (13) |
3(2(5(x1))) | → | 1(1(3(3(5(2(x1)))))) | (14) |
3(2(5(x1))) | → | 1(3(4(5(4(2(x1)))))) | (15) |
3(5(0(x1))) | → | 3(1(0(5(1(1(x1)))))) | (16) |
3(0(5(4(x1)))) | → | 3(4(0(5(1(3(x1)))))) | (27) |
3(0(2(4(x1)))) | → | 3(0(4(2(1(1(x1)))))) | (26) |
3(2(5(4(x1)))) | → | 3(4(3(5(2(x1))))) | (31) |
3(5(3(2(x1)))) | → | 3(3(0(2(5(x1))))) | (32) |
3(1(0(0(x1)))) | → | 0(1(1(3(0(1(x1)))))) | (28) |
3(2(4(0(x1)))) | → | 3(1(0(4(2(x1))))) | (29) |
3(2(4(5(x1)))) | → | 3(1(4(2(1(5(x1)))))) | (30) |
3(0(1(4(5(x1))))) | → | 3(4(0(5(1(1(x1)))))) | (41) |
3(0(3(1(2(x1))))) | → | 0(2(1(1(3(3(x1)))))) | (42) |
3(2(2(0(4(x1))))) | → | 3(2(2(0(1(4(x1)))))) | (43) |
3(5(1(4(0(x1))))) | → | 1(3(3(4(5(0(x1)))))) | (44) |
3(5(3(0(4(x1))))) | → | 3(0(1(5(3(4(x1)))))) | (45) |
4(0(4(2(x1)))) | → | 4(4(2(1(3(0(x1)))))) | (33) |
4(3(2(0(x1)))) | → | 0(2(1(3(4(x1))))) | (34) |
0(4(2(x1))) | → | 4(1(1(1(0(2(x1)))))) | (4) |
0(2(0(x1))) | → | 0(0(2(1(1(x1))))) | (2) |
3#(2(5(x1))) | → | 3#(5(2(x1))) | (73) |
3#(2(5(x1))) | → | 3#(3(5(2(x1)))) | (77) |
3#(2(5(x1))) | → | 3#(4(5(4(2(x1))))) | (78) |
3#(2(5(4(x1)))) | → | 3#(4(3(5(2(x1))))) | (122) |
3#(2(5(4(x1)))) | → | 3#(5(2(x1))) | (124) |
[3#(x1)] | = | 1 · x1 |
[0(x1)] | = | 0 |
[2(x1)] | = | 0 |
[4(x1)] | = | 0 |
[1(x1)] | = | 0 |
[5(x1)] | = | 1 |
[3(x1)] | = | 0 |
0(4(2(x1))) | → | 4(1(1(1(0(2(x1)))))) | (4) |
3(0(4(x1))) | → | 0(1(3(4(1(x1))))) | (5) |
3(2(0(x1))) | → | 0(2(1(3(x1)))) | (6) |
3(2(0(x1))) | → | 3(0(2(1(x1)))) | (7) |
3(2(0(x1))) | → | 0(1(2(1(3(x1))))) | (8) |
3(2(0(x1))) | → | 3(0(1(2(1(4(x1)))))) | (9) |
3(2(4(x1))) | → | 1(2(1(3(3(4(x1)))))) | (10) |
3(2(4(x1))) | → | 4(1(2(1(1(3(x1)))))) | (11) |
3(2(5(x1))) | → | 1(3(5(2(x1)))) | (12) |
3(2(5(x1))) | → | 3(1(4(5(2(x1))))) | (13) |
3(2(5(x1))) | → | 1(1(3(3(5(2(x1)))))) | (14) |
3(2(5(x1))) | → | 1(3(4(5(4(2(x1)))))) | (15) |
3(5(0(x1))) | → | 3(1(0(5(1(1(x1)))))) | (16) |
3(0(5(4(x1)))) | → | 3(4(0(5(1(3(x1)))))) | (27) |
3(0(2(4(x1)))) | → | 3(0(4(2(1(1(x1)))))) | (26) |
3(2(5(4(x1)))) | → | 3(4(3(5(2(x1))))) | (31) |
3(5(3(2(x1)))) | → | 3(3(0(2(5(x1))))) | (32) |
3(1(0(0(x1)))) | → | 0(1(1(3(0(1(x1)))))) | (28) |
3(2(4(0(x1)))) | → | 3(1(0(4(2(x1))))) | (29) |
3(2(4(5(x1)))) | → | 3(1(4(2(1(5(x1)))))) | (30) |
3(0(1(4(5(x1))))) | → | 3(4(0(5(1(1(x1)))))) | (41) |
3(0(3(1(2(x1))))) | → | 0(2(1(1(3(3(x1)))))) | (42) |
3(2(2(0(4(x1))))) | → | 3(2(2(0(1(4(x1)))))) | (43) |
3(5(1(4(0(x1))))) | → | 1(3(3(4(5(0(x1)))))) | (44) |
3(5(3(0(4(x1))))) | → | 3(0(1(5(3(4(x1)))))) | (45) |
0(2(0(x1))) | → | 0(0(2(1(1(x1))))) | (2) |
4(0(4(2(x1)))) | → | 4(4(2(1(3(0(x1)))))) | (33) |
4(3(2(0(x1)))) | → | 0(2(1(3(4(x1))))) | (34) |
3#(5(3(2(x1)))) | → | 3#(3(0(2(5(x1))))) | (126) |
3#(5(3(2(x1)))) | → | 3#(0(2(5(x1)))) | (127) |
3#(5(1(4(0(x1))))) | → | 3#(3(4(5(0(x1))))) | (163) |
3#(5(1(4(0(x1))))) | → | 3#(4(5(0(x1)))) | (164) |
[3#(x1)] | = | 1 · x1 |
[0(x1)] | = | 1 · x1 |
[2(x1)] | = | 1 + 1 · x1 |
[4(x1)] | = | 1 |
[1(x1)] | = | 0 |
[5(x1)] | = | 1 + 1 · x1 |
[3(x1)] | = | 0 |
0(4(2(x1))) | → | 4(1(1(1(0(2(x1)))))) | (4) |
4(0(4(2(x1)))) | → | 4(4(2(1(3(0(x1)))))) | (33) |
4(3(2(0(x1)))) | → | 0(2(1(3(4(x1))))) | (34) |
3#(0(2(4(x1)))) | → | 3#(0(4(2(1(1(x1)))))) | (106) |
3#(0(5(4(x1)))) | → | 3#(4(0(5(1(3(x1)))))) | (109) |
There are no pairs anymore.
5#(5(0(0(x1)))) | → | 5#(5(0(x1))) | (141) |
5#(4(2(0(2(x1))))) | → | 5#(0(4(2(1(2(x1)))))) | (178) |
[5#(x1)] | = | 1 · x1 |
[5(x1)] | = | 1 |
[0(x1)] | = | 1 · x1 |
[4(x1)] | = | 1 + 1 · x1 |
[2(x1)] | = | 1 + 1 · x1 |
[1(x1)] | = | 0 |
[3(x1)] | = | 0 |
0(4(2(x1))) | → | 4(1(1(1(0(2(x1)))))) | (4) |
5(0(2(x1))) | → | 1(1(0(2(5(x1))))) | (17) |
5(0(4(x1))) | → | 0(5(4(1(1(x1))))) | (18) |
5(2(4(x1))) | → | 5(2(1(1(3(4(x1)))))) | (19) |
5(3(2(x1))) | → | 1(1(3(5(1(2(x1)))))) | (20) |
5(5(0(x1))) | → | 5(1(1(5(0(x1))))) | (21) |
5(4(1(0(x1)))) | → | 5(1(1(4(0(1(x1)))))) | (35) |
5(5(0(0(x1)))) | → | 1(1(0(5(5(0(x1)))))) | (36) |
5(5(2(2(x1)))) | → | 5(5(1(1(2(2(x1)))))) | (37) |
5(1(0(2(4(x1))))) | → | 2(1(5(4(0(3(x1)))))) | (46) |
5(1(3(2(0(x1))))) | → | 2(3(5(0(1(1(x1)))))) | (47) |
5(4(2(0(2(x1))))) | → | 5(0(4(2(1(2(x1)))))) | (48) |
3(5(0(x1))) | → | 3(1(0(5(1(1(x1)))))) | (16) |
5#(4(2(0(2(x1))))) | → | 5#(0(4(2(1(2(x1)))))) | (178) |
[5#(x1)] | = |
|
||||||||||||||||||
[5(x1)] | = |
|
||||||||||||||||||
[0(x1)] | = |
|
||||||||||||||||||
[1(x1)] | = |
|
||||||||||||||||||
[2(x1)] | = |
|
||||||||||||||||||
[3(x1)] | = |
|
||||||||||||||||||
[4(x1)] | = |
|
0(0(0(x1))) | → | 0(0(1(0(1(x1))))) | (1) |
0(2(0(x1))) | → | 0(0(2(1(1(x1))))) | (2) |
0(3(2(x1))) | → | 2(1(3(0(x1)))) | (3) |
0(4(2(x1))) | → | 4(1(1(1(0(2(x1)))))) | (4) |
0(0(2(4(x1)))) | → | 0(4(0(2(1(1(x1)))))) | (22) |
0(3(1(2(x1)))) | → | 1(1(3(0(2(x1))))) | (23) |
0(3(2(4(x1)))) | → | 2(1(3(0(4(4(x1)))))) | (24) |
0(4(3(2(x1)))) | → | 2(3(4(0(1(x1))))) | (25) |
0(0(1(2(4(x1))))) | → | 0(0(2(1(1(4(x1)))))) | (38) |
0(5(3(1(2(x1))))) | → | 5(2(1(3(1(0(x1)))))) | (39) |
0(5(5(1(0(x1))))) | → | 5(0(0(5(1(1(x1)))))) | (40) |
5(0(2(x1))) | → | 1(1(0(2(5(x1))))) | (17) |
5(0(4(x1))) | → | 0(5(4(1(1(x1))))) | (18) |
5(2(4(x1))) | → | 5(2(1(1(3(4(x1)))))) | (19) |
5(3(2(x1))) | → | 1(1(3(5(1(2(x1)))))) | (20) |
5(5(0(x1))) | → | 5(1(1(5(0(x1))))) | (21) |
5(4(1(0(x1)))) | → | 5(1(1(4(0(1(x1)))))) | (35) |
5(5(0(0(x1)))) | → | 1(1(0(5(5(0(x1)))))) | (36) |
5(5(2(2(x1)))) | → | 5(5(1(1(2(2(x1)))))) | (37) |
5(1(0(2(4(x1))))) | → | 2(1(5(4(0(3(x1)))))) | (46) |
5(1(3(2(0(x1))))) | → | 2(3(5(0(1(1(x1)))))) | (47) |
5(4(2(0(2(x1))))) | → | 5(0(4(2(1(2(x1)))))) | (48) |
3(5(0(x1))) | → | 3(1(0(5(1(1(x1)))))) | (16) |
5#(5(0(0(x1)))) | → | 5#(5(0(x1))) | (141) |
There are no pairs anymore.