MAYBE Termination Proof

Termination Proof

by ttt2 (version ttt2 1.15)

Input

The rewrite relation of the following TRS is considered.

B(x0) → W(M(M(M(M(M(M(M(M(M(M(M(M(M(M(M(V(x0)))))))))))))))))
M(x0) → x0
M(V(0(x0))) → V(X0(x0))
M(V(1(x0))) → V(X1(x0))
M(V(2(x0))) → V(X2(x0))
M(V(3(x0))) → V(X3(x0))
M(V(4(x0))) → V(X4(x0))
M(V(5(x0))) → V(X5(x0))
X0(0(x0)) → 0(X0(x0))
X0(1(x0)) → 1(X0(x0))
X0(2(x0)) → 2(X0(x0))
X0(3(x0)) → 3(X0(x0))
X0(4(x0)) → 4(X0(x0))
X0(5(x0)) → 5(X0(x0))
X1(0(x0)) → 0(X1(x0))
X1(1(x0)) → 1(X1(x0))
X1(2(x0)) → 2(X1(x0))
X1(3(x0)) → 3(X1(x0))
X1(4(x0)) → 4(X1(x0))
X1(5(x0)) → 5(X1(x0))
X2(0(x0)) → 0(X2(x0))
X2(1(x0)) → 1(X2(x0))
X2(2(x0)) → 2(X2(x0))
X2(3(x0)) → 3(X2(x0))
X2(4(x0)) → 4(X2(x0))
X2(5(x0)) → 5(X2(x0))
X3(0(x0)) → 0(X3(x0))
X3(1(x0)) → 1(X3(x0))
X3(2(x0)) → 2(X3(x0))
X3(3(x0)) → 3(X3(x0))
X3(4(x0)) → 4(X3(x0))
X3(5(x0)) → 5(X3(x0))
X4(0(x0)) → 0(X4(x0))
X4(1(x0)) → 1(X4(x0))
X4(2(x0)) → 2(X4(x0))
X4(3(x0)) → 3(X4(x0))
X4(4(x0)) → 4(X4(x0))
X4(5(x0)) → 5(X4(x0))
X5(0(x0)) → 0(X5(x0))
X5(1(x0)) → 1(X5(x0))
X5(2(x0)) → 2(X5(x0))
X5(3(x0)) → 3(X5(x0))
X5(4(x0)) → 4(X5(x0))
X5(5(x0)) → 5(X5(x0))
X0(E(x0)) → 0(E(x0))
X1(E(x0)) → 1(E(x0))
X2(E(x0)) → 2(E(x0))
X3(E(x0)) → 3(E(x0))
X4(E(x0)) → 4(E(x0))
X5(E(x0)) → 5(E(x0))
W(V(x0)) → R(L(x0))
L(0(x0)) → Y0(L(x0))
L(1(x0)) → Y1(L(x0))
L(2(x0)) → Y2(L(x0))
L(3(x0)) → Y3(L(x0))
L(4(x0)) → Y4(L(x0))
L(5(x0)) → Y5(L(x0))
L(0(0(1(0(2(3(4(0(4(1(2(4(4(2(3(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(0(1(5(0(3(0(4(2(3(1(5(0(5(2(1(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(0(1(5(0(3(0(4(2(3(1(5(0(5(2(1(x0))))))))))))))))) → D(0(3(5(2(2(1(1(4(5(4(0(1(5(4(2(1(x0)))))))))))))))))
L(0(0(1(5(0(3(0(4(2(3(1(5(0(5(2(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(0(2(3(2(0(3(0(0(1(1(2(2(5(2(5(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(0(0(1(0(2(3(4(0(4(1(2(4(4(2(3(2(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(0(1(4(3(4(3(4(3(4(0(4(0(2(1(1(2(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(0(1(4(3(4(3(4(3(4(0(4(0(2(1(1(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(1(4(3(4(3(4(3(4(0(4(0(2(1(1(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(0(3(5(3(3(2(2(2(3(0(4(0(4(1(0(1(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(3(5(3(3(2(2(2(3(0(4(0(4(1(0(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(0(0(3(3(3(2(3(0(2(5(5(3(5(4(1(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(1(4(4(2(0(0(2(3(2(4(3(4(4(2(1(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(1(5(0(4(3(1(1(5(5(2(2(4(4(1(5(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(1(5(2(0(3(0(2(3(5(5(1(0(5(4(2(5(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(2(2(1(5(2(4(2(5(2(3(2(3(1(3(2(5(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(2(3(5(1(2(3(2(4(1(1(4(2(0(0(3(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(2(4(4(1(3(0(0(2(1(5(2(3(0(3(3(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(4(1(0(5(2(0(2(1(0(0(5(0(3(4(0(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(4(2(4(0(4(5(4(0(1(4(2(2(4(2(3(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(4(3(5(5(5(1(0(4(0(4(5(4(4(2(5(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(5(2(4(5(3(5(0(3(4(1(2(0(3(3(2(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(5(5(2(5(2(4(2(3(0(0(2(0(0(4(2(0(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(0(1(0(2(3(4(0(4(1(2(4(4(2(3(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(1(4(3(4(3(4(3(4(0(4(0(2(1(1(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(1(4(4(2(0(0(2(3(2(4(3(4(4(2(1(0(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(2(4(3(1(2(1(4(5(2(2(2(2(4(0(4(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(0(3(5(2(2(1(1(4(5(4(0(1(5(4(2(1(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(0(3(5(3(3(2(2(2(3(0(4(0(4(1(0(1(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(1(4(3(5(3(0(2(5(0(1(4(0(0(2(3(3(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(4(3(5(3(0(2(5(0(1(4(0(0(2(3(3(x0))))))))))))))))) → D(1(0(4(0(2(2(4(3(5(4(3(5(3(2(1(3(x0)))))))))))))))))
L(1(4(3(5(3(0(2(5(0(1(4(0(0(2(3(3(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(4(3(5(3(0(2(5(0(1(4(0(0(2(3(3(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(1(5(0(4(3(1(1(5(5(2(2(4(4(1(5(0(x0))))))))))))))))) → D(4(3(5(5(5(1(0(4(0(4(5(4(4(2(5(0(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(0(1(0(2(3(4(0(4(1(2(4(4(2(3(2(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(0(2(3(2(0(3(0(0(1(1(2(2(5(2(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(0(3(3(3(2(3(0(2(5(5(3(5(4(1(0(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(0(4(0(2(2(4(3(5(4(3(5(3(2(1(3(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(4(4(2(0(0(2(3(2(4(3(4(4(2(1(0(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(5(2(0(3(0(2(3(5(5(1(0(5(4(2(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(2(0(5(0(0(1(0(5(2(0(3(4(0(0(0(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(2(2(1(5(2(4(2(5(2(3(2(3(1(3(2(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(0(4(5(5(3(5(5(3(1(0(4(5(5(1(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(1(0(4(1(4(2(4(1(5(4(5(0(1(5(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(1(1(2(5(5(4(0(2(0(4(1(0(3(3(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(3(2(5(1(5(4(0(1(0(5(3(4(4(0(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(4(1(5(1(5(0(3(4(3(1(4(1(4(5(0(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(4(2(1(3(5(0(4(2(0(1(2(2(1(3(0(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(5(4(3(0(5(4(2(2(3(1(5(0(0(5(1(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(1(0(4(0(2(2(4(3(5(4(3(5(3(2(1(3(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(2(2(1(5(2(4(2(5(2(3(2(3(1(3(2(5(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(4(1(5(1(5(0(3(4(3(1(4(1(4(5(0(5(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(4(3(5(5(5(1(0(4(0(4(5(4(4(2(5(0(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(2(0(5(0(0(1(0(5(2(0(3(4(0(0(0(5(x0))))))))))))))))) → D(2(2(1(5(2(4(2(5(2(3(2(3(1(3(2(5(x0)))))))))))))))))
L(2(2(3(0(3(1(0(2(4(5(0(0(2(2(5(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(2(3(5(1(2(3(2(4(1(1(4(2(0(0(3(0(x0))))))))))))))))) → D(4(2(4(0(4(5(4(0(1(4(2(2(4(2(3(0(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(3(2(0(3(4(5(2(4(1(1(3(4(4(1(2(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(4(0(2(2(1(0(2(3(5(2(0(2(1(4(2(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(2(4(3(1(2(1(4(5(2(2(2(2(4(0(4(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(0(4(5(5(3(5(5(3(1(0(4(5(5(1(4(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(1(0(4(1(4(2(4(1(5(4(5(0(1(5(5(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(1(1(2(5(5(4(0(2(0(4(1(0(3(3(5(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(3(2(5(1(5(4(0(1(0(5(3(4(4(0(5(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(5(4(3(0(5(4(2(2(3(1(5(0(0(5(1(5(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(3(0(4(5(5(3(5(5(3(1(0(4(5(5(1(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(0(4(5(5(3(5(5(3(1(0(4(5(5(1(4(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(3(1(0(4(1(4(2(4(1(5(4(5(0(1(5(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(1(1(2(5(5(4(0(2(0(4(1(0(3(3(5(x0))))))))))))))))) → D(3(1(0(4(1(4(2(4(1(5(4(5(0(1(5(5(x0)))))))))))))))))
L(3(1(1(2(5(5(4(0(2(0(4(1(0(3(3(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(2(0(3(4(5(2(4(1(1(3(4(4(1(2(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(3(1(1(2(0(3(1(1(5(3(1(0(4(3(2(x0))))))))))))))))) → D(3(3(5(0(1(5(2(5(2(1(2(1(3(3(3(2(x0)))))))))))))))))
L(3(3(1(1(2(0(3(1(1(5(3(1(0(4(3(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(3(1(1(2(0(3(1(1(5(3(1(0(4(3(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(3(3(5(0(1(5(2(5(2(1(2(1(3(3(3(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(3(4(3(1(5(0(5(0(5(3(5(4(1(5(2(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(5(1(2(2(4(2(3(0(5(3(5(4(5(5(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(4(0(2(2(1(0(2(3(5(2(0(2(1(4(2(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(4(0(2(2(1(0(2(3(5(2(0(2(1(4(2(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(1(4(4(2(0(0(2(3(2(4(3(4(4(2(1(0(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(2(2(3(0(3(1(0(2(4(5(0(0(2(2(5(2(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(2(4(3(1(2(1(4(5(2(2(2(2(4(0(4(2(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(2(4(4(1(3(0(0(2(1(5(2(3(0(3(3(0(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(2(4(0(4(5(4(0(1(4(2(2(4(2(3(0(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(3(5(5(5(1(0(4(0(4(5(4(4(2(5(0(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(5(5(0(0(4(0(3(0(1(1(0(3(3(0(3(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(4(0(2(2(1(0(2(3(5(2(0(2(1(4(2(4(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(4(5(5(0(0(4(0(3(0(1(1(0(3(3(0(3(x0)))))))))))))))))
L(4(5(2(0(5(1(4(0(5(5(0(5(0(4(4(4(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(4(5(2(0(5(1(4(0(5(5(0(5(0(4(4(4(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(4(5(2(0(5(1(4(0(5(5(0(5(0(4(4(4(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(4(5(5(0(0(4(0(3(0(1(1(0(3(3(0(3(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(5(0(4(1(2(5(0(1(0(1(0(3(0(4(4(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(5(0(4(1(2(5(0(1(0(1(0(3(0(4(4(4(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(5(0(4(1(2(5(0(1(0(1(0(3(0(4(4(4(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(5(5(3(0(0(2(2(1(3(1(2(5(3(5(0(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(5(5(3(0(0(2(2(1(3(1(2(5(3(5(0(1(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(5(5(3(0(0(2(2(1(3(1(2(5(3(5(0(1(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
Y0(D(x0)) → D(0(x0))
Y1(D(x0)) → D(1(x0))
Y2(D(x0)) → D(2(x0))
Y3(D(x0)) → D(3(x0))
Y4(D(x0)) → D(4(x0))
Y5(D(x0)) → D(5(x0))
R(D(x0)) → B(x0)

Proof

1 Termination Assumption

We assume termination of the following TRS
B(x0) → W(M(M(M(M(M(M(M(M(M(M(M(M(M(M(M(V(x0)))))))))))))))))
M(x0) → x0
M(V(0(x0))) → V(X0(x0))
M(V(1(x0))) → V(X1(x0))
M(V(2(x0))) → V(X2(x0))
M(V(3(x0))) → V(X3(x0))
M(V(4(x0))) → V(X4(x0))
M(V(5(x0))) → V(X5(x0))
X0(0(x0)) → 0(X0(x0))
X0(1(x0)) → 1(X0(x0))
X0(2(x0)) → 2(X0(x0))
X0(3(x0)) → 3(X0(x0))
X0(4(x0)) → 4(X0(x0))
X0(5(x0)) → 5(X0(x0))
X1(0(x0)) → 0(X1(x0))
X1(1(x0)) → 1(X1(x0))
X1(2(x0)) → 2(X1(x0))
X1(3(x0)) → 3(X1(x0))
X1(4(x0)) → 4(X1(x0))
X1(5(x0)) → 5(X1(x0))
X2(0(x0)) → 0(X2(x0))
X2(1(x0)) → 1(X2(x0))
X2(2(x0)) → 2(X2(x0))
X2(3(x0)) → 3(X2(x0))
X2(4(x0)) → 4(X2(x0))
X2(5(x0)) → 5(X2(x0))
X3(0(x0)) → 0(X3(x0))
X3(1(x0)) → 1(X3(x0))
X3(2(x0)) → 2(X3(x0))
X3(3(x0)) → 3(X3(x0))
X3(4(x0)) → 4(X3(x0))
X3(5(x0)) → 5(X3(x0))
X4(0(x0)) → 0(X4(x0))
X4(1(x0)) → 1(X4(x0))
X4(2(x0)) → 2(X4(x0))
X4(3(x0)) → 3(X4(x0))
X4(4(x0)) → 4(X4(x0))
X4(5(x0)) → 5(X4(x0))
X5(0(x0)) → 0(X5(x0))
X5(1(x0)) → 1(X5(x0))
X5(2(x0)) → 2(X5(x0))
X5(3(x0)) → 3(X5(x0))
X5(4(x0)) → 4(X5(x0))
X5(5(x0)) → 5(X5(x0))
X0(E(x0)) → 0(E(x0))
X1(E(x0)) → 1(E(x0))
X2(E(x0)) → 2(E(x0))
X3(E(x0)) → 3(E(x0))
X4(E(x0)) → 4(E(x0))
X5(E(x0)) → 5(E(x0))
W(V(x0)) → R(L(x0))
L(0(x0)) → Y0(L(x0))
L(1(x0)) → Y1(L(x0))
L(2(x0)) → Y2(L(x0))
L(3(x0)) → Y3(L(x0))
L(4(x0)) → Y4(L(x0))
L(5(x0)) → Y5(L(x0))
L(0(0(1(0(2(3(4(0(4(1(2(4(4(2(3(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(0(1(5(0(3(0(4(2(3(1(5(0(5(2(1(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(0(1(5(0(3(0(4(2(3(1(5(0(5(2(1(x0))))))))))))))))) → D(0(3(5(2(2(1(1(4(5(4(0(1(5(4(2(1(x0)))))))))))))))))
L(0(0(1(5(0(3(0(4(2(3(1(5(0(5(2(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(0(2(3(2(0(3(0(0(1(1(2(2(5(2(5(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(0(0(1(0(2(3(4(0(4(1(2(4(4(2(3(2(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(0(1(4(3(4(3(4(3(4(0(4(0(2(1(1(2(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(1(2(1(5(3(4(1(0(0(1(4(2(0(0(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(0(1(4(3(4(3(4(3(4(0(4(0(2(1(1(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(1(4(3(4(3(4(3(4(0(4(0(2(1(1(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(2(3(2(2(4(2(2(1(0(2(1(4(0(3(4(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(0(3(5(3(3(2(2(2(3(0(4(0(4(1(0(1(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(0(3(5(3(3(2(2(2(3(0(4(0(4(1(0(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(0(0(3(3(3(2(3(0(2(5(5(3(5(4(1(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(1(4(4(2(0(0(2(3(2(4(3(4(4(2(1(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(1(5(0(4(3(1(1(5(5(2(2(4(4(1(5(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(1(5(2(0(3(0(2(3(5(5(1(0(5(4(2(5(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(2(2(1(5(2(4(2(5(2(3(2(3(1(3(2(5(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(2(3(5(1(2(3(2(4(1(1(4(2(0(0(3(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(2(4(4(1(3(0(0(2(1(5(2(3(0(3(3(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(4(1(0(5(2(0(2(1(0(0(5(0(3(4(0(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(4(2(4(0(4(5(4(0(1(4(2(2(4(2(3(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(4(3(5(5(5(1(0(4(0(4(5(4(4(2(5(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(5(2(4(5(3(5(0(3(4(1(2(0(3(3(2(0(x0)))))))))))))))))
L(1(1(0(4(0(1(4(3(1(2(1(0(4(1(1(0(x0))))))))))))))))) → D(5(5(2(5(2(4(2(3(0(0(2(0(0(4(2(0(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(0(1(0(2(3(4(0(4(1(2(4(4(2(3(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(1(4(3(4(3(4(3(4(0(4(0(2(1(1(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(1(4(4(2(0(0(2(3(2(4(3(4(4(2(1(0(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(2(4(3(1(2(1(4(5(2(2(2(2(4(0(4(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(2(0(1(3(2(3(1(3(1(1(3(0(4(3(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(0(3(5(2(2(1(1(4(5(4(0(1(5(4(2(1(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(0(3(5(3(3(2(2(2(3(0(4(0(4(1(0(1(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(1(2(2(5(1(4(2(2(5(3(2(5(3(3(3(1(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(1(4(3(5(3(0(2(5(0(1(4(0(0(2(3(3(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(4(3(5(3(0(2(5(0(1(4(0(0(2(3(3(x0))))))))))))))))) → D(1(0(4(0(2(2(4(3(5(4(3(5(3(2(1(3(x0)))))))))))))))))
L(1(4(3(5(3(0(2(5(0(1(4(0(0(2(3(3(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(4(3(5(3(0(2(5(0(1(4(0(0(2(3(3(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(1(5(0(4(3(1(1(5(5(2(2(4(4(1(5(0(x0))))))))))))))))) → D(4(3(5(5(5(1(0(4(0(4(5(4(4(2(5(0(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(0(1(0(2(3(4(0(4(1(2(4(4(2(3(2(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(0(2(3(2(0(3(0(0(1(1(2(2(5(2(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(0(3(3(3(2(3(0(2(5(5(3(5(4(1(0(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(0(4(0(2(2(4(3(5(4(3(5(3(2(1(3(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(4(4(2(0(0(2(3(2(4(3(4(4(2(1(0(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(1(5(2(0(3(0(2(3(5(5(1(0(5(4(2(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(2(0(5(0(0(1(0(5(2(0(3(4(0(0(0(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(2(2(1(5(2(4(2(5(2(3(2(3(1(3(2(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(0(4(5(5(3(5(5(3(1(0(4(5(5(1(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(1(0(4(1(4(2(4(1(5(4(5(0(1(5(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(1(1(2(5(5(4(0(2(0(4(1(0(3(3(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(3(2(5(1(5(4(0(1(0(5(3(4(4(0(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(4(1(5(1(5(0(3(4(3(1(4(1(4(5(0(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(4(2(1(3(5(0(4(2(0(1(2(2(1(3(0(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(5(4(3(0(5(4(2(2(3(1(5(0(0(5(1(5(x0)))))))))))))))))
L(1(5(1(1(5(0(2(1(1(5(0(4(1(0(0(5(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(1(0(4(0(2(2(4(3(5(4(3(5(3(2(1(3(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(2(2(1(5(2(4(2(5(2(3(2(3(1(3(2(5(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(4(1(5(1(5(0(3(4(3(1(4(1(4(5(0(5(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(4(3(5(5(5(1(0(4(0(4(5(4(4(2(5(0(x0)))))))))))))))))
L(2(0(1(0(3(4(0(4(1(3(2(5(1(1(1(5(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(2(0(5(0(0(1(0(5(2(0(3(4(0(0(0(5(x0))))))))))))))))) → D(2(2(1(5(2(4(2(5(2(3(2(3(1(3(2(5(x0)))))))))))))))))
L(2(2(3(0(3(1(0(2(4(5(0(0(2(2(5(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(2(3(5(1(2(3(2(4(1(1(4(2(0(0(3(0(x0))))))))))))))))) → D(4(2(4(0(4(5(4(0(1(4(2(2(4(2(3(0(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(1(0(0(1(4(5(2(0(3(3(3(5(0(1(4(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(2(0(2(0(4(1(0(1(3(2(2(1(3(5(5(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(3(2(0(3(4(5(2(4(1(1(3(4(4(1(2(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(4(0(2(2(1(0(2(3(5(2(0(2(1(4(2(4(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(2(4(1(1(1(5(4(2(5(1(0(0(5(2(5(4(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(2(4(3(1(2(1(4(5(2(2(2(2(4(0(4(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(0(4(5(5(3(5(5(3(1(0(4(5(5(1(4(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(1(0(4(1(4(2(4(1(5(4(5(0(1(5(5(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(1(1(2(5(5(4(0(2(0(4(1(0(3(3(5(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(3(2(5(1(5(4(0(1(0(5(3(4(4(0(5(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(5(4(3(0(5(4(2(2(3(1(5(0(0(5(1(5(x0)))))))))))))))))
L(3(0(4(1(2(0(0(1(0(2(3(1(0(5(1(5(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(3(0(4(5(5(3(5(5(3(1(0(4(5(5(1(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(0(4(5(5(3(5(5(3(1(0(4(5(5(1(4(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(3(1(0(4(1(4(2(4(1(5(4(5(0(1(5(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(1(1(2(5(5(4(0(2(0(4(1(0(3(3(5(x0))))))))))))))))) → D(3(1(0(4(1(4(2(4(1(5(4(5(0(1(5(5(x0)))))))))))))))))
L(3(1(1(2(5(5(4(0(2(0(4(1(0(3(3(5(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(2(0(3(4(5(2(4(1(1(3(4(4(1(2(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(3(1(1(2(0(3(1(1(5(3(1(0(4(3(2(x0))))))))))))))))) → D(3(3(5(0(1(5(2(5(2(1(2(1(3(3(3(2(x0)))))))))))))))))
L(3(3(1(1(2(0(3(1(1(5(3(1(0(4(3(2(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(3(1(1(2(0(3(1(1(5(3(1(0(4(3(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(3(3(5(0(1(5(2(5(2(1(2(1(3(3(3(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(3(4(3(1(5(0(5(0(5(3(5(4(1(5(2(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(3(5(1(2(2(4(2(3(0(5(3(5(4(5(5(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(4(0(2(2(1(0(2(3(5(2(0(2(1(4(2(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(4(0(2(2(1(0(2(3(5(2(0(2(1(4(2(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(0(3(1(3(0(4(5(4(1(5(4(5(4(2(1(4(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(0(4(2(0(4(0(2(5(5(3(3(0(4(4(5(2(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(1(4(4(2(0(0(2(3(2(4(3(4(4(2(1(0(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(2(2(3(0(3(1(0(2(4(5(0(0(2(2(5(2(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(2(4(3(1(2(1(4(5(2(2(2(2(4(0(4(2(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(2(4(3(2(3(0(4(0(4(0(4(3(2(2(3(2(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(2(4(4(1(3(0(0(2(1(5(2(3(0(3(3(0(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(2(4(0(4(5(4(0(1(4(2(2(4(2(3(0(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(3(5(5(5(1(0(4(0(4(5(4(4(2(5(0(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(4(5(5(0(0(4(0(3(0(1(1(0(3(3(0(3(x0)))))))))))))))))
L(4(1(2(3(2(2(1(5(5(3(1(1(0(5(5(2(x0))))))))))))))))) → D(5(4(1(4(5(5(2(2(0(0(3(5(5(5(4(2(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(0(5(2(0(2(2(5(4(2(4(1(4(2(4(5(4(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(1(3(2(3(4(4(5(4(5(2(5(2(4(4(0(4(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(4(0(2(2(1(0(2(3(5(2(0(2(1(4(2(4(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(4(1(5(4(5(5(1(1(2(0(1(0(1(2(5(4(x0))))))))))))))))) → D(4(5(5(0(0(4(0(3(0(1(1(0(3(3(0(3(x0)))))))))))))))))
L(4(5(2(0(5(1(4(0(5(5(0(5(0(4(4(4(x0))))))))))))))))) → D(2(4(3(2(5(4(0(4(2(3(4(5(0(5(2(1(x0)))))))))))))))))
L(4(5(2(0(5(1(4(0(5(5(0(5(0(4(4(4(x0))))))))))))))))) → D(4(2(2(5(1(3(5(2(2(0(3(0(3(4(4(1(x0)))))))))))))))))
L(4(5(2(0(5(1(4(0(5(5(0(5(0(4(4(4(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(4(5(5(0(0(4(0(3(0(1(1(0(3(3(0(3(x0))))))))))))))))) → D(4(3(2(1(4(0(0(0(0(3(2(2(1(5(3(3(x0)))))))))))))))))
L(5(0(4(1(2(5(0(1(0(1(0(3(0(4(4(4(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(5(0(4(1(2(5(0(1(0(1(0(3(0(4(4(4(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(5(0(4(1(2(5(0(1(0(1(0(3(0(4(4(4(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
L(5(5(3(0(0(2(2(1(3(1(2(5(3(5(0(1(x0))))))))))))))))) → D(3(4(4(5(0(4(2(5(3(4(4(5(3(5(2(4(x0)))))))))))))))))
L(5(5(3(0(0(2(2(1(3(1(2(5(3(5(0(1(x0))))))))))))))))) → D(5(0(0(4(3(3(0(0(1(3(3(5(0(2(4(4(x0)))))))))))))))))
L(5(5(3(0(0(2(2(1(3(1(2(5(3(5(0(1(x0))))))))))))))))) → D(5(4(5(5(5(2(5(1(2(3(4(5(4(4(1(4(x0)))))))))))))))))
Y0(D(x0)) → D(0(x0))
Y1(D(x0)) → D(1(x0))
Y2(D(x0)) → D(2(x0))
Y3(D(x0)) → D(3(x0))
Y4(D(x0)) → D(4(x0))
Y5(D(x0)) → D(5(x0))
R(D(x0)) → B(x0)