(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
0(q0(0(x1))) → 0(0(q0(x1)))
0(q0(1(x1))) → 0(1(q0(x1)))
1(q0(0(x1))) → 0(0(q1(x1)))
1(q0(1(x1))) → 0(1(q1(x1)))
1(q1(0(x1))) → 1(0(q1(x1)))
1(q1(1(x1))) → 1(1(q1(x1)))
0(q1(0(x1))) → 0(0(q2(x1)))
0(q1(1(x1))) → 0(1(q2(x1)))
1(q2(0(x1))) → 1(0(q2(x1)))
1(q2(1(x1))) → 1(1(q2(x1)))
0(q2(x1)) → q3(1(x1))
1(q3(x1)) → q3(1(x1))
0(q3(x1)) → q4(0(x1))
1(q4(x1)) → q4(1(x1))
0(q4(0(x1))) → 1(0(q5(x1)))
0(q4(1(x1))) → 1(1(q5(x1)))
1(q5(0(x1))) → 0(0(q1(x1)))
1(q5(1(x1))) → 0(1(q1(x1)))
0(q5(x1)) → q6(0(x1))
1(q6(x1)) → q6(1(x1))
1(q7(0(x1))) → 0(0(q8(x1)))
1(q7(1(x1))) → 0(1(q8(x1)))
0(q8(x1)) → 0(q0(x1))
1(q8(0(x1))) → 1(0(q8(x1)))
1(q8(1(x1))) → 1(1(q8(x1)))
0(q6(x1)) → q9(0(x1))
0(q9(0(x1))) → 1(0(q7(x1)))
0(q9(1(x1))) → 1(1(q7(x1)))
1(q9(x1)) → q9(1(x1))
h(q0(x1)) → h(0(q0(x1)))
q0(h(x1)) → q0(0(h(x1)))
h(q1(x1)) → h(0(q1(x1)))
q1(h(x1)) → q1(0(h(x1)))
h(q2(x1)) → h(0(q2(x1)))
q2(h(x1)) → q2(0(h(x1)))
h(q3(x1)) → h(0(q3(x1)))
q3(h(x1)) → q3(0(h(x1)))
h(q4(x1)) → h(0(q4(x1)))
q4(h(x1)) → q4(0(h(x1)))
h(q5(x1)) → h(0(q5(x1)))
q5(h(x1)) → q5(0(h(x1)))
h(q6(x1)) → h(0(q6(x1)))
q6(h(x1)) → q6(0(h(x1)))
Q is empty.
(1) QTRS Reverse (EQUIVALENT transformation)
We applied the QTRS Reverse Processor [REVERSE].
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
0(q0(0(x))) → q0(0(0(x)))
1(q0(0(x))) → q0(1(0(x)))
0(q0(1(x))) → q1(0(0(x)))
1(q0(1(x))) → q1(1(0(x)))
0(q1(1(x))) → q1(0(1(x)))
1(q1(1(x))) → q1(1(1(x)))
0(q1(0(x))) → q2(0(0(x)))
1(q1(0(x))) → q2(1(0(x)))
0(q2(1(x))) → q2(0(1(x)))
1(q2(1(x))) → q2(1(1(x)))
q2(0(x)) → 1(q3(x))
q3(1(x)) → 1(q3(x))
q3(0(x)) → 0(q4(x))
q4(1(x)) → 1(q4(x))
0(q4(0(x))) → q5(0(1(x)))
1(q4(0(x))) → q5(1(1(x)))
0(q5(1(x))) → q1(0(0(x)))
1(q5(1(x))) → q1(1(0(x)))
q5(0(x)) → 0(q6(x))
q6(1(x)) → 1(q6(x))
0(q7(1(x))) → q8(0(0(x)))
1(q7(1(x))) → q8(1(0(x)))
q8(0(x)) → q0(0(x))
0(q8(1(x))) → q8(0(1(x)))
1(q8(1(x))) → q8(1(1(x)))
q6(0(x)) → 0(q9(x))
0(q9(0(x))) → q7(0(1(x)))
1(q9(0(x))) → q7(1(1(x)))
q9(1(x)) → 1(q9(x))
q0(h(x)) → q0(0(h(x)))
h(q0(x)) → h(0(q0(x)))
q1(h(x)) → q1(0(h(x)))
h(q1(x)) → h(0(q1(x)))
q2(h(x)) → q2(0(h(x)))
h(q2(x)) → h(0(q2(x)))
q3(h(x)) → q3(0(h(x)))
h(q3(x)) → h(0(q3(x)))
q4(h(x)) → q4(0(h(x)))
h(q4(x)) → h(0(q4(x)))
q5(h(x)) → q5(0(h(x)))
h(q5(x)) → h(0(q5(x)))
q6(h(x)) → q6(0(h(x)))
h(q6(x)) → h(0(q6(x)))
Q is empty.
(3) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [OPPELT08] to show that the SRS problem is infinite.
Found the self-embedding DerivationStructure:
h q0 0 → h q0 0 0
h q0 0 →
h q0 0 0by OverlapClosure OC 2
h q0 → h 0 q0
by original rule (OC 1)
0 q0 0 → q0 0 0
by original rule (OC 1)
(4) NO