(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) 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.
(7) 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.