(0) Obligation:
Q restricted rewrite system:
The TRS R consists of the following rules:
g(f(x, y)) → f(f(g(g(x)), g(g(y))), f(g(g(x)), g(g(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:
G(f(x, y)) → G(g(x))
G(f(x, y)) → G(x)
G(f(x, y)) → G(g(y))
G(f(x, y)) → G(y)
The TRS R consists of the following rules:
g(f(x, y)) → f(f(g(g(x)), g(g(y))), f(g(g(x)), g(g(y))))
Q is empty.
We have to consider all minimal (P,Q,R)-chains.
(3) NonLoopProof (EQUIVALENT transformation)
By Theorem 8 [NONLOOP] we deduce infiniteness of the QDP.
We apply the theorem with m = 1, b = 0,
σ' = [ ], and μ' = [x2 / g(g(x2)), x0 / g(g(x0)), x1 / f(g(g(x2)), g(g(x0)))] on the rule
G(f(f(g(g(x2)), g(g(x0))), f(g(g(x2)), g(g(x0)))))[ ]n[ ] → G(f(f(g(g(x2)), g(g(x0))), f(g(g(x2)), g(g(x0)))))[ ]n[x2 / g(g(x2)), x0 / g(g(x0)), x1 / f(g(g(x2)), g(g(x0)))]
This rule is correct for the QDP as the following derivation shows:
intermediate steps: Equivalent (Simplify mu) - Instantiate mu - Instantiation
G(f(f(y1, y0), x0))[ ]n[ ] → G(f(f(g(g(y1)), g(g(y0))), f(g(g(y1)), g(g(y0)))))[ ]n[ ]
by Narrowing at position: [0]
intermediate steps: Instantiation - Instantiation
G(f(x, y))[ ]n[ ] → G(g(x))[ ]n[ ]
by OriginalRule from TRS P
intermediate steps: Instantiation
g(f(x, y))[ ]n[ ] → f(f(g(g(x)), g(g(y))), f(g(g(x)), g(g(y))))[ ]n[ ]
by OriginalRule from TRS R
(4) NO