R
↳Dependency Pair Analysis
F(f(a, f(a, a)), x) -> F(x, f(f(a, a), a))
F(f(a, f(a, a)), x) -> F(f(a, a), a)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
F(f(a, f(a, a)), x) -> F(f(a, a), a)
F(f(a, f(a, a)), x) -> F(x, f(f(a, a), a))
f(f(a, f(a, a)), x) -> f(x, f(f(a, a), a))
F(f(a, f(a, a)), x) -> F(f(a, a), a)
f(f(a, f(a, a)), x) -> f(x, f(f(a, a), a))
POL(a) = 0 POL(F(x1, x2)) = x1 + x2 POL(f(x1, x2)) = 1 + x1 + x2
F(x1, x2) -> F(x1, x2)
f(x1, x2) -> f(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
F(f(a, f(a, a)), x) -> F(x, f(f(a, a), a))
f(f(a, f(a, a)), x) -> f(x, f(f(a, a), a))