R
↳Dependency Pair Analysis
F(x, f(f(a, a), a)) -> F(f(a, f(a, a)), x)
F(x, f(f(a, a), a)) -> F(a, f(a, a))
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
F(x, f(f(a, a), a)) -> F(a, f(a, a))
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(x, f(f(a, a), a)) -> F(a, f(a, a))
f(x, f(f(a, a), a)) -> f(f(a, f(a, a)), x)
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(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)