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

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

0 QTRS
↳1 NonTerminationProof (⇒, 245 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(a(x))) → V(Xa(x))
M(V(p(x))) → V(Xp(x))
M(V(A(x))) → V(XA(x))
Xa(a(x)) → a(Xa(x))
Xa(p(x)) → p(Xa(x))
Xa(A(x)) → A(Xa(x))
Xp(a(x)) → a(Xp(x))
Xp(p(x)) → p(Xp(x))
Xp(A(x)) → A(Xp(x))
XA(a(x)) → a(XA(x))
XA(p(x)) → p(XA(x))
XA(A(x)) → A(XA(x))
Xa(E(x)) → a(E(x))
Xp(E(x)) → p(E(x))
XA(E(x)) → A(E(x))
W(V(x)) → R(L(x))
L(a(x)) → Ya(L(x))
L(p(x)) → Yp(L(x))
L(A(x)) → YA(L(x))
L(a(p(x))) → D(p(a(A(x))))
L(a(A(x))) → D(A(a(x)))
L(p(A(A(x)))) → D(a(p(x)))
Ya(D(x)) → D(a(x))
Yp(D(x)) → D(p(x))
YA(D(x)) → D(A(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 a A E → W V a A E

W V a A E → W V a A E
by OverlapClosure OC 3
W V a A E → W M V a A E
by OverlapClosure OC 2
W V a A → W M V a XA
by OverlapClosure OC 2
W V a A → W M V XA a
by OverlapClosure OC 3
W V a A → B A a
by OverlapClosure OC 3
W V a A → R D A a
by OverlapClosure OC 2
W V → R L
by original rule (OC 1)
L a A → D A a
by original rule (OC 1)
R D → B
by original rule (OC 1)
B A → W M V XA
by OverlapClosure OC 2
B → W M M V
by original rule (OC 1)
M V A → V XA
by original rule (OC 1)
XA a → a XA
by original rule (OC 1)
XA E → A E
by original rule (OC 1)
M →
by original rule (OC 1)

(2) NO