R
↳Dependency Pair Analysis
QUOT(s(x), s(y), z) > QUOT(x, y, z)
QUOT(x, 0, s(z)) > QUOT(x, plus(z, s(0)), s(z))
QUOT(x, 0, s(z)) > PLUS(z, s(0))
PLUS(s(x), y) > PLUS(x, y)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
PLUS(s(x), y) > PLUS(x, y)
quot(0, s(y), s(z)) > 0
quot(s(x), s(y), z) > quot(x, y, z)
quot(x, 0, s(z)) > s(quot(x, plus(z, s(0)), s(z)))
plus(0, y) > y
plus(s(x), y) > s(plus(x, y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 3
↳SizeChange Principle
→DP Problem 2
↳UsableRules
PLUS(s(x), y) > PLUS(x, y)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
QUOT(x, 0, s(z)) > QUOT(x, plus(z, s(0)), s(z))
QUOT(s(x), s(y), z) > QUOT(x, y, z)
quot(0, s(y), s(z)) > 0
quot(s(x), s(y), z) > quot(x, y, z)
quot(x, 0, s(z)) > s(quot(x, plus(z, s(0)), s(z)))
plus(0, y) > y
plus(s(x), y) > s(plus(x, y))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Negative Polynomial Order
QUOT(x, 0, s(z)) > QUOT(x, plus(z, s(0)), s(z))
QUOT(s(x), s(y), z) > QUOT(x, y, z)
plus(s(x), y) > s(plus(x, y))
plus(0, y) > y
innermost
QUOT(s(x), s(y), z) > QUOT(x, y, z)
plus(s(x), y) > s(plus(x, y))
plus(0, y) > y
POL( QUOT(x_{1}, ..., x_{3}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( plus(x_{1}, x_{2}) ) = x_{1} + x_{2}
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 4
↳Neg POLO
...
→DP Problem 5
↳Narrowing Transformation
QUOT(x, 0, s(z)) > QUOT(x, plus(z, s(0)), s(z))
plus(s(x), y) > s(plus(x, y))
plus(0, y) > y
innermost
two new Dependency Pairs are created:
QUOT(x, 0, s(z)) > QUOT(x, plus(z, s(0)), s(z))
QUOT(x, 0, s(s(x''))) > QUOT(x, s(plus(x'', s(0))), s(s(x'')))
QUOT(x, 0, s(0)) > QUOT(x, s(0), s(0))