R
↳Dependency Pair Analysis
F(f(a, f(x, a)), a) -> F(a, f(f(x, a), a))
F(f(a, f(x, a)), a) -> F(f(x, a), a)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
F(f(a, f(x, a)), a) -> F(f(x, a), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
one new Dependency Pair is created:
F(f(a, f(x, a)), a) -> F(f(x, a), a)
F(f(a, f(f(a, f(x'', a)), a)), a) -> F(f(a, f(f(x'', a), a)), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
F(f(a, f(f(a, f(x'', a)), a)), a) -> F(f(a, f(f(x'', a), a)), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
one new Dependency Pair is created:
F(f(a, f(f(a, f(x'', a)), a)), a) -> F(f(a, f(f(x'', a), a)), a)
F(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a) -> F(f(a, f(f(a, f(f(x', a), a)), a)), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Narrowing Transformation
F(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a) -> F(f(a, f(f(a, f(f(x', a), a)), a)), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
two new Dependency Pairs are created:
F(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a) -> F(f(a, f(f(a, f(f(x', a), a)), a)), a)
F(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a) -> F(f(a, f(a, f(f(f(x'', a), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(x'', a), a)), a)), a)), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Narrowing Transformation
F(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(x'', a), a)), a)), a)), a)
F(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a) -> F(f(a, f(a, f(f(f(x'', a), a), a))), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
one new Dependency Pair is created:
F(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a) -> F(f(a, f(a, f(f(f(x'', a), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(x', a), a)), a), a))), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
F(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(x', a), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(x'', a), a)), a)), a)), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
three new Dependency Pairs are created:
F(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(x'', a), a)), a)), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(x''', a), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(a, f(f(f(x''', a), a), a))), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(a, f(f(x', a), a)), a)), a)), a)), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(a, f(f(x', a), a)), a)), a)), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(a, f(f(f(x''', a), a), a))), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(x''', a), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(x', a), a)), a), a))), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
two new Dependency Pairs are created:
F(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(x', a), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(a, f(f(f(x'', a), a), a)), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(a, f(f(x'', a), a)), a)), a), a))), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(a, f(f(x'', a), a)), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(a, f(f(f(x'', a), a), a)), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(a, f(f(f(x''', a), a), a))), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(x''', a), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(a, f(f(x', a), a)), a)), a)), a)), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
two new Dependency Pairs are created:
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(x''', a), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'''', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(a, f(f(f(x'''', a), a), a)), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(a, f(f(x', a), a)), a)), a), a))), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(a, f(f(x', a), a)), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'''', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(a, f(f(f(x'''', a), a), a)), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(a, f(f(f(x'', a), a), a)), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(a, f(f(x', a), a)), a)), a)), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(a, f(f(f(x''', a), a), a))), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(a, f(f(x'', a), a)), a)), a), a))), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))
one new Dependency Pair is created:
F(f(a, f(f(a, f(f(a, f(f(a, f(x''', a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(a, f(f(f(x''', a), a), a))), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(a, f(f(f(a, f(f(x', a), a)), a), a))), a)), a)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 9
↳Remaining Obligation(s)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(a, f(f(f(a, f(f(x', a), a)), a), a))), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'''', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(a, f(f(f(x'''', a), a), a)), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(a, f(f(x'', a), a)), a)), a), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(x'', a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(a, f(f(f(x'', a), a), a)), a))), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(f(a, f(f(a, f(f(a, f(f(x', a), a)), a)), a)), a)), a)
F(f(a, f(f(a, f(f(a, f(f(a, f(f(a, f(x', a)), a)), a)), a)), a)), a) -> F(f(a, f(a, f(f(f(a, f(f(a, f(f(x', a), a)), a)), a), a))), a)
f(f(a, f(x, a)), a) -> f(a, f(f(x, a), a))