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

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

0 QTRS
↳1 NonTerminationProof (⇒, 1141 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(1(x))) → V(X1(x))
M(V(q0(x))) → V(Xq0(x))
M(V(0(x))) → V(X0(x))
M(V(q1(x))) → V(Xq1(x))
M(V(q2(x))) → V(Xq2(x))
X1(1(x)) → 1(X1(x))
X1(q0(x)) → q0(X1(x))
X1(0(x)) → 0(X1(x))
X1(q1(x)) → q1(X1(x))
X1(q2(x)) → q2(X1(x))
Xq0(1(x)) → 1(Xq0(x))
Xq0(q0(x)) → q0(Xq0(x))
Xq0(0(x)) → 0(Xq0(x))
Xq0(q1(x)) → q1(Xq0(x))
Xq0(q2(x)) → q2(Xq0(x))
X0(1(x)) → 1(X0(x))
X0(q0(x)) → q0(X0(x))
X0(0(x)) → 0(X0(x))
X0(q1(x)) → q1(X0(x))
X0(q2(x)) → q2(X0(x))
Xq1(1(x)) → 1(Xq1(x))
Xq1(q0(x)) → q0(Xq1(x))
Xq1(0(x)) → 0(Xq1(x))
Xq1(q1(x)) → q1(Xq1(x))
Xq1(q2(x)) → q2(Xq1(x))
Xq2(1(x)) → 1(Xq2(x))
Xq2(q0(x)) → q0(Xq2(x))
Xq2(0(x)) → 0(Xq2(x))
Xq2(q1(x)) → q1(Xq2(x))
Xq2(q2(x)) → q2(Xq2(x))
X1(E(x)) → 1(E(x))
Xq0(E(x)) → q0(E(x))
X0(E(x)) → 0(E(x))
Xq1(E(x)) → q1(E(x))
Xq2(E(x)) → q2(E(x))
W(V(x)) → R(L(x))
L(1(x)) → Y1(L(x))
L(q0(x)) → Yq0(L(x))
L(0(x)) → Y0(L(x))
L(q1(x)) → Yq1(L(x))
L(q2(x)) → Yq2(L(x))
L(1(q0(1(x)))) → D(0(1(q1(x))))
L(1(q0(0(x)))) → D(0(0(q1(x))))
L(1(q1(1(x)))) → D(1(1(q1(x))))
L(1(q1(0(x)))) → D(1(0(q1(x))))
L(0(q1(x))) → D(q2(1(x)))
L(1(q2(x))) → D(q2(1(x)))
L(0(q2(x))) → D(0(q0(x)))
Y1(D(x)) → D(1(x))
Yq0(D(x)) → D(q0(x))
Y0(D(x)) → D(0(x))
Yq1(D(x)) → D(q1(x))
Yq2(D(x)) → D(q2(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 1 q2 E → W V 1 q2 E

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

(2) NO