R
↳Overlay and local confluence Check
R
↳OC
→TRS2
↳Dependency Pair Analysis
MIN(s(X), s(Y)) > MIN(X, Y)
QUOT(s(X), s(Y)) > QUOT(min(X, Y), s(Y))
QUOT(s(X), s(Y)) > MIN(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
MIN(s(X), s(Y)) > MIN(X, Y)
min(X, 0) > X
min(s(X), s(Y)) > min(X, Y)
quot(0, s(Y)) > 0
quot(s(X), s(Y)) > s(quot(min(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
MIN(s(X), s(Y)) > MIN(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(min(X, Y), s(Y))
min(X, 0) > X
min(s(X), s(Y)) > min(X, Y)
quot(0, s(Y)) > 0
quot(s(X), s(Y)) > s(quot(min(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(min(X, Y), s(Y))
min(s(X), s(Y)) > min(X, Y)
min(X, 0) > X
innermost
QUOT(s(X), s(Y)) > QUOT(min(X, Y), s(Y))
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}
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 6
↳Dependency Graph
→DP Problem 3
↳UsableRules
min(s(X), s(Y)) > min(X, Y)
min(X, 0) > 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)))))
min(X, 0) > X
min(s(X), s(Y)) > min(X, Y)
quot(0, s(Y)) > 0
quot(s(X), s(Y)) > s(quot(min(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(min(X, Y), s(Y)))
min(s(X), s(Y)) > min(X, Y)
min(X, 0) > 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(min(X, Y), s(Y)))
min(s(X), s(Y)) > min(X, Y)
min(X, 0) > 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( min(x_{1}, x_{2}) ) = 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(min(X, Y), s(Y)))
min(s(X), s(Y)) > min(X, Y)
min(X, 0) > X
innermost