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

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

0 QTRS
↳1 NonTerminationProof (⇒, 849 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(0(x))) → V(X0(x))
M(V(*(x))) → V(X*(x))
M(V(1(x))) → V(X1(x))
M(V(#(x))) → V(X#(x))
M(V($(x))) → V(X$(x))
X0(0(x)) → 0(X0(x))
X0(*(x)) → *(X0(x))
X0(1(x)) → 1(X0(x))
X0(#(x)) → #(X0(x))
X0($(x)) → $(X0(x))
X*(0(x)) → 0(X*(x))
X*(*(x)) → *(X*(x))
X*(1(x)) → 1(X*(x))
X*(#(x)) → #(X*(x))
X*($(x)) → $(X*(x))
X1(0(x)) → 0(X1(x))
X1(*(x)) → *(X1(x))
X1(1(x)) → 1(X1(x))
X1(#(x)) → #(X1(x))
X1($(x)) → $(X1(x))
X#(0(x)) → 0(X#(x))
X#(*(x)) → *(X#(x))
X#(1(x)) → 1(X#(x))
X#(#(x)) → #(X#(x))
X#($(x)) → $(X#(x))
X$(0(x)) → 0(X$(x))
X$(*(x)) → *(X$(x))
X$(1(x)) → 1(X$(x))
X$(#(x)) → #(X$(x))
X$($(x)) → $(X$(x))
X0(E(x)) → 0(E(x))
X*(E(x)) → *(E(x))
X1(E(x)) → 1(E(x))
X#(E(x)) → #(E(x))
X$(E(x)) → $(E(x))
W(V(x)) → R(L(x))
L(0(x)) → Y0(L(x))
L(*(x)) → Y*(L(x))
L(1(x)) → Y1(L(x))
L(#(x)) → Y#(L(x))
L($(x)) → Y$(L(x))
L(0(*(x))) → D(*(1(x)))
L(1(*(x))) → D(0(#(x)))
L(#(0(x))) → D(0(#(x)))
L(#(1(x))) → D(1(#(x)))
L(#($(x))) → D(*($(x)))
L(#(#(x))) → D(#(x))
L(#(*(x))) → D(*(x))
Y0(D(x)) → D(0(x))
Y*(D(x)) → D(*(x))
Y1(D(x)) → D(1(x))
Y#(D(x)) → D(#(x))
Y$(D(x)) → D($(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 1 # E → B 1 # E

B 1 # E → B 1 # E
by OverlapClosure OC 3
B 1 # E → R D 1 # E
by OverlapClosure OC 3
B 1 # E → R L # 1 E
by OverlapClosure OC 2
B 1 # → R L # X1
by OverlapClosure OC 2
B 1 → R L X1
by OverlapClosure OC 3
B 1 → W V X1
by OverlapClosure OC 2
B → W M V
by original rule (OC 1)
M V 1 → V X1
by original rule (OC 1)
W V → R L
by original rule (OC 1)
X1 # → # X1
by original rule (OC 1)
X1 E → 1 E
by original rule (OC 1)
L # 1 → D 1 #
by original rule (OC 1)
R D → B
by original rule (OC 1)

(2) NO