The rewrite relation of the following TRS is considered.
p(a(x0),p(b(x1),p(a(x2),x3))) | → | p(x2,p(a(a(x0)),p(b(x1),x3))) | (1) |
p#(a(x0),p(b(x1),p(a(x2),x3))) | → | p#(a(a(x0)),p(b(x1),x3)) | (2) |
p#(a(x0),p(b(x1),p(a(x2),x3))) | → | p#(b(x1),x3) | (3) |
p#(a(x0),p(b(x1),p(a(x2),x3))) | → | p#(x2,p(a(a(x0)),p(b(x1),x3))) | (4) |
The dependency pairs are split into 1 component.
p#(a(x0),p(b(x1),p(a(x2),x3))) | → | p#(x2,p(a(a(x0)),p(b(x1),x3))) | (4) |
p#(a(x0),p(b(x1),p(a(x2),x3))) | → | p#(a(a(x0)),p(b(x1),x3)) | (2) |
[a(x1)] | = | x1 + 30613 |
[b(x1)] | = | 42736 |
[p#(x1, x2)] | = | x1 + x2 + 0 |
[p(x1, x2)] | = | x1 + x2 + 1 |
p(a(x0),p(b(x1),p(a(x2),x3))) | → | p(x2,p(a(a(x0)),p(b(x1),x3))) | (1) |
p#(a(x0),p(b(x1),p(a(x2),x3))) | → | p#(a(a(x0)),p(b(x1),x3)) | (2) |
The dependency pairs are split into 1 component.
p#(a(x0),p(b(x1),p(a(x2),x3))) | → | p#(x2,p(a(a(x0)),p(b(x1),x3))) | (4) |
[a(x1)] | = |
|
|||||||||||||||||||
[b(x1)] | = |
|
|||||||||||||||||||
[p#(x1, x2)] | = |
|
|||||||||||||||||||
[p(x1, x2)] | = |
|
p(a(x0),p(b(x1),p(a(x2),x3))) | → | p(x2,p(a(a(x0)),p(b(x1),x3))) | (1) |
p#(a(x0),p(b(x1),p(a(x2),x3))) | → | p#(x2,p(a(a(x0)),p(b(x1),x3))) | (4) |
The dependency pairs are split into 0 components.