R
↳Dependency Pair Analysis
C(b(a(X))) -> A(a(b(b(c(c(X))))))
C(b(a(X))) -> A(b(b(c(c(X)))))
C(b(a(X))) -> B(b(c(c(X))))
C(b(a(X))) -> B(c(c(X)))
C(b(a(X))) -> C(c(X))
C(b(a(X))) -> C(X)
R
↳DPs
→DP Problem 1
↳Narrowing Transformation
C(b(a(X))) -> C(X)
C(b(a(X))) -> C(c(X))
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
two new Dependency Pairs are created:
C(b(a(X))) -> C(c(X))
C(b(a(b(a(X''))))) -> C(a(a(b(b(c(c(X'')))))))
C(b(a(X''))) -> C(e)
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Narrowing Transformation
C(b(a(b(a(X''))))) -> C(a(a(b(b(c(c(X'')))))))
C(b(a(X))) -> C(X)
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
seven new Dependency Pairs are created:
C(b(a(b(a(X''))))) -> C(a(a(b(b(c(c(X'')))))))
C(b(a(b(a(X'''))))) -> C(e)
C(b(a(b(a(X'''))))) -> C(a(e))
C(b(a(b(a(X'''))))) -> C(a(a(e)))
C(b(a(b(a(X'''))))) -> C(a(a(b(e))))
C(b(a(b(a(X'''))))) -> C(a(a(b(b(e)))))
C(b(a(b(a(b(a(X'))))))) -> C(a(a(b(b(c(a(a(b(b(c(c(X'))))))))))))
C(b(a(b(a(X'''))))) -> C(a(a(b(b(c(e))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 3
↳Forward Instantiation Transformation
C(b(a(b(a(X'''))))) -> C(a(a(b(b(c(e))))))
C(b(a(b(a(b(a(X'))))))) -> C(a(a(b(b(c(a(a(b(b(c(c(X'))))))))))))
C(b(a(b(a(X'''))))) -> C(a(a(b(b(e)))))
C(b(a(b(a(X'''))))) -> C(a(a(b(e))))
C(b(a(b(a(X'''))))) -> C(a(a(e)))
C(b(a(b(a(X'''))))) -> C(a(e))
C(b(a(X))) -> C(X)
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
no new Dependency Pairs are created.
C(b(a(b(a(X'''))))) -> C(a(e))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 4
↳Forward Instantiation Transformation
C(b(a(b(a(b(a(X'))))))) -> C(a(a(b(b(c(a(a(b(b(c(c(X'))))))))))))
C(b(a(b(a(X'''))))) -> C(a(a(b(b(e)))))
C(b(a(b(a(X'''))))) -> C(a(a(b(e))))
C(b(a(b(a(X'''))))) -> C(a(a(e)))
C(b(a(X))) -> C(X)
C(b(a(b(a(X'''))))) -> C(a(a(b(b(c(e))))))
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
no new Dependency Pairs are created.
C(b(a(b(a(X'''))))) -> C(a(a(e)))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 5
↳Forward Instantiation Transformation
C(b(a(b(a(X'''))))) -> C(a(a(b(b(c(e))))))
C(b(a(b(a(X'''))))) -> C(a(a(b(b(e)))))
C(b(a(b(a(X'''))))) -> C(a(a(b(e))))
C(b(a(X))) -> C(X)
C(b(a(b(a(b(a(X'))))))) -> C(a(a(b(b(c(a(a(b(b(c(c(X'))))))))))))
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
no new Dependency Pairs are created.
C(b(a(b(a(X'''))))) -> C(a(a(b(e))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 6
↳Forward Instantiation Transformation
C(b(a(b(a(b(a(X'))))))) -> C(a(a(b(b(c(a(a(b(b(c(c(X'))))))))))))
C(b(a(b(a(X'''))))) -> C(a(a(b(b(e)))))
C(b(a(X))) -> C(X)
C(b(a(b(a(X'''))))) -> C(a(a(b(b(c(e))))))
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
no new Dependency Pairs are created.
C(b(a(b(a(X'''))))) -> C(a(a(b(b(e)))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 7
↳Forward Instantiation Transformation
C(b(a(b(a(X'''))))) -> C(a(a(b(b(c(e))))))
C(b(a(X))) -> C(X)
C(b(a(b(a(b(a(X'))))))) -> C(a(a(b(b(c(a(a(b(b(c(c(X'))))))))))))
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
no new Dependency Pairs are created.
C(b(a(b(a(b(a(X'))))))) -> C(a(a(b(b(c(a(a(b(b(c(c(X'))))))))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 8
↳Forward Instantiation Transformation
C(b(a(X))) -> C(X)
C(b(a(b(a(X'''))))) -> C(a(a(b(b(c(e))))))
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
no new Dependency Pairs are created.
C(b(a(b(a(X'''))))) -> C(a(a(b(b(c(e))))))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 9
↳Forward Instantiation Transformation
C(b(a(X))) -> C(X)
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
one new Dependency Pair is created:
C(b(a(X))) -> C(X)
C(b(a(b(x'')))) -> C(b(x''))
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 10
↳Polynomial Ordering
C(b(a(b(x'')))) -> C(b(x''))
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e
C(b(a(b(x'')))) -> C(b(x''))
b(X) -> e
POL(C(x1)) = 1 + x1 POL(e) = 0 POL(b(x1)) = x1 POL(a(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Nar
→DP Problem 2
↳Nar
...
→DP Problem 11
↳Dependency Graph
c(b(a(X))) -> a(a(b(b(c(c(X))))))
c(X) -> e
a(X) -> e
b(X) -> e