(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(0, 1, x) → F(x, x, x)
The TRS R consists of the following rules:
f(0, 1, x) → f(x, x, x)
f(x, y, z) → 2
0 → 2
1 → 2
g(x, x, y) → y
g(x, y, y) → x
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) NonTerminationLoopProof (EQUIVALENT transformation)
We used the non-termination processor [FROCOS05] to show that the DP problem is infinite.
Found a loop by narrowing to the left:
s =
F(
g(
1,
0,
0),
g(
1,
y,
y),
x) evaluates to t =
F(
x,
x,
x)
Thus s starts an infinite chain as s semiunifies with t with the following substitutions:
- Matcher: [ ]
- Semiunifier: [y / 0, x / g(1, 0, 0)]
Rewriting sequenceF(g(1, 0, 0), g(1, 0, 0), g(1, 0, 0)) →
F(
g(
1,
0,
0),
1,
g(
1,
0,
0))
with rule
g(
x',
y,
y) →
x' at position [1] and matcher [
x' /
1,
y /
0]
F(g(1, 0, 0), 1, g(1, 0, 0)) →
F(
g(
1,
2,
0),
1,
g(
1,
0,
0))
with rule
0 →
2 at position [0,1] and matcher [ ]
F(g(1, 2, 0), 1, g(1, 0, 0)) →
F(
g(
2,
2,
0),
1,
g(
1,
0,
0))
with rule
1 →
2 at position [0,0] and matcher [ ]
F(g(2, 2, 0), 1, g(1, 0, 0)) →
F(
0,
1,
g(
1,
0,
0))
with rule
g(
x',
x',
y) →
y at position [0] and matcher [
x' /
2,
y /
0]
F(0, 1, g(1, 0, 0)) →
F(
g(
1,
0,
0),
g(
1,
0,
0),
g(
1,
0,
0))
with rule
F(
0,
1,
x) →
F(
x,
x,
x)
Now applying the matcher to the start term leads to a term which is equal to the last term in the rewriting sequence
All these steps are and every following step will be a correct step w.r.t to Q.