by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
a(b(c(a(b(c(a(a(a(x0))))))))) | → | a(a(a(a(b(c(a(b(c(a(b(c(x0)))))))))))) |
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(b(c(x0))) |
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(b(c(a(b(c(x0)))))) |
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(b(c(a(b(c(a(b(c(x0))))))))) |
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(a(b(c(a(b(c(a(b(c(x0)))))))))) |
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(a(a(b(c(a(b(c(a(b(c(x0))))))))))) |
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(a(a(a(b(c(a(b(c(a(b(c(x0)))))))))))) |
The dependency pairs are split into 1 component.
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(b(c(a(b(c(a(b(c(x0))))))))) |
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(b(c(a(b(c(x0)))))) |
a#(b(c(a(b(c(a(a(a(x0))))))))) | → | a#(b(c(x0))) |
[c(x1)] | = |
|
||||||||||||||||||
[a#(x1)] | = |
|
||||||||||||||||||
[a(x1)] | = |
|
||||||||||||||||||
[b(x1)] | = |
|
There are no pairs anymore.