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

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

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

(0) Obligation:

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

B(x1) → W(M(M(V(x1))))
M(x1) → x1
M(V(a(x1))) → V(Xa(x1))
M(V(b(x1))) → V(Xb(x1))
M(V(P(x1))) → V(XP(x1))
M(V(x(x1))) → V(Xx(x1))
M(V(Q(x1))) → V(XQ(x1))
Xa(a(x1)) → a(Xa(x1))
Xa(b(x1)) → b(Xa(x1))
Xa(P(x1)) → P(Xa(x1))
Xa(x(x1)) → x(Xa(x1))
Xa(Q(x1)) → Q(Xa(x1))
Xb(a(x1)) → a(Xb(x1))
Xb(b(x1)) → b(Xb(x1))
Xb(P(x1)) → P(Xb(x1))
Xb(x(x1)) → x(Xb(x1))
Xb(Q(x1)) → Q(Xb(x1))
XP(a(x1)) → a(XP(x1))
XP(b(x1)) → b(XP(x1))
XP(P(x1)) → P(XP(x1))
XP(x(x1)) → x(XP(x1))
XP(Q(x1)) → Q(XP(x1))
Xx(a(x1)) → a(Xx(x1))
Xx(b(x1)) → b(Xx(x1))
Xx(P(x1)) → P(Xx(x1))
Xx(x(x1)) → x(Xx(x1))
Xx(Q(x1)) → Q(Xx(x1))
XQ(a(x1)) → a(XQ(x1))
XQ(b(x1)) → b(XQ(x1))
XQ(P(x1)) → P(XQ(x1))
XQ(x(x1)) → x(XQ(x1))
XQ(Q(x1)) → Q(XQ(x1))
Xa(E(x1)) → a(E(x1))
Xb(E(x1)) → b(E(x1))
XP(E(x1)) → P(E(x1))
Xx(E(x1)) → x(E(x1))
XQ(E(x1)) → Q(E(x1))
W(V(x1)) → R(L(x1))
L(a(x1)) → Ya(L(x1))
L(b(x1)) → Yb(L(x1))
L(P(x1)) → YP(L(x1))
L(x(x1)) → Yx(L(x1))
L(Q(x1)) → YQ(L(x1))
L(a(b(b(x1)))) → D(P(a(b(x1))))
L(a(P(x1))) → D(P(a(x(x1))))
L(a(x(x1))) → D(x(a(x1)))
L(b(P(x1))) → D(b(Q(x1)))
L(Q(x(x1))) → D(a(Q(x1)))
L(Q(a(x1))) → D(b(b(a(x1))))
Ya(D(x1)) → D(a(x1))
Yb(D(x1)) → D(b(x1))
YP(D(x1)) → D(P(x1))
Yx(D(x1)) → D(x(x1))
YQ(D(x1)) → D(Q(x1))
R(D(x1)) → B(x1)

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 x E → W V a x E

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

(2) NO