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

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

0 QTRS
↳1 NonTerminationProof (⇒, 1455 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(1(x))) → V(X1(x))
M(V(0(x))) → V(X0(x))
X1(1(x)) → 1(X1(x))
X1(0(x)) → 0(X1(x))
X0(1(x)) → 1(X0(x))
X0(0(x)) → 0(X0(x))
X1(E(x)) → 1(E(x))
X0(E(x)) → 0(E(x))
W(V(x)) → R(L(x))
L(1(x)) → Y1(L(x))
L(0(x)) → Y0(L(x))
L(1(0(x))) → D(0(0(0(1(x)))))
L(0(1(x))) → D(1(x))
L(1(1(x))) → D(0(0(0(0(x)))))
L(0(0(x))) → D(0(x))
Y1(D(x)) → D(1(x))
Y0(D(x)) → D(0(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 0 E → W V 1 0 E

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

(2) NO