R
↳Dependency Pair Analysis
MINUS(s(x), s(y)) > MINUS(x, y)
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
QUOT(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)) > minus(x, y)
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(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)
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
minus(x, 0) > x
minus(s(x), s(y)) > minus(x, y)
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(x, y), s(y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Negative Polynomial Order
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
minus(s(x), s(y)) > minus(x, y)
minus(x, 0) > x
innermost
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
minus(s(x), s(y)) > minus(x, y)
minus(x, 0) > x
POL( QUOT(x_{1}, x_{2}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( minus(x_{1}, x_{2}) ) = x_{1}
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Neg POLO
...
→DP Problem 5
↳Dependency Graph
minus(s(x), s(y)) > minus(x, y)
minus(x, 0) > x
innermost