R
↳Dependency Pair Analysis
F(a, f(x, a)) -> F(a, f(f(f(a, a), a), x))
F(a, f(x, a)) -> F(f(f(a, a), a), x)
F(a, f(x, a)) -> F(f(a, a), a)
F(a, f(x, a)) -> F(a, a)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
F(a, f(x, a)) -> F(a, f(f(f(a, a), a), x))
f(a, f(x, a)) -> f(a, f(f(f(a, a), a), x))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Instantiation Transformation
F(a, f(x, a)) -> F(a, f(f(f(a, a), a), x))
none
innermost
one new Dependency Pair is created:
F(a, f(x, a)) -> F(a, f(f(f(a, a), a), x))
F(a, f(f(f(a, a), a), a)) -> F(a, f(f(f(a, a), a), f(f(a, a), a)))