(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
i(x, x) → i(a, b)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
(1) DependencyPairsProof (EQUIVALENT transformation)
Using Dependency Pairs [AG00,LPAR04] we result in the following initial DP problem.
(2) Obligation:
Q DP problem:
The TRS P consists of the following rules:
I(x, x) → I(a, b)
G(x, x) → G(a, b)
H(s(f(x))) → H(f(x))
F(s(x)) → F(h(s(x)))
F(s(x)) → H(s(x))
F(g(s(x), y)) → F(g(x, s(y)))
F(g(s(x), y)) → G(x, s(y))
H(g(x, s(y))) → H(g(s(x), y))
H(g(x, s(y))) → G(s(x), y)
H(i(x, y)) → I(i(c, h(h(y))), x)
H(i(x, y)) → I(c, h(h(y)))
H(i(x, y)) → H(h(y))
H(i(x, y)) → H(y)
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(a, g(a, g(x, g(b, g(b, y))))))
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(a, g(x, g(b, g(b, y)))))
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(x, g(b, g(b, y))))
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
G(a, g(x, g(b, g(a, g(x, y))))) → G(b, g(b, y))
G(a, g(x, g(b, g(a, g(x, y))))) → G(b, y)
The TRS R consists of the following rules:
i(x, x) → i(a, b)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 3 SCCs with 10 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(x, g(b, g(b, y))))
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(a, g(x, g(b, g(b, y)))))
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
The TRS R consists of the following rules:
i(x, x) → i(a, b)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(6) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(7) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(x, g(b, g(b, y))))
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(a, g(x, g(b, g(b, y)))))
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(8) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
G(
a,
g(
x,
g(
b,
g(
a,
g(
x,
y))))) →
G(
a,
g(
x,
g(
b,
g(
b,
y)))) at position [1] we obtained the following new rules [LPAR04]:
G(a, g(g(b, g(b, y1)), g(b, g(a, g(g(b, g(b, y1)), y1))))) → G(a, g(a, b)) → G(a, g(g(b, g(b, y1)), g(b, g(a, g(g(b, g(b, y1)), y1))))) → G(a, g(a, b))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, x1))))))) → G(a, g(a, g(a, g(a, g(b, g(b, g(b, x1))))))) → G(a, g(a, g(b, g(a, g(a, g(a, g(b, x1))))))) → G(a, g(a, g(a, g(a, g(b, g(b, g(b, x1)))))))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(y0, g(b, g(a, b)))) → G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(y0, g(b, g(a, b))))
(9) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(a, g(x, g(b, g(b, y)))))
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
G(a, g(g(b, g(b, y1)), g(b, g(a, g(g(b, g(b, y1)), y1))))) → G(a, g(a, b))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, x1))))))) → G(a, g(a, g(a, g(a, g(b, g(b, g(b, x1)))))))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(y0, g(b, g(a, b))))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(10) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(11) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
G(a, g(x, g(b, g(a, g(x, y))))) → G(a, g(a, g(x, g(b, g(b, y)))))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(y0, g(b, g(a, b))))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(12) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
G(
a,
g(
x,
g(
b,
g(
a,
g(
x,
y))))) →
G(
a,
g(
a,
g(
x,
g(
b,
g(
b,
y))))) at position [1] we obtained the following new rules [LPAR04]:
G(a, g(g(b, g(b, y1)), g(b, g(a, g(g(b, g(b, y1)), y1))))) → G(a, g(a, g(a, b))) → G(a, g(g(b, g(b, y1)), g(b, g(a, g(g(b, g(b, y1)), y1))))) → G(a, g(a, g(a, b)))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, x1))))))) → G(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, x1)))))))) → G(a, g(a, g(b, g(a, g(a, g(a, g(b, x1))))))) → G(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, x1))))))))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(a, g(y0, g(b, g(a, b))))) → G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(a, g(y0, g(b, g(a, b)))))
(13) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(y0, g(b, g(a, b))))
G(a, g(g(b, g(b, y1)), g(b, g(a, g(g(b, g(b, y1)), y1))))) → G(a, g(a, g(a, b)))
G(a, g(a, g(b, g(a, g(a, g(a, g(b, x1))))))) → G(a, g(a, g(a, g(a, g(a, g(b, g(b, g(b, x1))))))))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(a, g(y0, g(b, g(a, b)))))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(14) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 2 less nodes.
(15) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(y0, g(b, g(a, b))))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(a, g(y0, g(b, g(a, b)))))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(16) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
G(
a,
g(
y0,
g(
b,
g(
a,
g(
y0,
b))))) →
G(
a,
g(
y0,
g(
b,
g(
a,
b)))) at position [1] we obtained the following new rules [LPAR04]:
G(a, g(g(b, g(a, b)), g(b, g(a, g(g(b, g(a, b)), b))))) → G(a, g(a, b)) → G(a, g(g(b, g(a, b)), g(b, g(a, g(g(b, g(a, b)), b))))) → G(a, g(a, b))
(17) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(a, g(y0, g(b, g(a, b)))))
G(a, g(g(b, g(a, b)), g(b, g(a, g(g(b, g(a, b)), b))))) → G(a, g(a, b))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(18) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(19) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
G(a, g(y0, g(b, g(a, g(y0, b))))) → G(a, g(a, g(y0, g(b, g(a, b)))))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(20) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
G(
a,
g(
y0,
g(
b,
g(
a,
g(
y0,
b))))) →
G(
a,
g(
a,
g(
y0,
g(
b,
g(
a,
b))))) at position [1] we obtained the following new rules [LPAR04]:
G(a, g(g(b, g(a, b)), g(b, g(a, g(g(b, g(a, b)), b))))) → G(a, g(a, g(a, b))) → G(a, g(g(b, g(a, b)), g(b, g(a, g(g(b, g(a, b)), b))))) → G(a, g(a, g(a, b)))
(21) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
G(a, g(g(b, g(a, b)), g(b, g(a, g(g(b, g(a, b)), b))))) → G(a, g(a, g(a, b)))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(22) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 1 less node.
(23) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(24) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(25) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(x, g(b, g(a, g(x, y))))) → G(x, g(b, g(b, y)))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(26) TransformationProof (EQUIVALENT transformation)
By forward instantiating [JAR06] the rule
G(
a,
g(
x,
g(
b,
g(
a,
g(
x,
y))))) →
G(
x,
g(
b,
g(
b,
y))) we obtained the following new rules [LPAR04]:
G(a, g(a, g(b, g(a, g(a, x1))))) → G(a, g(b, g(b, x1))) → G(a, g(a, g(b, g(a, g(a, x1))))) → G(a, g(b, g(b, x1)))
(27) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(a, g(a, g(b, g(a, g(a, x1))))) → G(a, g(b, g(b, x1)))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(28) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 0 SCCs with 1 less node.
(29) TRUE
(30) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(g(x, s(y))) → H(g(s(x), y))
H(s(f(x))) → H(f(x))
H(i(x, y)) → H(h(y))
H(i(x, y)) → H(y)
The TRS R consists of the following rules:
i(x, x) → i(a, b)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(31) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(32) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(g(x, s(y))) → H(g(s(x), y))
H(s(f(x))) → H(f(x))
H(i(x, y)) → H(h(y))
H(i(x, y)) → H(y)
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
g(x, x) → g(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(33) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
H(s(f(x))) → H(f(x))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:
POL(H(x1)) = [1/2]x1
POL(a) = 0
POL(b) = 0
POL(c) = 0
POL(f(x1)) = [4]x1
POL(g(x1, x2)) = 0
POL(h(x1)) = [1/2]x1
POL(i(x1, x2)) = [2]x1 + x2
POL(s(x1)) = [4] + x1
The value of delta used in the strict ordering is 2.
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
g(x, x) → g(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
(34) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(g(x, s(y))) → H(g(s(x), y))
H(i(x, y)) → H(h(y))
H(i(x, y)) → H(y)
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
g(x, x) → g(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(35) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
H(g(x, s(y))) → H(g(s(x), y))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :
| POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
i(x, x) → i(a, b)
(36) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(i(x, y)) → H(h(y))
H(i(x, y)) → H(y)
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
g(x, x) → g(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(37) TransformationProof (EQUIVALENT transformation)
By narrowing [LPAR04] the rule
H(
i(
x,
y)) →
H(
h(
y)) at position [0] we obtained the following new rules [LPAR04]:
H(i(y0, g(x0, s(x1)))) → H(h(g(s(x0), x1))) → H(i(y0, g(x0, s(x1)))) → H(h(g(s(x0), x1)))
H(i(y0, s(f(x0)))) → H(h(f(x0))) → H(i(y0, s(f(x0)))) → H(h(f(x0)))
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0)) → H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
(38) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(i(x, y)) → H(y)
H(i(y0, g(x0, s(x1)))) → H(h(g(s(x0), x1)))
H(i(y0, s(f(x0)))) → H(h(f(x0)))
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
g(x, x) → g(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(39) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
H(i(y0, g(x0, s(x1)))) → H(h(g(s(x0), x1)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] with arctic natural numbers [ARCTIC]:
| POL(i(x1, x2)) = | 2A | + | 0A | · | x1 | + | 0A | · | x2 |
| POL(g(x1, x2)) = | 1A | + | -I | · | x1 | + | -I | · | x2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
i(x, x) → i(a, b)
(40) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(i(x, y)) → H(y)
H(i(y0, s(f(x0)))) → H(h(f(x0)))
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
g(x, x) → g(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(41) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
H(i(y0, s(f(x0)))) → H(h(f(x0)))
The remaining pairs can at least be oriented weakly.
Used ordering: Polynomial interpretation [POLO,RATPOLO]:
POL(H(x1)) = [1/2]x1
POL(a) = 0
POL(b) = 0
POL(c) = 0
POL(f(x1)) = [1/4]
POL(g(x1, x2)) = 0
POL(h(x1)) = [1/2]x1
POL(i(x1, x2)) = [2]x1 + x2
POL(s(x1)) = [1/4]
The value of delta used in the strict ordering is 1/16.
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
g(x, x) → g(a, b)
(42) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(i(x, y)) → H(y)
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
g(x, x) → g(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(43) SplitQDPProof (EQUIVALENT transformation)
We show in the first subproof that some pairs and rules can be removed, afterwards, we continue with the remaining DP-Problem
(44) Complex Obligation (AND)
(45) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(i(x, y)) → H(y)
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
g(x, x) → g(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(46) SemLabProof (SOUND transformation)
We found the following model for the rules of the TRSs R and P.
Interpretation over the domain with elements from 0 to 1.
s: 0
a: 1
b: 1
c: 0
H: 0
f: 0
i: 0
h: 0
g: 0
By semantic labelling [SEMLAB] we obtain the following labelled QDP problem.
(47) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.0-1(x, y)) → H.1(y)
H.0(i.1-0(x, y)) → H.0(y)
H.0(i.1-1(x, y)) → H.1(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
H.0(i.0-0(y0, i.1-0(x0, x1))) → H.0(i.0-1(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.1-1(x0, x1))) → H.0(i.0-1(i.0-0(c., h.0(h.1(x1))), x0))
H.0(i.1-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.1-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
H.0(i.1-0(y0, i.1-0(x0, x1))) → H.0(i.0-1(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.1-0(y0, i.1-1(x0, x1))) → H.0(i.0-1(i.0-0(c., h.0(h.1(x1))), x0))
The TRS R consists of the following rules:
h.0(g.0-0(x, s.0(y))) → h.0(g.0-0(s.0(x), y))
h.0(g.0-0(x, s.1(y))) → h.0(g.0-1(s.0(x), y))
h.0(g.1-0(x, s.0(y))) → h.0(g.0-0(s.1(x), y))
h.0(g.1-0(x, s.1(y))) → h.0(g.0-1(s.1(x), y))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
h.0(i.0-1(x, y)) → i.0-0(i.0-0(c., h.0(h.1(y))), x)
h.0(i.1-0(x, y)) → i.0-1(i.0-0(c., h.0(h.0(y))), x)
h.0(i.1-1(x, y)) → i.0-1(i.0-0(c., h.0(h.1(y))), x)
i.0-0(x, x) → i.1-1(a., b.)
i.1-1(x, x) → i.1-1(a., b.)
g.0-0(x, x) → g.1-1(a., b.)
g.1-1(x, x) → g.1-1(a., b.)
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
f.0(g.0-0(s.0(x), y)) → f.0(g.0-0(x, s.0(y)))
f.0(g.0-1(s.0(x), y)) → f.0(g.0-0(x, s.1(y)))
f.0(g.0-0(s.1(x), y)) → f.0(g.1-0(x, s.0(y)))
f.0(g.0-1(s.1(x), y)) → f.0(g.1-0(x, s.1(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(48) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 6 less nodes.
(49) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.1-0(x, y)) → H.0(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
H.0(i.1-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.1-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
The TRS R consists of the following rules:
h.0(g.0-0(x, s.0(y))) → h.0(g.0-0(s.0(x), y))
h.0(g.0-0(x, s.1(y))) → h.0(g.0-1(s.0(x), y))
h.0(g.1-0(x, s.0(y))) → h.0(g.0-0(s.1(x), y))
h.0(g.1-0(x, s.1(y))) → h.0(g.0-1(s.1(x), y))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
h.0(i.0-1(x, y)) → i.0-0(i.0-0(c., h.0(h.1(y))), x)
h.0(i.1-0(x, y)) → i.0-1(i.0-0(c., h.0(h.0(y))), x)
h.0(i.1-1(x, y)) → i.0-1(i.0-0(c., h.0(h.1(y))), x)
i.0-0(x, x) → i.1-1(a., b.)
i.1-1(x, x) → i.1-1(a., b.)
g.0-0(x, x) → g.1-1(a., b.)
g.1-1(x, x) → g.1-1(a., b.)
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
f.0(g.0-0(s.0(x), y)) → f.0(g.0-0(x, s.0(y)))
f.0(g.0-1(s.0(x), y)) → f.0(g.0-0(x, s.1(y)))
f.0(g.0-0(s.1(x), y)) → f.0(g.1-0(x, s.0(y)))
f.0(g.0-1(s.1(x), y)) → f.0(g.1-0(x, s.1(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(50) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
H.0(i.1-0(x, y)) → H.0(y)
H.0(i.1-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.1-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
The following rules are removed from R:
h.0(i.1-0(x, y)) → i.0-1(i.0-0(c., h.0(h.0(y))), x)
i.1-1(x, x) → i.1-1(a., b.)
g.1-1(x, x) → g.1-1(a., b.)
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(H.0(x1)) = x1
POL(a.) = 0
POL(b.) = 0
POL(c.) = 0
POL(f.0(x1)) = x1
POL(f.1(x1)) = x1
POL(g.0-0(x1, x2)) = x1 + x2
POL(g.0-1(x1, x2)) = x1 + x2
POL(g.1-0(x1, x2)) = x1 + x2
POL(g.1-1(x1, x2)) = x1 + x2
POL(h.0(x1)) = x1
POL(h.1(x1)) = x1
POL(i.0-0(x1, x2)) = x1 + x2
POL(i.0-1(x1, x2)) = x1 + x2
POL(i.1-0(x1, x2)) = x1 + x2
POL(i.1-1(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
The TRS R consists of the following rules:
i.0-0(x, x) → i.1-1(a., b.)
h.0(g.1-0(x, s.0(y))) → h.0(g.0-0(s.1(x), y))
h.0(g.0-0(x, s.0(y))) → h.0(g.0-0(s.0(x), y))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(g.0-0(x, s.1(y))) → h.0(g.0-1(s.0(x), y))
h.0(g.1-0(x, s.1(y))) → h.0(g.0-1(s.1(x), y))
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
h.0(i.0-1(x, y)) → i.0-0(i.0-0(c., h.0(h.1(y))), x)
h.0(i.1-1(x, y)) → i.0-1(i.0-0(c., h.0(h.1(y))), x)
g.0-0(x, x) → g.1-1(a., b.)
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
f.0(g.0-1(s.0(x), y)) → f.0(g.0-0(x, s.1(y)))
f.0(g.0-0(s.0(x), y)) → f.0(g.0-0(x, s.0(y)))
f.0(g.0-0(s.1(x), y)) → f.0(g.1-0(x, s.0(y)))
f.0(g.0-1(s.1(x), y)) → f.0(g.1-0(x, s.1(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(52) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
g.0-0(x, x) → g.1-1(a., b.)
Used ordering: Polynomial interpretation [POLO]:
POL(H.0(x1)) = x1
POL(a.) = 0
POL(b.) = 0
POL(c.) = 0
POL(f.0(x1)) = x1
POL(f.1(x1)) = x1
POL(g.0-0(x1, x2)) = 1 + x1 + x2
POL(g.0-1(x1, x2)) = 1 + x1 + x2
POL(g.1-0(x1, x2)) = 1 + x1 + x2
POL(g.1-1(x1, x2)) = x1 + x2
POL(h.0(x1)) = x1
POL(h.1(x1)) = x1
POL(i.0-0(x1, x2)) = x1 + x2
POL(i.0-1(x1, x2)) = x1 + x2
POL(i.1-1(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
(53) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
The TRS R consists of the following rules:
i.0-0(x, x) → i.1-1(a., b.)
h.0(g.1-0(x, s.0(y))) → h.0(g.0-0(s.1(x), y))
h.0(g.0-0(x, s.0(y))) → h.0(g.0-0(s.0(x), y))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(g.0-0(x, s.1(y))) → h.0(g.0-1(s.0(x), y))
h.0(g.1-0(x, s.1(y))) → h.0(g.0-1(s.1(x), y))
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
h.0(i.0-1(x, y)) → i.0-0(i.0-0(c., h.0(h.1(y))), x)
h.0(i.1-1(x, y)) → i.0-1(i.0-0(c., h.0(h.1(y))), x)
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
f.0(g.0-1(s.0(x), y)) → f.0(g.0-0(x, s.1(y)))
f.0(g.0-0(s.0(x), y)) → f.0(g.0-0(x, s.0(y)))
f.0(g.0-0(s.1(x), y)) → f.0(g.1-0(x, s.0(y)))
f.0(g.0-1(s.1(x), y)) → f.0(g.1-0(x, s.1(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(54) PisEmptyProof (SOUND transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(55) TRUE
(56) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(i(x, y)) → H(y)
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
The TRS R consists of the following rules:
i(x, x) → i(a, b)
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(57) SplitQDPProof (EQUIVALENT transformation)
We show in the first subproof that some pairs and rules can be removed, afterwards, we continue with the remaining DP-Problem
(58) Complex Obligation (AND)
(59) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(i(x, y)) → H(y)
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
The TRS R consists of the following rules:
i(x, x) → i(a, b)
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(60) SemLabProof (SOUND transformation)
We found the following model for the rules of the TRSs R and P.
Interpretation over the domain with elements from 0 to 1.
s: 0
a: 0
b: 0
c: 0
H: 0
f: 0
i: 0
h: 0
g: 1
By semantic labelling [SEMLAB] we obtain the following labelled QDP problem.
(61) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.0-1(x, y)) → H.1(y)
H.0(i.1-0(x, y)) → H.0(y)
H.0(i.1-1(x, y)) → H.1(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
H.0(i.0-0(y0, i.1-0(x0, x1))) → H.0(i.0-1(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.1-1(x0, x1))) → H.0(i.0-1(i.0-0(c., h.0(h.1(x1))), x0))
H.0(i.1-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.1-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
H.0(i.1-0(y0, i.1-0(x0, x1))) → H.0(i.0-1(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.1-0(y0, i.1-1(x0, x1))) → H.0(i.0-1(i.0-0(c., h.0(h.1(x1))), x0))
The TRS R consists of the following rules:
i.0-0(x, x) → i.0-0(a., b.)
i.1-1(x, x) → i.0-0(a., b.)
h.1(g.0-0(x, s.0(y))) → h.1(g.0-0(s.0(x), y))
h.1(g.0-0(x, s.1(y))) → h.1(g.0-1(s.0(x), y))
h.1(g.1-0(x, s.0(y))) → h.1(g.0-0(s.1(x), y))
h.1(g.1-0(x, s.1(y))) → h.1(g.0-1(s.1(x), y))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
h.0(i.0-1(x, y)) → i.0-0(i.0-0(c., h.0(h.1(y))), x)
h.0(i.1-0(x, y)) → i.0-1(i.0-0(c., h.0(h.0(y))), x)
h.0(i.1-1(x, y)) → i.0-1(i.0-0(c., h.0(h.1(y))), x)
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
f.1(g.0-0(s.0(x), y)) → f.1(g.0-0(x, s.0(y)))
f.1(g.0-1(s.0(x), y)) → f.1(g.0-0(x, s.1(y)))
f.1(g.0-0(s.1(x), y)) → f.1(g.1-0(x, s.0(y)))
f.1(g.0-1(s.1(x), y)) → f.1(g.1-0(x, s.1(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(62) DependencyGraphProof (EQUIVALENT transformation)
The approximation of the Dependency Graph [LPAR04,FROCOS05,EDGSTAR] contains 1 SCC with 6 less nodes.
(63) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.1-0(x, y)) → H.0(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
H.0(i.1-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.1-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
The TRS R consists of the following rules:
i.0-0(x, x) → i.0-0(a., b.)
i.1-1(x, x) → i.0-0(a., b.)
h.1(g.0-0(x, s.0(y))) → h.1(g.0-0(s.0(x), y))
h.1(g.0-0(x, s.1(y))) → h.1(g.0-1(s.0(x), y))
h.1(g.1-0(x, s.0(y))) → h.1(g.0-0(s.1(x), y))
h.1(g.1-0(x, s.1(y))) → h.1(g.0-1(s.1(x), y))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
h.0(i.0-1(x, y)) → i.0-0(i.0-0(c., h.0(h.1(y))), x)
h.0(i.1-0(x, y)) → i.0-1(i.0-0(c., h.0(h.0(y))), x)
h.0(i.1-1(x, y)) → i.0-1(i.0-0(c., h.0(h.1(y))), x)
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
f.1(g.0-0(s.0(x), y)) → f.1(g.0-0(x, s.0(y)))
f.1(g.0-1(s.0(x), y)) → f.1(g.0-0(x, s.1(y)))
f.1(g.0-0(s.1(x), y)) → f.1(g.1-0(x, s.0(y)))
f.1(g.0-1(s.1(x), y)) → f.1(g.1-0(x, s.1(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(64) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
H.0(i.1-0(x, y)) → H.0(y)
H.0(i.1-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.1-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
The following rules are removed from R:
i.1-1(x, x) → i.0-0(a., b.)
h.0(i.1-0(x, y)) → i.0-1(i.0-0(c., h.0(h.0(y))), x)
h.0(i.1-1(x, y)) → i.0-1(i.0-0(c., h.0(h.1(y))), x)
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(H.0(x1)) = x1
POL(a.) = 0
POL(b.) = 0
POL(c.) = 0
POL(f.0(x1)) = x1
POL(f.1(x1)) = x1
POL(g.0-0(x1, x2)) = x1 + x2
POL(g.0-1(x1, x2)) = x1 + x2
POL(g.1-0(x1, x2)) = x1 + x2
POL(h.0(x1)) = x1
POL(h.1(x1)) = x1
POL(i.0-0(x1, x2)) = x1 + x2
POL(i.0-1(x1, x2)) = x1 + x2
POL(i.1-0(x1, x2)) = x1 + x2
POL(i.1-1(x1, x2)) = 1 + x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
(65) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
H.0(i.0-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
The TRS R consists of the following rules:
h.1(g.0-0(x, s.0(y))) → h.1(g.0-0(s.0(x), y))
h.1(g.0-0(x, s.1(y))) → h.1(g.0-1(s.0(x), y))
h.1(g.1-0(x, s.0(y))) → h.1(g.0-0(s.1(x), y))
h.1(g.1-0(x, s.1(y))) → h.1(g.0-1(s.1(x), y))
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
h.0(i.0-1(x, y)) → i.0-0(i.0-0(c., h.0(h.1(y))), x)
i.0-0(x, x) → i.0-0(a., b.)
f.1(g.0-0(s.0(x), y)) → f.1(g.0-0(x, s.0(y)))
f.1(g.0-1(s.0(x), y)) → f.1(g.0-0(x, s.1(y)))
f.1(g.0-0(s.1(x), y)) → f.1(g.1-0(x, s.0(y)))
f.1(g.0-1(s.1(x), y)) → f.1(g.1-0(x, s.1(y)))
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(66) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
The following dependency pairs can be deleted:
H.0(i.0-0(y0, i.0-1(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.1(x1))), x0))
The following rules are removed from R:
h.0(i.0-1(x, y)) → i.0-0(i.0-0(c., h.0(h.1(y))), x)
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(H.0(x1)) = x1
POL(a.) = 0
POL(b.) = 0
POL(c.) = 0
POL(f.0(x1)) = x1
POL(f.1(x1)) = x1
POL(g.0-0(x1, x2)) = x1 + x2
POL(g.0-1(x1, x2)) = x1 + x2
POL(g.1-0(x1, x2)) = x1 + x2
POL(h.0(x1)) = x1
POL(h.1(x1)) = x1
POL(i.0-0(x1, x2)) = x1 + x2
POL(i.0-1(x1, x2)) = 1 + x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
(67) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
The TRS R consists of the following rules:
h.1(g.0-0(x, s.0(y))) → h.1(g.0-0(s.0(x), y))
h.1(g.0-0(x, s.1(y))) → h.1(g.0-1(s.0(x), y))
h.1(g.1-0(x, s.0(y))) → h.1(g.0-0(s.1(x), y))
h.1(g.1-0(x, s.1(y))) → h.1(g.0-1(s.1(x), y))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
i.0-0(x, x) → i.0-0(a., b.)
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
f.1(g.0-0(s.0(x), y)) → f.1(g.0-0(x, s.0(y)))
f.1(g.0-1(s.0(x), y)) → f.1(g.0-0(x, s.1(y)))
f.1(g.0-0(s.1(x), y)) → f.1(g.1-0(x, s.0(y)))
f.1(g.0-1(s.1(x), y)) → f.1(g.1-0(x, s.1(y)))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(68) UsableRulesReductionPairsProof (EQUIVALENT transformation)
By using the usable rules with reduction pair processor [LPAR04] with a polynomial ordering [POLO], all dependency pairs and the corresponding usable rules [FROCOS05] can be oriented non-strictly. All non-usable rules are removed, and those dependency pairs and usable rules that have been oriented strictly or contain non-usable symbols in their left-hand side are removed as well.
No dependency pairs are removed.
The following rules are removed from R:
h.1(g.0-0(x, s.0(y))) → h.1(g.0-0(s.0(x), y))
h.1(g.0-0(x, s.1(y))) → h.1(g.0-1(s.0(x), y))
h.1(g.1-0(x, s.0(y))) → h.1(g.0-0(s.1(x), y))
h.1(g.1-0(x, s.1(y))) → h.1(g.0-1(s.1(x), y))
f.1(g.0-1(s.0(x), y)) → f.1(g.0-0(x, s.1(y)))
f.1(g.0-1(s.1(x), y)) → f.1(g.1-0(x, s.1(y)))
Used ordering: POLO with Polynomial interpretation [POLO]:
POL(H.0(x1)) = x1
POL(a.) = 0
POL(b.) = 0
POL(c.) = 0
POL(f.0(x1)) = x1
POL(f.1(x1)) = x1
POL(g.0-0(x1, x2)) = x1 + x2
POL(g.0-1(x1, x2)) = 1 + x1 + x2
POL(g.1-0(x1, x2)) = x1 + x2
POL(h.0(x1)) = x1
POL(i.0-0(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = x1
(69) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
The TRS R consists of the following rules:
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
i.0-0(x, x) → i.0-0(a., b.)
f.1(g.0-0(s.0(x), y)) → f.1(g.0-0(x, s.0(y)))
f.1(g.0-0(s.1(x), y)) → f.1(g.1-0(x, s.0(y)))
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(70) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented rules of the TRS R:
f.1(g.0-0(s.1(x), y)) → f.1(g.1-0(x, s.0(y)))
Used ordering: Polynomial interpretation [POLO]:
POL(H.0(x1)) = x1
POL(a.) = 0
POL(b.) = 0
POL(c.) = 0
POL(f.0(x1)) = x1
POL(f.1(x1)) = x1
POL(g.0-0(x1, x2)) = 1 + x1 + x2
POL(g.1-0(x1, x2)) = 1 + x1 + x2
POL(h.0(x1)) = x1
POL(i.0-0(x1, x2)) = x1 + x2
POL(s.0(x1)) = x1
POL(s.1(x1)) = 1 + x1
(71) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H.0(i.0-0(x, y)) → H.0(y)
H.0(i.0-0(y0, i.0-0(x0, x1))) → H.0(i.0-0(i.0-0(c., h.0(h.0(x1))), x0))
The TRS R consists of the following rules:
h.0(s.0(f.1(x))) → h.0(f.1(x))
h.0(s.0(f.0(x))) → h.0(f.0(x))
h.0(i.0-0(x, y)) → i.0-0(i.0-0(c., h.0(h.0(y))), x)
i.0-0(x, x) → i.0-0(a., b.)
f.1(g.0-0(s.0(x), y)) → f.1(g.0-0(x, s.0(y)))
f.0(s.0(x)) → s.0(s.0(f.0(h.0(s.0(x)))))
f.0(s.1(x)) → s.0(s.0(f.0(h.0(s.1(x)))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(72) PisEmptyProof (SOUND transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(73) TRUE
(74) Obligation:
Q DP problem:
The TRS P consists of the following rules:
H(i(x, y)) → H(y)
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
The TRS R consists of the following rules:
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
f(g(s(x), y)) → f(g(x, s(y)))
f(s(x)) → s(s(f(h(s(x)))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(75) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
H(i(x, y)) → H(y)
H(i(y0, i(x0, x1))) → H(i(i(c, h(h(x1))), x0))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO] to (N^2, +, *, >=, >) :
| POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
| POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
(76) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
h(s(f(x))) → h(f(x))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
f(g(s(x), y)) → f(g(x, s(y)))
f(s(x)) → s(s(f(h(s(x)))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(77) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(78) YES
(79) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(g(s(x), y)) → F(g(x, s(y)))
F(s(x)) → F(h(s(x)))
The TRS R consists of the following rules:
i(x, x) → i(a, b)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(a, g(x, g(b, g(a, g(x, y))))) → g(a, g(a, g(a, g(x, g(b, g(b, y))))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(80) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(81) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(g(s(x), y)) → F(g(x, s(y)))
F(s(x)) → F(h(s(x)))
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
g(x, x) → g(a, b)
h(i(x, y)) → i(i(c, h(h(y))), x)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
i(x, x) → i(a, b)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(82) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04,JAR06].
The following pairs can be oriented strictly and are deleted.
F(s(x)) → F(h(s(x)))
The remaining pairs can at least be oriented weakly.
Used ordering: Combined order from the following AFS and order.
F(
x1) =
x1
g(
x1,
x2) =
g
s(
x1) =
s
h(
x1) =
h
i(
x1,
x2) =
i
Knuth-Bendix order [KBO] with precedence:
s > h > i
and weight map:
s=1
i=1
h=1
g=2
The following usable rules [FROCOS05] with respect to the argument filtering of the ordering [JAR06] were oriented:
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
h(i(x, y)) → i(i(c, h(h(y))), x)
i(x, x) → i(a, b)
(83) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(g(s(x), y)) → F(g(x, s(y)))
The TRS R consists of the following rules:
h(g(x, s(y))) → h(g(s(x), y))
h(s(f(x))) → h(f(x))
g(x, x) → g(a, b)
h(i(x, y)) → i(i(c, h(h(y))), x)
f(s(x)) → s(s(f(h(s(x)))))
f(g(s(x), y)) → f(g(x, s(y)))
i(x, x) → i(a, b)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(84) UsableRulesProof (EQUIVALENT transformation)
We can use the usable rules and reduction pair processor [LPAR04] with the Ce-compatible extension of the polynomial order that maps every function symbol to the sum of its arguments. Then, we can delete all non-usable rules [FROCOS05] from R.
(85) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(g(s(x), y)) → F(g(x, s(y)))
The TRS R consists of the following rules:
g(x, x) → g(a, b)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(86) MRRProof (EQUIVALENT transformation)
By using the rule removal processor [LPAR04] with the following ordering, at least one Dependency Pair or term rewrite system rule of this QDP problem can be strictly oriented.
Strictly oriented dependency pairs:
F(g(s(x), y)) → F(g(x, s(y)))
Used ordering: Polynomial interpretation [POLO]:
POL(F(x1)) = x1
POL(a) = 0
POL(b) = 0
POL(g(x1, x2)) = 2·x1 + x2
POL(s(x1)) = 1 + x1
(87) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
g(x, x) → g(a, b)
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(88) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(89) YES