R
↳Dependency Pair Analysis
MINUS(s(x), s(y)) > MINUS(x, y)
LE(s(x), s(y)) > LE(x, y)
QUOT(s(x), s(y)) > QUOT(minus(s(x), s(y)), s(y))
QUOT(s(x), s(y)) > MINUS(s(x), s(y))
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
MINUS(s(x), s(y)) > MINUS(x, y)
minus(x, 0) > x
minus(s(x), s(y)) > minus(x, y)
le(0, y) > true
le(s(x), 0) > false
le(s(x), s(y)) > le(x, y)
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(s(x), s(y)), s(y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳SizeChange Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳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)
→DP Problem 3
↳UsableRules
LE(s(x), s(y)) > LE(x, y)
minus(x, 0) > x
minus(s(x), s(y)) > minus(x, y)
le(0, y) > true
le(s(x), 0) > false
le(s(x), s(y)) > le(x, y)
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(s(x), s(y)), s(y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 5
↳SizeChange Principle
→DP Problem 3
↳UsableRules
LE(s(x), s(y)) > LE(x, y)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
QUOT(s(x), s(y)) > QUOT(minus(s(x), s(y)), s(y))
minus(x, 0) > x
minus(s(x), s(y)) > minus(x, y)
le(0, y) > true
le(s(x), 0) > false
le(s(x), s(y)) > le(x, y)
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(s(x), s(y)), s(y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 6
↳Rewriting Transformation
QUOT(s(x), s(y)) > QUOT(minus(s(x), s(y)), s(y))
minus(s(x), s(y)) > minus(x, y)
minus(x, 0) > x
innermost
one new Dependency Pair is created:
QUOT(s(x), s(y)) > QUOT(minus(s(x), s(y)), s(y))
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 6
↳Rw
...
→DP Problem 7
↳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 3
↳UsableRules
→DP Problem 6
↳Rw
...
→DP Problem 8
↳Dependency Graph
minus(s(x), s(y)) > minus(x, y)
minus(x, 0) > x
innermost