(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(x) → f(f(x))
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:
f(x) → f(f(x))
Q is empty.
(3) QTRS Reverse (EQUIVALENT transformation)
We applied the QTRS Reverse Processor [REVERSE].
(4) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(x) → f(f(x))
Q is empty.
(5) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(6) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
f(x) → f(f(x))
The set Q consists of the following terms:
f(x0)
(7) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(x) → F(f(x))
F(x) → F(x)
The TRS R consists of the following rules:
f(x) → f(f(x))
The set Q consists of the following terms:
f(x0)
We have to consider all minimal (P,Q,R)-chains.
(9) MNOCProof (EQUIVALENT transformation)
We use the modular non-overlap check [FROCOS05] to decrease Q to the empty set.
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(x) → F(f(x))
F(x) → F(x)
The TRS R consists of the following rules:
f(x) → f(f(x))
Q is empty.
We have to consider all (P,Q,R)-chains.
(11) NonTerminationProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by semiunifying a rule from P directly.
s =
F(
x) evaluates to t =
F(
f(
x))
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Semiunifier: [ ]
- Matcher: [x / f(x)]
Rewriting sequenceThe DP semiunifies directly so there is only one rewrite step from F(x) to F(f(x)).
(12) FALSE