(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
h(f(x, y)) → f(f(a, h(h(y))), x)
Q is empty.
(1) Overlay + Local Confluence (EQUIVALENT transformation)
The TRS is overlay and locally confluent. By [NOC] we can switch to innermost.
(2) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
h(f(x, y)) → f(f(a, h(h(y))), x)
The set Q consists of the following terms:
h(f(x0, x1))
(3) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(4) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(f(x, y)) → H(h(y))
H(f(x, y)) → H(y)
The TRS R consists of the following rules:
h(f(x, y)) → f(f(a, h(h(y))), x)
The set Q consists of the following terms:
h(f(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(5) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
H(
f(
x,
y)) →
H(
h(
y)) at position [0] we obtained the following new rules [LPAR04]:
H(f(y0, f(x0, x1))) → H(f(f(a, h(h(x1))), x0)) → H(f(y0, f(x0, x1))) → H(f(f(a, h(h(x1))), x0))
(6) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(f(x, y)) → H(y)
H(f(y0, f(x0, x1))) → H(f(f(a, h(h(x1))), x0))
The TRS R consists of the following rules:
h(f(x, y)) → f(f(a, h(h(y))), x)
The set Q consists of the following terms:
h(f(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(7) TransformationProof (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
H(
f(
x,
y)) →
H(
y) we obtained the following new rules [LPAR04]:
H(f(x0, f(y_0, y_1))) → H(f(y_0, y_1)) → H(f(x0, f(y_0, y_1))) → H(f(y_0, y_1))
H(f(x0, f(y_0, f(y_1, y_2)))) → H(f(y_0, f(y_1, y_2))) → H(f(x0, f(y_0, f(y_1, y_2)))) → H(f(y_0, f(y_1, y_2)))
(8) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(f(y0, f(x0, x1))) → H(f(f(a, h(h(x1))), x0))
H(f(x0, f(y_0, y_1))) → H(f(y_0, y_1))
H(f(x0, f(y_0, f(y_1, y_2)))) → H(f(y_0, f(y_1, y_2)))
The TRS R consists of the following rules:
h(f(x, y)) → f(f(a, h(h(y))), x)
The set Q consists of the following terms:
h(f(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(9) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
H(f(y0, f(x0, x1))) → H(f(f(a, h(h(x1))), x0))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
POL(f(x1, x2)) = | | + | / | 3A | 2A | 0A | \ |
| | -I | 0A | -I | | |
\ | -I | 0A | -I | / |
| · | x1 | + | / | -I | 2A | -I | \ |
| | -I | 0A | -I | | |
\ | 3A | 2A | 0A | / |
| · | x2 |
POL(h(x1)) = | | + | / | -I | 0A | 3A | \ |
| | -I | 0A | -I | | |
\ | 0A | -I | -I | / |
| · | x1 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
h(f(x, y)) → f(f(a, h(h(y))), x)
(10) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(f(x0, f(y_0, y_1))) → H(f(y_0, y_1))
H(f(x0, f(y_0, f(y_1, y_2)))) → H(f(y_0, f(y_1, y_2)))
The TRS R consists of the following rules:
h(f(x, y)) → f(f(a, h(h(y))), x)
The set Q consists of the following terms:
h(f(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(11) UsableRulesProof (EQUIVALENT transformation)
As all Q-normal forms are R-normal forms we are in the innermost case. Hence, by the usable rules processor [LPAR04] we can delete all non-usable rules [FROCOS05] from R.
(12) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(f(x0, f(y_0, y_1))) → H(f(y_0, y_1))
H(f(x0, f(y_0, f(y_1, y_2)))) → H(f(y_0, f(y_1, y_2)))
R is empty.
The set Q consists of the following terms:
h(f(x0, x1))
We have to consider all minimal (P,Q,R)-chains.
(13) QReductionProof (EQUIVALENT transformation)
We deleted the following terms from Q as each root-symbol of these terms does neither occur in P nor in R.[THIEMANN].
h(f(x0, x1))
(14) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(f(x0, f(y_0, y_1))) → H(f(y_0, y_1))
H(f(x0, f(y_0, f(y_1, y_2)))) → H(f(y_0, f(y_1, y_2)))
R is empty.
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(15) QDPSizeChangeProof (EQUIVALENT transformation)
By using the subterm criterion [SUBTERM_CRITERION] together with the size-change analysis [AAECC05] we have proven that there are no infinite chains for this DP problem.
From the DPs we obtained the following set of size-change graphs:
- H(f(x0, f(y_0, y_1))) → H(f(y_0, y_1))
The graph contains the following edges 1 > 1
- H(f(x0, f(y_0, f(y_1, y_2)))) → H(f(y_0, f(y_1, y_2)))
The graph contains the following edges 1 > 1
(16) YES