NO Termination w.r.t. Q proof of /home/cern_httpd/provide/research/cycsrs/tpdb/TPDB-d9b80194f163/SRS_Standard/Zantema_04/z090-shift.srs

Termination w.r.t. Q of the given QTRS could be disproven:

0 QTRS
↳1 NonTerminationProof (⇒, 645 ms)
↳2 NO

(0) Obligation:

Q restricted rewrite system:
The TRS R consists of the following rules:

B(x) → W(M(M(V(x))))
M(x) → x
M(V(s(x))) → V(Xs(x))
M(V(b(x))) → V(Xb(x))
M(V(t(x))) → V(Xt(x))
M(V(u(x))) → V(Xu(x))
Xs(s(x)) → s(Xs(x))
Xs(b(x)) → b(Xs(x))
Xs(t(x)) → t(Xs(x))
Xs(u(x)) → u(Xs(x))
Xb(s(x)) → s(Xb(x))
Xb(b(x)) → b(Xb(x))
Xb(t(x)) → t(Xb(x))
Xb(u(x)) → u(Xb(x))
Xt(s(x)) → s(Xt(x))
Xt(b(x)) → b(Xt(x))
Xt(t(x)) → t(Xt(x))
Xt(u(x)) → u(Xt(x))
Xu(s(x)) → s(Xu(x))
Xu(b(x)) → b(Xu(x))
Xu(t(x)) → t(Xu(x))
Xu(u(x)) → u(Xu(x))
Xs(E(x)) → s(E(x))
Xb(E(x)) → b(E(x))
Xt(E(x)) → t(E(x))
Xu(E(x)) → u(E(x))
W(V(x)) → R(L(x))
L(s(x)) → Ys(L(x))
L(b(x)) → Yb(L(x))
L(t(x)) → Yt(L(x))
L(u(x)) → Yu(L(x))
L(s(b(x))) → D(b(s(s(s(x)))))
L(s(b(s(x)))) → D(b(t(x)))
L(t(b(x))) → D(b(s(x)))
L(t(b(s(x)))) → D(u(t(b(x))))
L(b(u(x))) → D(b(s(x)))
L(t(s(x))) → D(t(t(x)))
L(t(u(x))) → D(u(t(x)))
L(s(u(x))) → D(s(s(x)))
Ys(D(x)) → D(s(x))
Yb(D(x)) → D(b(x))
Yt(D(x)) → D(t(x))
Yu(D(x)) → D(u(x))
R(D(x)) → B(x)

Q is empty.

(1) NonTerminationProof (COMPLETE transformation)

We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.

Found the self-embedding DerivationStructure:
W V t u E → W V t u E

W V t u E → W V t u E
by OverlapClosure OC 3
W V t u E → W M V t u E
by OverlapClosure OC 2
W V t u → W M V t Xu
by OverlapClosure OC 2
W V t u → W M V Xu t
by OverlapClosure OC 3
W V t u → B u t
by OverlapClosure OC 3
W V t u → R D u t
by OverlapClosure OC 2
W V → R L
by original rule (OC 1)
L t u → D u t
by original rule (OC 1)
R D → B
by original rule (OC 1)
B u → W M V Xu
by OverlapClosure OC 2
B → W M M V
by original rule (OC 1)
M V u → V Xu
by original rule (OC 1)
Xu t → t Xu
by original rule (OC 1)
Xu E → u E
by original rule (OC 1)
M →
by original rule (OC 1)

(2) NO