R
↳Overlay and local confluence Check
R
↳OC
→TRS2
↳Dependency Pair Analysis
'(s(x), s(y)) > '(x, y)
LT(s(x), s(y)) > LT(x, y)
DIV(s(x), s(y)) > IF(lt(x, y), 0, s(div((x, y), s(y))))
DIV(s(x), s(y)) > LT(x, y)
DIV(s(x), s(y)) > DIV((x, y), s(y))
DIV(s(x), s(y)) > '(x, y)
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
'(s(x), s(y)) > '(x, y)
(x, 0) > x
(0, s(y)) > 0
(s(x), s(y)) > (x, y)
lt(x, 0) > false
lt(0, s(y)) > true
lt(s(x), s(y)) > lt(x, y)
if(true, x, y) > x
if(false, x, y) > y
div(x, 0) > 0
div(0, y) > 0
div(s(x), s(y)) > if(lt(x, y), 0, s(div((x, y), s(y))))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 4
↳SizeChange Principle
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
'(s(x), s(y)) > '(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
LT(s(x), s(y)) > LT(x, y)
(x, 0) > x
(0, s(y)) > 0
(s(x), s(y)) > (x, y)
lt(x, 0) > false
lt(0, s(y)) > true
lt(s(x), s(y)) > lt(x, y)
if(true, x, y) > x
if(false, x, y) > y
div(x, 0) > 0
div(0, y) > 0
div(s(x), s(y)) > if(lt(x, y), 0, s(div((x, y), s(y))))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 5
↳SizeChange Principle
→DP Problem 3
↳UsableRules
LT(s(x), s(y)) > LT(x, y)
none
innermost


trivial
s(x_{1}) > s(x_{1})
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳Usable Rules (Innermost)
DIV(s(x), s(y)) > DIV((x, y), s(y))
(x, 0) > x
(0, s(y)) > 0
(s(x), s(y)) > (x, y)
lt(x, 0) > false
lt(0, s(y)) > true
lt(s(x), s(y)) > lt(x, y)
if(true, x, y) > x
if(false, x, y) > y
div(x, 0) > 0
div(0, y) > 0
div(s(x), s(y)) > if(lt(x, y), 0, s(div((x, y), s(y))))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
...
→DP Problem 6
↳Negative Polynomial Order
DIV(s(x), s(y)) > DIV((x, y), s(y))
(s(x), s(y)) > (x, y)
(x, 0) > x
(0, s(y)) > 0
innermost
DIV(s(x), s(y)) > DIV((x, y), s(y))
(s(x), s(y)) > (x, y)
(x, 0) > x
(0, s(y)) > 0
POL( DIV(x_{1}, x_{2}) ) = x_{1}
POL( s(x_{1}) ) = x_{1} + 1
POL( (x_{1}, x_{2}) ) = x_{1}
POL( 0 ) = 0
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
→DP Problem 3
↳UsableRules
...
→DP Problem 7
↳Dependency Graph
(s(x), s(y)) > (x, y)
(x, 0) > x
(0, s(y)) > 0
innermost