R
↳Dependency Pair Analysis
F(a, f(b, x)) -> F(b, f(a, x))
F(a, f(b, x)) -> F(a, x)
F(b, f(c, x)) -> F(c, f(b, x))
F(b, f(c, x)) -> F(b, x)
F(c, f(a, x)) -> F(a, f(c, x))
F(c, f(a, x)) -> F(c, x)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
F(b, f(c, x)) -> F(b, x)
F(c, f(a, x)) -> F(c, x)
F(a, f(b, x)) -> F(a, x)
F(c, f(a, x)) -> F(a, f(c, x))
F(b, f(c, x)) -> F(c, f(b, x))
F(a, f(b, x)) -> F(b, f(a, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(a, f(b, x)) -> F(b, f(a, x))
F(a, f(b, f(b, x''))) -> F(b, f(b, f(a, x'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
F(c, f(a, x)) -> F(c, x)
F(a, f(b, f(b, x''))) -> F(b, f(b, f(a, x'')))
F(a, f(b, x)) -> F(a, x)
F(c, f(a, x)) -> F(a, f(c, x))
F(b, f(c, x)) -> F(c, f(b, x))
F(b, f(c, x)) -> F(b, x)
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(b, f(c, x)) -> F(c, f(b, x))
F(b, f(c, f(c, x''))) -> F(c, f(c, f(b, x'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Narrowing Transformation
F(b, f(c, f(c, x''))) -> F(c, f(c, f(b, x'')))
F(b, f(c, x)) -> F(b, x)
F(a, f(b, f(b, x''))) -> F(b, f(b, f(a, x'')))
F(a, f(b, x)) -> F(a, x)
F(c, f(a, x)) -> F(a, f(c, x))
F(c, f(a, x)) -> F(c, x)
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(c, f(a, x)) -> F(a, f(c, x))
F(c, f(a, f(a, x''))) -> F(a, f(a, f(c, x'')))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Narrowing Transformation
F(b, f(c, x)) -> F(b, x)
F(a, f(b, f(b, x''))) -> F(b, f(b, f(a, x'')))
F(a, f(b, x)) -> F(a, x)
F(c, f(a, f(a, x''))) -> F(a, f(a, f(c, x'')))
F(c, f(a, x)) -> F(c, x)
F(b, f(c, f(c, x''))) -> F(c, f(c, f(b, x'')))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(a, f(b, f(b, x''))) -> F(b, f(b, f(a, x'')))
F(a, f(b, f(b, f(b, x')))) -> F(b, f(b, f(b, f(a, x'))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
F(a, f(b, f(b, f(b, x')))) -> F(b, f(b, f(b, f(a, x'))))
F(a, f(b, x)) -> F(a, x)
F(c, f(a, f(a, x''))) -> F(a, f(a, f(c, x'')))
F(c, f(a, x)) -> F(c, x)
F(b, f(c, f(c, x''))) -> F(c, f(c, f(b, x'')))
F(b, f(c, x)) -> F(b, x)
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(b, f(c, f(c, x''))) -> F(c, f(c, f(b, x'')))
F(b, f(c, f(c, f(c, x')))) -> F(c, f(c, f(c, f(b, x'))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
F(a, f(b, x)) -> F(a, x)
F(c, f(a, f(a, x''))) -> F(a, f(a, f(c, x'')))
F(c, f(a, x)) -> F(c, x)
F(b, f(c, f(c, f(c, x')))) -> F(c, f(c, f(c, f(b, x'))))
F(b, f(c, x)) -> F(b, x)
F(a, f(b, f(b, f(b, x')))) -> F(b, f(b, f(b, f(a, x'))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(c, f(a, f(a, x''))) -> F(a, f(a, f(c, x'')))
F(c, f(a, f(a, f(a, x')))) -> F(a, f(a, f(a, f(c, x'))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Polynomial Ordering
F(c, f(a, f(a, f(a, x')))) -> F(a, f(a, f(a, f(c, x'))))
F(c, f(a, x)) -> F(c, x)
F(b, f(c, f(c, f(c, x')))) -> F(c, f(c, f(c, f(b, x'))))
F(b, f(c, x)) -> F(b, x)
F(a, f(b, f(b, f(b, x')))) -> F(b, f(b, f(b, f(a, x'))))
F(a, f(b, x)) -> F(a, x)
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
F(c, f(a, x)) -> F(c, x)
F(b, f(c, x)) -> F(b, x)
F(a, f(b, x)) -> F(a, x)
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
POL(c) = 0 POL(b) = 0 POL(a) = 0 POL(f(x1, x2)) = 1 + x2 POL(F(x1, x2)) = x2
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
F(c, f(a, f(a, f(a, x')))) -> F(a, f(a, f(a, f(c, x'))))
F(b, f(c, f(c, f(c, x')))) -> F(c, f(c, f(c, f(b, x'))))
F(a, f(b, f(b, f(b, x')))) -> F(b, f(b, f(b, f(a, x'))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(a, f(b, f(b, f(b, x')))) -> F(b, f(b, f(b, f(a, x'))))
F(a, f(b, f(b, f(b, f(b, x''))))) -> F(b, f(b, f(b, f(b, f(a, x'')))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 9
↳Narrowing Transformation
F(b, f(c, f(c, f(c, x')))) -> F(c, f(c, f(c, f(b, x'))))
F(a, f(b, f(b, f(b, f(b, x''))))) -> F(b, f(b, f(b, f(b, f(a, x'')))))
F(c, f(a, f(a, f(a, x')))) -> F(a, f(a, f(a, f(c, x'))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(b, f(c, f(c, f(c, x')))) -> F(c, f(c, f(c, f(b, x'))))
F(b, f(c, f(c, f(c, f(c, x''))))) -> F(c, f(c, f(c, f(c, f(b, x'')))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 10
↳Narrowing Transformation
F(c, f(a, f(a, f(a, x')))) -> F(a, f(a, f(a, f(c, x'))))
F(b, f(c, f(c, f(c, f(c, x''))))) -> F(c, f(c, f(c, f(c, f(b, x'')))))
F(a, f(b, f(b, f(b, f(b, x''))))) -> F(b, f(b, f(b, f(b, f(a, x'')))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(c, f(a, f(a, f(a, x')))) -> F(a, f(a, f(a, f(c, x'))))
F(c, f(a, f(a, f(a, f(a, x''))))) -> F(a, f(a, f(a, f(a, f(c, x'')))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 11
↳Narrowing Transformation
F(a, f(b, f(b, f(b, f(b, x''))))) -> F(b, f(b, f(b, f(b, f(a, x'')))))
F(c, f(a, f(a, f(a, f(a, x''))))) -> F(a, f(a, f(a, f(a, f(c, x'')))))
F(b, f(c, f(c, f(c, f(c, x''))))) -> F(c, f(c, f(c, f(c, f(b, x'')))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(a, f(b, f(b, f(b, f(b, x''))))) -> F(b, f(b, f(b, f(b, f(a, x'')))))
F(a, f(b, f(b, f(b, f(b, f(b, x')))))) -> F(b, f(b, f(b, f(b, f(b, f(a, x'))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 12
↳Narrowing Transformation
F(b, f(c, f(c, f(c, f(c, x''))))) -> F(c, f(c, f(c, f(c, f(b, x'')))))
F(a, f(b, f(b, f(b, f(b, f(b, x')))))) -> F(b, f(b, f(b, f(b, f(b, f(a, x'))))))
F(c, f(a, f(a, f(a, f(a, x''))))) -> F(a, f(a, f(a, f(a, f(c, x'')))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(b, f(c, f(c, f(c, f(c, x''))))) -> F(c, f(c, f(c, f(c, f(b, x'')))))
F(b, f(c, f(c, f(c, f(c, f(c, x')))))) -> F(c, f(c, f(c, f(c, f(c, f(b, x'))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 13
↳Narrowing Transformation
F(c, f(a, f(a, f(a, f(a, x''))))) -> F(a, f(a, f(a, f(a, f(c, x'')))))
F(b, f(c, f(c, f(c, f(c, f(c, x')))))) -> F(c, f(c, f(c, f(c, f(c, f(b, x'))))))
F(a, f(b, f(b, f(b, f(b, f(b, x')))))) -> F(b, f(b, f(b, f(b, f(b, f(a, x'))))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(c, f(a, f(a, f(a, f(a, x''))))) -> F(a, f(a, f(a, f(a, f(c, x'')))))
F(c, f(a, f(a, f(a, f(a, f(a, x')))))) -> F(a, f(a, f(a, f(a, f(a, f(c, x'))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 14
↳Narrowing Transformation
F(a, f(b, f(b, f(b, f(b, f(b, x')))))) -> F(b, f(b, f(b, f(b, f(b, f(a, x'))))))
F(c, f(a, f(a, f(a, f(a, f(a, x')))))) -> F(a, f(a, f(a, f(a, f(a, f(c, x'))))))
F(b, f(c, f(c, f(c, f(c, f(c, x')))))) -> F(c, f(c, f(c, f(c, f(c, f(b, x'))))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(a, f(b, f(b, f(b, f(b, f(b, x')))))) -> F(b, f(b, f(b, f(b, f(b, f(a, x'))))))
F(a, f(b, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(b, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 15
↳Narrowing Transformation
F(b, f(c, f(c, f(c, f(c, f(c, x')))))) -> F(c, f(c, f(c, f(c, f(c, f(b, x'))))))
F(a, f(b, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(b, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(c, f(a, f(a, f(a, f(a, f(a, x')))))) -> F(a, f(a, f(a, f(a, f(a, f(c, x'))))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(b, f(c, f(c, f(c, f(c, f(c, x')))))) -> F(c, f(c, f(c, f(c, f(c, f(b, x'))))))
F(b, f(c, f(c, f(c, f(c, f(c, f(c, x''))))))) -> F(c, f(c, f(c, f(c, f(c, f(c, f(b, x'')))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 16
↳Narrowing Transformation
F(c, f(a, f(a, f(a, f(a, f(a, x')))))) -> F(a, f(a, f(a, f(a, f(a, f(c, x'))))))
F(b, f(c, f(c, f(c, f(c, f(c, f(c, x''))))))) -> F(c, f(c, f(c, f(c, f(c, f(c, f(b, x'')))))))
F(a, f(b, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(b, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))
one new Dependency Pair is created:
F(c, f(a, f(a, f(a, f(a, f(a, x')))))) -> F(a, f(a, f(a, f(a, f(a, f(c, x'))))))
F(c, f(a, f(a, f(a, f(a, f(a, f(a, x''))))))) -> F(a, f(a, f(a, f(a, f(a, f(a, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 17
↳Remaining Obligation(s)
F(a, f(b, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(b, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(c, f(a, f(a, f(a, f(a, f(a, f(a, x''))))))) -> F(a, f(a, f(a, f(a, f(a, f(a, f(c, x'')))))))
F(b, f(c, f(c, f(c, f(c, f(c, f(c, x''))))))) -> F(c, f(c, f(c, f(c, f(c, f(c, f(b, x'')))))))
f(a, f(b, x)) -> f(b, f(a, x))
f(b, f(c, x)) -> f(c, f(b, x))
f(c, f(a, x)) -> f(a, f(c, x))