R
↳Dependency Pair Analysis
F(a, f(x, a)) -> F(x, f(f(f(a, a), a), a))
F(a, f(x, a)) -> F(f(f(a, a), a), a)
F(a, f(x, a)) -> F(f(a, a), a)
F(a, f(x, a)) -> F(a, a)
R
↳DPs
→DP Problem 1
↳Forward Instantiation Transformation
F(a, f(x, a)) -> F(x, f(f(f(a, a), a), a))
f(a, f(x, a)) -> f(x, f(f(f(a, a), a), a))
one new Dependency Pair is created:
F(a, f(x, a)) -> F(x, f(f(f(a, a), a), a))
F(a, f(a, a)) -> F(a, f(f(f(a, a), a), a))
R
↳DPs
→DP Problem 1
↳FwdInst
→DP Problem 2
↳Narrowing Transformation
F(a, f(a, a)) -> F(a, f(f(f(a, a), a), a))
f(a, f(x, a)) -> f(x, f(f(f(a, a), a), a))
no new Dependency Pairs are created.
F(a, f(a, a)) -> F(a, f(f(f(a, a), a), a))