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