R
↳Dependency Pair Analysis
F(f(a, f(x, a)), a) -> F(a, f(f(x, a), a))
F(f(a, f(x, a)), a) -> F(f(x, a), a)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
F(f(a, f(x, a)), a) -> F(f(x, a), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
one new Dependency Pair is created:
F(f(a, f(x, a)), a) -> F(f(x, a), a)
F(f(a, f(f(a, f(x'', a)), a)), a) -> F(f(a, f(f(x'', a), a)), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Remaining Obligation(s)
F(f(a, f(f(a, f(x'', a)), a)), a) -> F(f(a, f(f(x'', a), a)), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))