The rewrite relation of the following TRS is considered.
tower(0(x1)) | → | s(0(p(s(p(s(x1)))))) | (1) |
tower(s(x1)) | → | p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) | (2) |
twoto(0(x1)) | → | s(0(x1)) | (3) |
twoto(s(x1)) | → | p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) | (4) |
twice(0(x1)) | → | 0(x1) | (5) |
twice(s(x1)) | → | p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) | (6) |
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
[0(x1)] | = |
x1 +
|
||||
[s(x1)] | = |
x1 +
|
||||
[p(x1)] | = |
x1 +
|
||||
[tower(x1)] | = |
x1 +
|
||||
[twoto(x1)] | = |
x1 +
|
||||
[twice(x1)] | = |
x1 +
|
tower(0(x1)) | → | s(0(p(s(p(s(x1)))))) | (1) |
p#(p(s(x1))) | → | p#(x1) | (10) |
tower#(s(x1)) | → | p#(s(x1)) | (11) |
tower#(s(x1)) | → | p#(s(p(s(x1)))) | (12) |
tower#(s(x1)) | → | p#(s(p(s(tower(p(s(p(s(x1))))))))) | (13) |
tower#(s(x1)) | → | p#(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) | (14) |
tower#(s(x1)) | → | p#(s(tower(p(s(p(s(x1))))))) | (15) |
tower#(s(x1)) | → | p#(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))) | (16) |
tower#(s(x1)) | → | tower#(p(s(p(s(x1))))) | (17) |
tower#(s(x1)) | → | twoto#(p(s(p(s(tower(p(s(p(s(x1)))))))))) | (18) |
twoto#(s(x1)) | → | p#(s(x1)) | (19) |
twoto#(s(x1)) | → | p#(s(s(s(twoto(p(s(p(s(x1))))))))) | (20) |
twoto#(s(x1)) | → | p#(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))) | (21) |
twoto#(s(x1)) | → | p#(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))) | (22) |
twoto#(s(x1)) | → | p#(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))) | (23) |
twoto#(s(x1)) | → | p#(s(p(s(x1)))) | (24) |
twoto#(s(x1)) | → | p#(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))) | (25) |
twoto#(s(x1)) | → | p#(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))) | (26) |
twoto#(s(x1)) | → | p#(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))) | (27) |
twoto#(s(x1)) | → | p#(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))) | (28) |
twoto#(s(x1)) | → | p#(p(s(s(s(twoto(p(s(p(s(x1)))))))))) | (29) |
twoto#(s(x1)) | → | p#(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))) | (30) |
twoto#(s(x1)) | → | p#(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) | (31) |
twoto#(s(x1)) | → | p#(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))) | (32) |
twoto#(s(x1)) | → | p#(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))) | (33) |
twoto#(s(x1)) | → | twoto#(p(s(p(s(x1))))) | (34) |
twoto#(s(x1)) | → | twice#(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))) | (35) |
twice#(s(x1)) | → | p#(s(s(s(x1)))) | (36) |
twice#(s(x1)) | → | p#(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))) | (37) |
twice#(s(x1)) | → | p#(p(s(s(s(x1))))) | (38) |
twice#(s(x1)) | → | p#(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))) | (39) |
twice#(s(x1)) | → | p#(p(p(s(s(s(x1)))))) | (40) |
twice#(s(x1)) | → | p#(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) | (41) |
twice#(s(x1)) | → | twice#(p(p(p(s(s(s(x1))))))) | (42) |
[0(x1)] | = |
x1 +
|
||||
[s(x1)] | = |
x1 +
|
||||
[p(x1)] | = |
x1 +
|
||||
[tower(x1)] | = |
x1 +
|
||||
[twoto(x1)] | = |
x1 +
|
||||
[twice(x1)] | = |
x1 +
|
||||
[p#(x1)] | = |
x1 +
|
||||
[tower#(x1)] | = |
x1 +
|
||||
[twoto#(x1)] | = |
x1 +
|
||||
[twice#(x1)] | = |
x1 +
|
tower(s(x1)) | → | p(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) | (2) |
twoto(0(x1)) | → | s(0(x1)) | (3) |
twoto(s(x1)) | → | p(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) | (4) |
twice(0(x1)) | → | 0(x1) | (5) |
twice(s(x1)) | → | p(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) | (6) |
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
tower#(s(x1)) | → | p#(s(x1)) | (11) |
tower#(s(x1)) | → | p#(s(p(s(x1)))) | (12) |
tower#(s(x1)) | → | p#(s(p(s(tower(p(s(p(s(x1))))))))) | (13) |
tower#(s(x1)) | → | p#(s(p(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))))) | (14) |
tower#(s(x1)) | → | p#(s(tower(p(s(p(s(x1))))))) | (15) |
tower#(s(x1)) | → | p#(s(twoto(p(s(p(s(tower(p(s(p(s(x1)))))))))))) | (16) |
tower#(s(x1)) | → | twoto#(p(s(p(s(tower(p(s(p(s(x1)))))))))) | (18) |
twoto#(s(x1)) | → | p#(s(x1)) | (19) |
twoto#(s(x1)) | → | p#(s(s(s(twoto(p(s(p(s(x1))))))))) | (20) |
twoto#(s(x1)) | → | p#(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))) | (21) |
twoto#(s(x1)) | → | p#(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))) | (22) |
twoto#(s(x1)) | → | p#(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))) | (23) |
twoto#(s(x1)) | → | p#(s(p(s(x1)))) | (24) |
twoto#(s(x1)) | → | p#(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))) | (25) |
twoto#(s(x1)) | → | p#(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))) | (26) |
twoto#(s(x1)) | → | p#(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))))) | (27) |
twoto#(s(x1)) | → | p#(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))) | (28) |
twoto#(s(x1)) | → | p#(p(s(s(s(twoto(p(s(p(s(x1)))))))))) | (29) |
twoto#(s(x1)) | → | p#(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))) | (30) |
twoto#(s(x1)) | → | p#(p(s(p(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))))))))))))))))))) | (31) |
twoto#(s(x1)) | → | p#(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))) | (32) |
twoto#(s(x1)) | → | p#(p(p(s(s(p(s(s(p(s(s(p(s(twice(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1))))))))))))))))))))))))))))) | (33) |
twoto#(s(x1)) | → | twice#(p(s(p(s(p(p(p(s(s(s(twoto(p(s(p(s(x1)))))))))))))))) | (35) |
twice#(s(x1)) | → | p#(s(s(s(x1)))) | (36) |
twice#(s(x1)) | → | p#(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))) | (37) |
twice#(s(x1)) | → | p#(p(s(s(s(x1))))) | (38) |
twice#(s(x1)) | → | p#(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1)))))))))))))) | (39) |
twice#(s(x1)) | → | p#(p(p(s(s(s(x1)))))) | (40) |
twice#(s(x1)) | → | p#(p(p(s(s(s(s(s(twice(p(p(p(s(s(s(x1))))))))))))))) | (41) |
The dependency pairs are split into 4 components.
p#(p(s(x1))) | → | p#(x1) | (10) |
[s(x1)] | = |
x1 +
|
||||
[p(x1)] | = |
x1 +
|
||||
[p#(x1)] | = |
x1 +
|
p#(p(s(x1))) | → | p#(x1) | (10) |
The dependency pairs are split into 0 components.
tower#(s(x1)) | → | tower#(p(s(p(s(x1))))) | (17) |
[0(x1)] | = |
|
||||||||||||
[s(x1)] | = |
|
||||||||||||
[p(x1)] | = |
|
||||||||||||
[tower#(x1)] | = |
|
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
tower#(s(x1)) | → | tower#(p(s(p(s(x1))))) | (17) |
[0(x1)] | = |
x1 +
|
||||
[s(x1)] | = |
x1 +
|
||||
[p(x1)] | = |
x1 +
|
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
The dependency pairs are split into 0 components.
twoto#(s(x1)) | → | twoto#(p(s(p(s(x1))))) | (34) |
[0(x1)] | = |
|
||||||||||||
[s(x1)] | = |
|
||||||||||||
[p(x1)] | = |
|
||||||||||||
[twoto#(x1)] | = |
|
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
twoto#(s(x1)) | → | twoto#(p(s(p(s(x1))))) | (34) |
[0(x1)] | = |
x1 +
|
||||
[s(x1)] | = |
x1 +
|
||||
[p(x1)] | = |
x1 +
|
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
The dependency pairs are split into 0 components.
twice#(s(x1)) | → | twice#(p(p(p(s(s(s(x1))))))) | (42) |
[0(x1)] | = |
|
||||||||||||||||||||||||||
[s(x1)] | = |
|
||||||||||||||||||||||||||
[p(x1)] | = |
|
||||||||||||||||||||||||||
[twice#(x1)] | = |
|
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
twice#(s(x1)) | → | twice#(p(p(p(s(s(s(x1))))))) | (42) |
[0(x1)] | = |
x1 +
|
||||
[s(x1)] | = |
x1 +
|
||||
[p(x1)] | = |
x1 +
|
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
p(p(s(x1))) | → | p(x1) | (7) |
p(s(x1)) | → | x1 | (8) |
p(0(x1)) | → | 0(s(s(s(s(s(s(s(s(x1))))))))) | (9) |
The dependency pairs are split into 0 components.