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

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

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

(0) Obligation:

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

B(x) → W(M(V(x)))
M(x) → x
M(V(t(x))) → V(Xt(x))
M(V(f(x))) → V(Xf(x))
M(V(c(x))) → V(Xc(x))
M(V(n(x))) → V(Xn(x))
M(V(o(x))) → V(Xo(x))
M(V(s(x))) → V(Xs(x))
Xt(t(x)) → t(Xt(x))
Xt(f(x)) → f(Xt(x))
Xt(c(x)) → c(Xt(x))
Xt(n(x)) → n(Xt(x))
Xt(o(x)) → o(Xt(x))
Xt(s(x)) → s(Xt(x))
Xf(t(x)) → t(Xf(x))
Xf(f(x)) → f(Xf(x))
Xf(c(x)) → c(Xf(x))
Xf(n(x)) → n(Xf(x))
Xf(o(x)) → o(Xf(x))
Xf(s(x)) → s(Xf(x))
Xc(t(x)) → t(Xc(x))
Xc(f(x)) → f(Xc(x))
Xc(c(x)) → c(Xc(x))
Xc(n(x)) → n(Xc(x))
Xc(o(x)) → o(Xc(x))
Xc(s(x)) → s(Xc(x))
Xn(t(x)) → t(Xn(x))
Xn(f(x)) → f(Xn(x))
Xn(c(x)) → c(Xn(x))
Xn(n(x)) → n(Xn(x))
Xn(o(x)) → o(Xn(x))
Xn(s(x)) → s(Xn(x))
Xo(t(x)) → t(Xo(x))
Xo(f(x)) → f(Xo(x))
Xo(c(x)) → c(Xo(x))
Xo(n(x)) → n(Xo(x))
Xo(o(x)) → o(Xo(x))
Xo(s(x)) → s(Xo(x))
Xs(t(x)) → t(Xs(x))
Xs(f(x)) → f(Xs(x))
Xs(c(x)) → c(Xs(x))
Xs(n(x)) → n(Xs(x))
Xs(o(x)) → o(Xs(x))
Xs(s(x)) → s(Xs(x))
Xt(E(x)) → t(E(x))
Xf(E(x)) → f(E(x))
Xc(E(x)) → c(E(x))
Xn(E(x)) → n(E(x))
Xo(E(x)) → o(E(x))
Xs(E(x)) → s(E(x))
W(V(x)) → R(L(x))
L(t(x)) → Yt(L(x))
L(f(x)) → Yf(L(x))
L(c(x)) → Yc(L(x))
L(n(x)) → Yn(L(x))
L(o(x)) → Yo(L(x))
L(s(x)) → Ys(L(x))
L(t(f(x))) → D(t(c(n(x))))
L(n(f(x))) → D(f(n(x)))
L(o(f(x))) → D(f(o(x)))
L(n(s(x))) → D(f(s(x)))
L(o(s(x))) → D(f(s(x)))
L(c(f(x))) → D(f(c(x)))
L(c(n(x))) → D(n(c(x)))
L(c(o(x))) → D(o(c(x)))
L(c(o(x))) → D(o(x))
Yt(D(x)) → D(t(x))
Yf(D(x)) → D(f(x))
Yc(D(x)) → D(c(x))
Yn(D(x)) → D(n(x))
Yo(D(x)) → D(o(x))
Ys(D(x)) → D(s(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:
B o c E → B o c E

B o c E → B o c E
by OverlapClosure OC 3
B o c E → R D o c E
by OverlapClosure OC 3
B o c E → R L c o E
by OverlapClosure OC 2
B o c → R L c Xo
by OverlapClosure OC 2
B o → R L Xo
by OverlapClosure OC 3
B o → W V Xo
by OverlapClosure OC 2
B → W M V
by original rule (OC 1)
M V o → V Xo
by original rule (OC 1)
W V → R L
by original rule (OC 1)
Xo c → c Xo
by original rule (OC 1)
Xo E → o E
by original rule (OC 1)
L c o → D o c
by original rule (OC 1)
R D → B
by original rule (OC 1)

(2) NO