R
↳Overlay and local confluence Check
R
↳OC
→TRS2
↳Dependency Pair Analysis
LE(s(x), s(y)) > LE(x, y)
MINUS(x, s(y)) > IF(le(x, s(y)), 0, p(minus(x, p(s(y)))))
MINUS(x, s(y)) > LE(x, s(y))
MINUS(x, s(y)) > P(minus(x, p(s(y))))
MINUS(x, s(y)) > MINUS(x, p(s(y)))
MINUS(x, s(y)) > P(s(y))
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
LE(s(x), s(y)) > LE(x, y)
p(0) > 0
p(s(x)) > x
le(0, y) > true
le(s(x), 0) > false
le(s(x), s(y)) > le(x, y)
minus(x, 0) > x
minus(x, s(y)) > if(le(x, s(y)), 0, p(minus(x, p(s(y)))))
if(true, x, y) > x
if(false, x, y) > y
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 3
↳SizeChange Principle
→DP Problem 2
↳UsableRules
LE(s(x), s(y)) > LE(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)
MINUS(x, s(y)) > MINUS(x, p(s(y)))
p(0) > 0
p(s(x)) > x
le(0, y) > true
le(s(x), 0) > false
le(s(x), s(y)) > le(x, y)
minus(x, 0) > x
minus(x, s(y)) > if(le(x, s(y)), 0, p(minus(x, p(s(y)))))
if(true, x, y) > x
if(false, x, y) > y
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 4
↳Rewriting Transformation
MINUS(x, s(y)) > MINUS(x, p(s(y)))
p(s(x)) > x
innermost
one new Dependency Pair is created:
MINUS(x, s(y)) > MINUS(x, p(s(y)))
MINUS(x, s(y)) > MINUS(x, y)
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 5
↳Usable Rules (Innermost)
MINUS(x, s(y)) > MINUS(x, y)
p(s(x)) > x
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 6
↳SizeChange Principle
MINUS(x, s(y)) > MINUS(x, y)
none
innermost


trivial
s(x_{1}) > s(x_{1})