(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
0(0(0(0(x1)))) → 0(1(0(1(x1))))
1(0(0(1(x1)))) → 0(1(0(0(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(0(0(0(x)))) → 1(0(1(0(x))))
1(0(0(1(x)))) → 0(0(1(0(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:
1 0 0 1 0 1 0 1 0 1 0 1 0 1 0 → 1 0 0 1 0 1 0 1 0 1 0 1 0 1 0
1 0 0 1 0 1 0 1 0 1 0 1 0 1 0 →
1 0 0 1 0 1 0 1 0 1 0 1 0 1 0by OverlapClosure OC 2
1 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 0 0 1 0 1 0 1 0 1 0 0 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 0 0 1 0 0 0 0 0 1 0 0 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 0 0 1 0 0 0 1 0 0 1 0 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 0 0 1 0 0 1 0 0 1 0 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 1 0 0 1 0 1 0 0 1 0 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 1 0 0 0 0 0 0 0 1 0 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 1 0 0 0 0 0 1 0 0 1 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 1 0 0 0 1 0 0 1 0 1 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 1 0 1 0 0 1 0 1 0 1 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 1 0 1 0 0 0 0 0 0 1 0 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 1 0 1 0 0 0 0 1 0 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 1 0 1 0 0 1 0 0 1 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 0 0 0 0 0 1 0 0 1 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 0 0 0 1 0 0 1 0 1 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 0 1 → 1 1 0 0 0 1 0 0 0 0 0 0 1 0
by OverlapClosure OC 21 0 0 1 0 1 0 1 0 1 0 1 → 1 1 0 0 0 1 0 0 0 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 → 1 1 0 1 0 0 1 0 0 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 → 1 0 0 0 0 0 1 0 0 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 → 1 0 0 0 1 0 0 1 0 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 0 1 0 1 → 1 0 1 0 0 1 0 1 0 0 1 0
by OverlapClosure OC 21 0 0 1 0 1 → 1 0 1 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 → 0 0 0 0 1 0
by OverlapClosure OC 21 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
1 0 0 1 0 1 0 1 → 0 1 0 1 0 0 1 0
by OverlapClosure OC 31 0 0 1 0 1 0 1 → 0 0 0 0 0 0 1 0
by OverlapClosure OC 21 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 0 1 → 0 0 0 0 1 0
by OverlapClosure OC 21 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
1 0 0 1 → 0 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
0 0 0 0 → 1 0 1 0
by original rule (OC 1)
(4) NO