R
↳Overlay and local confluence Check
R
↳OC
→TRS2
↳Dependency Pair Analysis
MINUS(x, s(y)) > PRED(minus(x, y))
MINUS(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)
LOG(s(s(x))) > LOG(s(quot(x, s(s(0)))))
LOG(s(s(x))) > QUOT(x, s(s(0)))
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
MINUS(x, s(y)) > MINUS(x, y)
pred(s(x)) > x
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(x, y), s(y)))
log(s(0)) > 0
log(s(s(x))) > s(log(s(quot(x, s(s(0))))))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 4
↳SizeChange Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
MINUS(x, s(y)) > MINUS(x, y)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳Usable Rules (Innermost)
→DP Problem 3
↳UsableRules
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
pred(s(x)) > x
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(x, y), s(y)))
log(s(0)) > 0
log(s(s(x))) > s(log(s(quot(x, s(s(0))))))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 5
↳Negative Polynomial Order
→DP Problem 3
↳UsableRules
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
pred(s(x)) > x
innermost
QUOT(s(x), s(y)) > QUOT(minus(x, y), s(y))
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
pred(s(x)) > x
POL( QUOT(x_{1}, x_{2}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( minus(x_{1}, x_{2}) ) = x_{1}
POL( pred(x_{1}) ) = x_{1}
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 6
↳Dependency Graph
→DP Problem 3
↳UsableRules
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
pred(s(x)) > x
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
LOG(s(s(x))) > LOG(s(quot(x, s(s(0)))))
pred(s(x)) > x
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(x, y), s(y)))
log(s(0)) > 0
log(s(s(x))) > s(log(s(quot(x, s(s(0))))))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
...
→DP Problem 7
↳Negative Polynomial Order
LOG(s(s(x))) > LOG(s(quot(x, s(s(0)))))
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(x, y), s(y)))
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
pred(s(x)) > x
innermost
LOG(s(s(x))) > LOG(s(quot(x, s(s(0)))))
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(x, y), s(y)))
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
pred(s(x)) > x
POL( LOG(x_{1}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( quot(x_{1}, x_{2}) ) = x_{1}
POL( 0 ) = 0
POL( minus(x_{1}, x_{2}) ) = x_{1}
POL( pred(x_{1}) ) = x_{1}
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
...
→DP Problem 8
↳Dependency Graph
quot(0, s(y)) > 0
quot(s(x), s(y)) > s(quot(minus(x, y), s(y)))
minus(x, 0) > x
minus(x, s(y)) > pred(minus(x, y))
pred(s(x)) > x
innermost