R
↳Dependency Pair Analysis
PLUS(s(X), Y) > PLUS(X, Y)
MIN(s(X), s(Y)) > MIN(X, Y)
MIN(min(X, Y), Z) > MIN(X, plus(Y, Z))
MIN(min(X, Y), Z) > PLUS(Y, Z)
QUOT(s(X), s(Y)) > QUOT(min(X, Y), s(Y))
QUOT(s(X), s(Y)) > MIN(X, Y)
R
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
PLUS(s(X), Y) > PLUS(X, Y)
plus(0, Y) > Y
plus(s(X), Y) > s(plus(X, Y))
min(X, 0) > X
min(s(X), s(Y)) > min(X, Y)
min(min(X, Y), Z) > min(X, plus(Y, Z))
quot(0, s(Y)) > 0
quot(s(X), s(Y)) > s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 4
↳SizeChange Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳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)
→DP Problem 3
↳UsableRules
MIN(min(X, Y), Z) > MIN(X, plus(Y, Z))
MIN(s(X), s(Y)) > MIN(X, Y)
plus(0, Y) > Y
plus(s(X), Y) > s(plus(X, Y))
min(X, 0) > X
min(s(X), s(Y)) > min(X, Y)
min(min(X, Y), Z) > min(X, plus(Y, Z))
quot(0, s(Y)) > 0
quot(s(X), s(Y)) > s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 5
↳SizeChange Principle
→DP Problem 3
↳UsableRules
MIN(min(X, Y), Z) > MIN(X, plus(Y, Z))
MIN(s(X), s(Y)) > MIN(X, Y)
plus(s(X), Y) > s(plus(X, Y))
plus(0, Y) > Y
innermost




trivial
min(x_{1}, x_{2}) > min(x_{1}, x_{2})
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(min(X, Y), s(Y))
plus(0, Y) > Y
plus(s(X), Y) > s(plus(X, Y))
min(X, 0) > X
min(s(X), s(Y)) > min(X, Y)
min(min(X, Y), Z) > min(X, plus(Y, Z))
quot(0, s(Y)) > 0
quot(s(X), s(Y)) > s(quot(min(X, Y), s(Y)))
innermost
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 6
↳Negative Polynomial Order
QUOT(s(X), s(Y)) > QUOT(min(X, Y), s(Y))
plus(s(X), Y) > s(plus(X, Y))
plus(0, Y) > Y
min(min(X, Y), Z) > min(X, plus(Y, Z))
min(s(X), s(Y)) > min(X, Y)
min(X, 0) > X
innermost
QUOT(s(X), s(Y)) > QUOT(min(X, Y), s(Y))
plus(s(X), Y) > s(plus(X, Y))
plus(0, Y) > Y
min(min(X, Y), Z) > min(X, plus(Y, Z))
min(s(X), s(Y)) > min(X, Y)
min(X, 0) > X
POL( QUOT(x_{1}, x_{2}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( min(x_{1}, x_{2}) ) = x_{1}
POL( plus(x_{1}, x_{2}) ) = x_{1} + x_{2}
R
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
→DP Problem 6
↳Neg POLO
...
→DP Problem 7
↳Dependency Graph
plus(s(X), Y) > s(plus(X, Y))
plus(0, Y) > Y
min(min(X, Y), Z) > min(X, plus(Y, Z))
min(s(X), s(Y)) > min(X, Y)
min(X, 0) > X
innermost