R
↳Dependency Pair Analysis
A(a(f(x, y))) -> F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
A(a(f(x, y))) -> A(b(a(b(a(x)))))
A(a(f(x, y))) -> A(b(a(x)))
A(a(f(x, y))) -> A(x)
A(a(f(x, y))) -> A(b(a(b(a(y)))))
A(a(f(x, y))) -> A(b(a(y)))
A(a(f(x, y))) -> A(y)
F(a(x), a(y)) -> A(f(x, y))
F(a(x), a(y)) -> F(x, y)
F(b(x), b(y)) -> F(x, y)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
F(b(x), b(y)) -> F(x, y)
F(a(x), a(y)) -> F(x, y)
A(a(f(x, y))) -> A(y)
A(a(f(x, y))) -> A(x)
F(a(x), a(y)) -> A(f(x, y))
A(a(f(x, y))) -> F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
a(a(f(x, y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) -> a(f(x, y))
f(b(x), b(y)) -> b(f(x, y))
innermost
A(a(f(x, y))) -> A(y)
A(a(f(x, y))) -> A(x)
f(a(x), a(y)) -> a(f(x, y))
f(b(x), b(y)) -> b(f(x, y))
a(a(f(x, y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
POL(b(x1)) = x1 POL(a(x1)) = x1 POL(f(x1, x2)) = 1 + x1 + x2 POL(F(x1, x2)) = 1 + x1 + x2 POL(A(x1)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Remaining Obligation(s)
F(b(x), b(y)) -> F(x, y)
F(a(x), a(y)) -> F(x, y)
F(a(x), a(y)) -> A(f(x, y))
A(a(f(x, y))) -> F(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
a(a(f(x, y))) -> f(a(b(a(b(a(x))))), a(b(a(b(a(y))))))
f(a(x), a(y)) -> a(f(x, y))
f(b(x), b(y)) -> b(f(x, y))
innermost