by ttt2 (version ttt2 1.15)
The rewrite relation of the following TRS is considered.
| B(x0) | → | W(M(M(V(x0)))) |
| M(x0) | → | x0 |
| M(V(a(x0))) | → | V(Xa(x0)) |
| M(V(b(x0))) | → | V(Xb(x0)) |
| M(V(c(x0))) | → | V(Xc(x0)) |
| Xa(a(x0)) | → | a(Xa(x0)) |
| Xa(b(x0)) | → | b(Xa(x0)) |
| Xa(c(x0)) | → | c(Xa(x0)) |
| Xb(a(x0)) | → | a(Xb(x0)) |
| Xb(b(x0)) | → | b(Xb(x0)) |
| Xb(c(x0)) | → | c(Xb(x0)) |
| Xc(a(x0)) | → | a(Xc(x0)) |
| Xc(b(x0)) | → | b(Xc(x0)) |
| Xc(c(x0)) | → | c(Xc(x0)) |
| Xa(E(x0)) | → | a(E(x0)) |
| Xb(E(x0)) | → | b(E(x0)) |
| Xc(E(x0)) | → | c(E(x0)) |
| W(V(x0)) | → | R(L(x0)) |
| L(a(x0)) | → | Ya(L(x0)) |
| L(b(x0)) | → | Yb(L(x0)) |
| L(c(x0)) | → | Yc(L(x0)) |
| L(a(x0)) | → | D(x0) |
| L(a(x0)) | → | D(b(c(x0))) |
| L(b(b(x0))) | → | D(a(a(x0))) |
| L(c(c(c(x0)))) | → | D(b(x0)) |
| Ya(D(x0)) | → | D(a(x0)) |
| Yb(D(x0)) | → | D(b(x0)) |
| Yc(D(x0)) | → | D(c(x0)) |
| R(D(x0)) | → | B(x0) |
| B(x0) | → | W(M(M(V(x0)))) |
| M(x0) | → | x0 |
| M(V(a(x0))) | → | V(Xa(x0)) |
| M(V(b(x0))) | → | V(Xb(x0)) |
| M(V(c(x0))) | → | V(Xc(x0)) |
| Xa(a(x0)) | → | a(Xa(x0)) |
| Xa(b(x0)) | → | b(Xa(x0)) |
| Xa(c(x0)) | → | c(Xa(x0)) |
| Xb(a(x0)) | → | a(Xb(x0)) |
| Xb(b(x0)) | → | b(Xb(x0)) |
| Xb(c(x0)) | → | c(Xb(x0)) |
| Xc(a(x0)) | → | a(Xc(x0)) |
| Xc(b(x0)) | → | b(Xc(x0)) |
| Xc(c(x0)) | → | c(Xc(x0)) |
| Xa(E(x0)) | → | a(E(x0)) |
| Xb(E(x0)) | → | b(E(x0)) |
| Xc(E(x0)) | → | c(E(x0)) |
| W(V(x0)) | → | R(L(x0)) |
| L(a(x0)) | → | Ya(L(x0)) |
| L(b(x0)) | → | Yb(L(x0)) |
| L(c(x0)) | → | Yc(L(x0)) |
| L(a(x0)) | → | D(x0) |
| L(a(x0)) | → | D(b(c(x0))) |
| L(b(b(x0))) | → | D(a(a(x0))) |
| L(c(c(c(x0)))) | → | D(b(x0)) |
| Ya(D(x0)) | → | D(a(x0)) |
| Yb(D(x0)) | → | D(b(x0)) |
| Yc(D(x0)) | → | D(c(x0)) |
| R(D(x0)) | → | B(x0) |