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