R
↳Dependency Pair Analysis
F(a, x) -> F(b, f(c, x))
F(a, x) -> F(c, x)
F(a, f(b, x)) -> F(b, f(a, x))
F(a, f(b, x)) -> F(a, x)
F(d, f(c, x)) -> F(d, f(a, x))
F(d, f(c, x)) -> F(a, x)
F(a, f(c, x)) -> F(c, f(a, x))
F(a, f(c, x)) -> F(a, x)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Nar
F(a, f(c, x)) -> F(a, x)
F(a, f(b, x)) -> F(a, x)
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
F(a, f(c, x)) -> F(a, x)
F(a, f(b, x)) -> F(a, x)
F(x1, x2) -> F(x1, x2)
f(x1, x2) -> f(x1, x2)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Nar
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Narrowing Transformation
F(d, f(c, x)) -> F(d, f(a, x))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, x)) -> F(d, f(a, x))
F(d, f(c, x'')) -> F(d, f(b, f(c, x'')))
F(d, f(c, f(b, x''))) -> F(d, f(b, f(a, x'')))
F(d, f(c, f(c, x''))) -> F(d, f(c, f(a, x'')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Narrowing Transformation
F(d, f(c, f(c, x''))) -> F(d, f(c, f(a, x'')))
F(d, f(c, f(b, x''))) -> F(d, f(b, f(a, x'')))
F(d, f(c, x'')) -> F(d, f(b, f(c, x'')))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, x'')) -> F(d, f(b, f(c, x'')))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 5
↳Narrowing Transformation
F(d, f(c, f(b, x''))) -> F(d, f(b, f(a, x'')))
F(d, f(c, f(c, x''))) -> F(d, f(c, f(a, x'')))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, x''))) -> F(d, f(b, f(a, x'')))
F(d, f(c, f(b, x'''))) -> F(d, f(b, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, x')))) -> F(d, f(b, f(b, f(a, x'))))
F(d, f(c, f(b, f(c, x')))) -> F(d, f(b, f(c, f(a, x'))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 6
↳Narrowing Transformation
F(d, f(c, f(b, f(c, x')))) -> F(d, f(b, f(c, f(a, x'))))
F(d, f(c, f(b, f(b, x')))) -> F(d, f(b, f(b, f(a, x'))))
F(d, f(c, f(b, x'''))) -> F(d, f(b, f(b, f(c, x'''))))
F(d, f(c, f(c, x''))) -> F(d, f(c, f(a, x'')))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(c, x''))) -> F(d, f(c, f(a, x'')))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, x')))) -> F(d, f(c, f(b, f(a, x'))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 7
↳Narrowing Transformation
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, f(b, x')))) -> F(d, f(c, f(b, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, x')))) -> F(d, f(b, f(b, f(a, x'))))
F(d, f(c, f(b, x'''))) -> F(d, f(b, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, x')))) -> F(d, f(b, f(c, f(a, x'))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, x'''))) -> F(d, f(b, f(b, f(c, x'''))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 8
↳Narrowing Transformation
F(d, f(c, f(c, f(b, x')))) -> F(d, f(c, f(b, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, x')))) -> F(d, f(b, f(c, f(a, x'))))
F(d, f(c, f(b, f(b, x')))) -> F(d, f(b, f(b, f(a, x'))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(b, x')))) -> F(d, f(b, f(b, f(a, x'))))
F(d, f(c, f(b, f(b, x'')))) -> F(d, f(b, f(b, f(b, f(c, x'')))))
F(d, f(c, f(b, f(b, f(b, x''))))) -> F(d, f(b, f(b, f(b, f(a, x'')))))
F(d, f(c, f(b, f(b, f(c, x''))))) -> F(d, f(b, f(b, f(c, f(a, x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 9
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(c, x''))))) -> F(d, f(b, f(b, f(c, f(a, x'')))))
F(d, f(c, f(b, f(b, f(b, x''))))) -> F(d, f(b, f(b, f(b, f(a, x'')))))
F(d, f(c, f(b, f(b, x'')))) -> F(d, f(b, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, x')))) -> F(d, f(b, f(c, f(a, x'))))
F(d, f(c, f(c, f(b, x')))) -> F(d, f(c, f(b, f(a, x'))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(c, x')))) -> F(d, f(b, f(c, f(a, x'))))
F(d, f(c, f(b, f(c, x'')))) -> F(d, f(b, f(c, f(b, f(c, x'')))))
F(d, f(c, f(b, f(c, f(b, x''))))) -> F(d, f(b, f(c, f(b, f(a, x'')))))
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 10
↳Narrowing Transformation
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
F(d, f(c, f(b, f(c, f(b, x''))))) -> F(d, f(b, f(c, f(b, f(a, x'')))))
F(d, f(c, f(b, f(c, x'')))) -> F(d, f(b, f(c, f(b, f(c, x'')))))
F(d, f(c, f(b, f(b, f(b, x''))))) -> F(d, f(b, f(b, f(b, f(a, x'')))))
F(d, f(c, f(b, f(b, x'')))) -> F(d, f(b, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, f(b, x')))) -> F(d, f(c, f(b, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(c, x''))))) -> F(d, f(b, f(b, f(c, f(a, x'')))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(c, f(b, x')))) -> F(d, f(c, f(b, f(a, x'))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 11
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(b, f(c, f(b, x''))))) -> F(d, f(b, f(c, f(b, f(a, x'')))))
F(d, f(c, f(b, f(c, x'')))) -> F(d, f(b, f(c, f(b, f(c, x'')))))
F(d, f(c, f(b, f(b, f(c, x''))))) -> F(d, f(b, f(b, f(c, f(a, x'')))))
F(d, f(c, f(b, f(b, f(b, x''))))) -> F(d, f(b, f(b, f(b, f(a, x'')))))
F(d, f(c, f(b, f(b, x'')))) -> F(d, f(b, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(b, x'')))) -> F(d, f(b, f(b, f(b, f(c, x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 12
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
F(d, f(c, f(b, f(c, f(b, x''))))) -> F(d, f(b, f(c, f(b, f(a, x'')))))
F(d, f(c, f(b, f(c, x'')))) -> F(d, f(b, f(c, f(b, f(c, x'')))))
F(d, f(c, f(b, f(b, f(c, x''))))) -> F(d, f(b, f(b, f(c, f(a, x'')))))
F(d, f(c, f(b, f(b, f(b, x''))))) -> F(d, f(b, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(b, f(b, x''))))) -> F(d, f(b, f(b, f(b, f(a, x'')))))
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 13
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
F(d, f(c, f(b, f(c, f(b, x''))))) -> F(d, f(b, f(c, f(b, f(a, x'')))))
F(d, f(c, f(b, f(c, x'')))) -> F(d, f(b, f(c, f(b, f(c, x'')))))
F(d, f(c, f(b, f(b, f(c, x''))))) -> F(d, f(b, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(b, f(c, x''))))) -> F(d, f(b, f(b, f(c, f(a, x'')))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 14
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
F(d, f(c, f(b, f(c, f(b, x''))))) -> F(d, f(b, f(c, f(b, f(a, x'')))))
F(d, f(c, f(b, f(c, x'')))) -> F(d, f(b, f(c, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(c, x'')))) -> F(d, f(b, f(c, f(b, f(c, x'')))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 15
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
F(d, f(c, f(b, f(c, f(b, x''))))) -> F(d, f(b, f(c, f(b, f(a, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(c, f(b, x''))))) -> F(d, f(b, f(c, f(b, f(a, x'')))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 16
↳Narrowing Transformation
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(c, f(c, x''))))) -> F(d, f(b, f(c, f(c, f(a, x'')))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 17
↳Narrowing Transformation
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(c, f(b, f(b, x''))))) -> F(d, f(c, f(b, f(b, f(a, x'')))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 18
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(c, f(b, f(c, x''))))) -> F(d, f(c, f(b, f(c, f(a, x'')))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 19
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(b, f(b, x'''))))) -> F(d, f(b, f(b, f(b, f(b, f(c, x'''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 20
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(b, f(b, f(b, x')))))) -> F(d, f(b, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 21
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(b, f(b, f(c, x')))))) -> F(d, f(b, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 22
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(b, f(c, x'''))))) -> F(d, f(b, f(b, f(c, f(b, f(c, x'''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 23
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(b, f(c, f(b, x')))))) -> F(d, f(b, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 24
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(b, f(c, f(c, x')))))) -> F(d, f(b, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 25
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(c, f(b, x'''))))) -> F(d, f(b, f(c, f(b, f(b, f(c, x'''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 26
↳Narrowing Transformation
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(c, f(b, f(b, x')))))) -> F(d, f(b, f(c, f(b, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 27
↳Narrowing Transformation
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(c, f(b, f(c, x')))))) -> F(d, f(b, f(c, f(b, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 28
↳Narrowing Transformation
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(c, f(c, x'''))))) -> F(d, f(b, f(c, f(c, f(b, f(c, x'''))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 29
↳Narrowing Transformation
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(c, f(c, f(b, x')))))) -> F(d, f(b, f(c, f(c, f(b, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 30
↳Narrowing Transformation
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(b, f(c, f(c, f(c, x')))))) -> F(d, f(b, f(c, f(c, f(c, f(a, x'))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 31
↳Narrowing Transformation
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(c, f(b, f(b, f(b, x')))))) -> F(d, f(c, f(b, f(b, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 32
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(c, f(b, f(b, f(c, x')))))) -> F(d, f(c, f(b, f(b, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 33
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(c, f(b, f(c, f(b, x')))))) -> F(d, f(c, f(b, f(c, f(b, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 34
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
three new Dependency Pairs are created:
F(d, f(c, f(c, f(b, f(c, f(c, x')))))) -> F(d, f(c, f(b, f(c, f(c, f(a, x'))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 35
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(b, f(b, f(b, x'')))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 36
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(b, f(b, f(c, x'')))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 37
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(b, f(c, f(b, x'')))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 38
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(b, f(c, f(c, x'')))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 39
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(c, f(b, f(b, x'')))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 40
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(c, f(b, f(c, x'')))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 41
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(c, f(c, f(b, x'')))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 42
↳Narrowing Transformation
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))
no new Dependency Pairs are created.
F(d, f(c, f(b, f(c, f(c, f(c, x'')))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(c, x'')))))))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Nar
→DP Problem 4
↳Nar
...
→DP Problem 43
↳Remaining Obligation(s)
F(d, f(c, f(c, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(c, x'')))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, f(b, x'')))))) -> F(d, f(c, f(b, f(c, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(c, x'')))))) -> F(d, f(c, f(b, f(b, f(c, f(b, f(c, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(b, f(b, x'')))))) -> F(d, f(c, f(b, f(b, f(b, f(b, f(c, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(c, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(c, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(c, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(c, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(c, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(c, f(b, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(c, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(c, f(a, x'')))))))
F(d, f(c, f(b, f(b, f(b, f(b, f(b, x''))))))) -> F(d, f(b, f(b, f(b, f(b, f(b, f(a, x'')))))))
F(d, f(c, f(c, f(b, f(c, x'''))))) -> F(d, f(c, f(b, f(c, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, f(b, x'''))))) -> F(d, f(c, f(b, f(b, f(b, f(c, x'''))))))
F(d, f(c, f(c, f(b, x'')))) -> F(d, f(c, f(b, f(b, f(c, x'')))))
F(d, f(c, f(c, f(c, x')))) -> F(d, f(c, f(c, f(a, x'))))
F(d, f(c, f(c, x'''))) -> F(d, f(c, f(b, f(c, x'''))))
F(d, f(c, f(c, f(b, f(c, f(c, f(b, x''))))))) -> F(d, f(c, f(b, f(c, f(c, f(b, f(a, x'')))))))
f(a, x) -> f(b, f(c, x))
f(a, f(b, x)) -> f(b, f(a, x))
f(d, f(c, x)) -> f(d, f(a, x))
f(a, f(c, x)) -> f(c, f(a, x))