R
↳Dependency Pair Analysis
MINUS(s(X), s(Y)) > P(minus(X, Y))
MINUS(s(X), s(Y)) > MINUS(X, Y)
DIV(s(X), s(Y)) > DIV(minus(X, Y), s(Y))
DIV(s(X), s(Y)) > MINUS(X, Y)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
MINUS(s(X), s(Y)) > MINUS(X, Y)
minus(X, 0) > X
minus(s(X), s(Y)) > p(minus(X, Y))
p(s(X)) > X
div(0, s(Y)) > 0
div(s(X), s(Y)) > s(div(minus(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 3
↳SizeChange Principle
→DP Problem 2
↳UsableRules
MINUS(s(X), s(Y)) > MINUS(X, Y)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
DIV(s(X), s(Y)) > DIV(minus(X, Y), s(Y))
minus(X, 0) > X
minus(s(X), s(Y)) > p(minus(X, Y))
p(s(X)) > X
div(0, s(Y)) > 0
div(s(X), s(Y)) > s(div(minus(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Negative Polynomial Order
DIV(s(X), s(Y)) > DIV(minus(X, Y), s(Y))
p(s(X)) > X
minus(X, 0) > X
minus(s(X), s(Y)) > p(minus(X, Y))
innermost
DIV(s(X), s(Y)) > DIV(minus(X, Y), s(Y))
p(s(X)) > X
minus(X, 0) > X
minus(s(X), s(Y)) > p(minus(X, Y))
POL( DIV(x_{1}, x_{2}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( minus(x_{1}, x_{2}) ) = x_{1}
POL( p(x_{1}) ) = x_{1}
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Neg POLO
...
→DP Problem 5
↳Dependency Graph
p(s(X)) > X
minus(X, 0) > X
minus(s(X), s(Y)) > p(minus(X, Y))
innermost