(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))
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:
H(x, x) → H(a, b)
G(g(x, a), y) → G(g(a, y), g(a, x))
G(g(x, a), y) → G(a, y)
G(g(x, a), y) → G(a, x)
F(g(x, y)) → G(g(f(f(y)), h(a, a)), x)
F(g(x, y)) → G(f(f(y)), h(a, a))
F(g(x, y)) → F(f(y))
F(g(x, y)) → F(y)
F(g(x, y)) → H(a, a)
H(h(f(f(x)), y), h(z, v)) → H(h(f(z), f(f(f(y)))), h(v, x))
H(h(f(f(x)), y), h(z, v)) → H(f(z), f(f(f(y))))
H(h(f(f(x)), y), h(z, v)) → F(z)
H(h(f(f(x)), y), h(z, v)) → F(f(f(y)))
H(h(f(f(x)), y), h(z, v)) → F(f(y))
H(h(f(f(x)), y), h(z, v)) → F(y)
H(h(f(f(x)), y), h(z, v)) → H(v, x)
The TRS R consists of the following rules:
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))
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 11 less nodes.
(4) Complex Obligation (AND)
(5) Obligation:
Q DP problem:
The TRS P consists of the following rules:
G(g(x, a), y) → G(g(a, y), g(a, x))
The TRS R consists of the following rules:
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))
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:
F(g(x, y)) → F(y)
F(g(x, y)) → F(f(y))
The TRS R consists of the following rules:
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))
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:
H(h(f(f(x)), y), h(z, v)) → H(v, x)
H(h(f(f(x)), y), h(z, v)) → H(h(f(z), f(f(f(y)))), h(v, x))
The TRS R consists of the following rules:
h(x, x) → h(a, b)
g(g(x, a), y) → g(g(a, y), g(a, x))
f(g(x, y)) → g(g(f(f(y)), h(a, a)), x)
h(h(f(f(x)), y), h(z, v)) → h(h(f(z), f(f(f(y)))), h(v, x))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.