(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) Narrowing (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(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))))
(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) Narrowing (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(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)))))
(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) Narrowing (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))
(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) Narrowing (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)))
(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) ForwardInstantiation (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)))
(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(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)
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].
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: Matrix interpretation [MATRO]:
POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
h(i(x, y)) → i(i(c, h(h(y))), x)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
g(x, x) → g(a, b)
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)))))
(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(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)
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].
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]:
POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
h(i(x, y)) → i(i(c, h(h(y))), x)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
g(x, x) → g(a, b)
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)))))
(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(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)
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) Narrowing (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, s(f(x0)))) → H(h(f(x0)))
H(i(y0, g(x0, s(x1)))) → H(h(g(s(x0), x1)))
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, s(f(x0)))) → H(h(f(x0)))
H(i(y0, g(x0, s(x1)))) → H(h(g(s(x0), x1)))
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(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)
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].
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: Matrix interpretation [MATRO]:
POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
h(i(x, y)) → i(i(c, h(h(y))), x)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
g(x, x) → g(a, b)
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)))))
(40) 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, 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(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)
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].
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]:
POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
h(i(x, y)) → i(i(c, h(h(y))), x)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
g(x, x) → g(a, b)
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)))))
(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(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)
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) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
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]:
POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
h(i(x, y)) → i(i(c, h(h(y))), x)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
g(x, x) → g(a, b)
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)))))
(44) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
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)
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.
(45) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(46) TRUE
(47) 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.
(48) 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.
(49) 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(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
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.
(50) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
The following pairs can be oriented strictly and are deleted.
F(g(s(x), y)) → F(g(x, s(y)))
The remaining pairs can at least be oriented weakly.
Used ordering: Matrix interpretation [MATRO]:
POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
f(g(s(x), y)) → f(g(x, s(y)))
i(x, x) → i(a, b)
f(s(x)) → s(s(f(h(s(x)))))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
(51) Obligation:
Q DP problem:
The TRS P consists of the following rules:
F(s(x)) → F(h(s(x)))
The TRS R consists of the following rules:
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
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.
(52) QDPOrderProof (EQUIVALENT transformation)
We use the reduction pair processor [LPAR04].
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: Matrix interpretation [MATRO]:
POL(g(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
POL(i(x1, x2)) = | | + | | · | x1 | + | | · | x2 |
The following usable rules [FROCOS05] were oriented:
f(g(s(x), y)) → f(g(x, s(y)))
i(x, x) → i(a, b)
f(s(x)) → s(s(f(h(s(x)))))
h(i(x, y)) → i(i(c, h(h(y))), x)
g(x, x) → g(a, b)
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
(53) Obligation:
Q DP problem:
P is empty.
The TRS R consists of the following rules:
h(s(f(x))) → h(f(x))
h(g(x, s(y))) → h(g(s(x), y))
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.
(54) PisEmptyProof (EQUIVALENT transformation)
The TRS P is empty. Hence, there is no (P,Q,R) chain.
(55) TRUE