R
↳Overlay and local confluence Check
R
↳OC
→TRS2
↳Dependency Pair Analysis
LEQ(s(X), s(Y)) > LEQ(X, Y)
DIFF(X, Y) > IF(leq(X, Y), 0, s(diff(p(X), Y)))
DIFF(X, Y) > LEQ(X, Y)
DIFF(X, Y) > DIFF(p(X), Y)
DIFF(X, Y) > P(X)
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳Usable Rules (Innermost)
→DP Problem 2
↳UsableRules
LEQ(s(X), s(Y)) > LEQ(X, Y)
p(0) > 0
p(s(X)) > X
leq(0, Y) > true
leq(s(X), 0) > false
leq(s(X), s(Y)) > leq(X, Y)
if(true, X, Y) > X
if(false, X, Y) > Y
diff(X, Y) > if(leq(X, Y), 0, s(diff(p(X), Y)))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
...
→DP Problem 3
↳SizeChange Principle
→DP Problem 2
↳UsableRules
LEQ(s(X), s(Y)) > LEQ(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)
DIFF(X, Y) > DIFF(p(X), Y)
p(0) > 0
p(s(X)) > X
leq(0, Y) > true
leq(s(X), 0) > false
leq(s(X), s(Y)) > leq(X, Y)
if(true, X, Y) > X
if(false, X, Y) > Y
diff(X, Y) > if(leq(X, Y), 0, s(diff(p(X), Y)))
innermost
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 4
↳Modular Removal of Rules
DIFF(X, Y) > DIFF(p(X), Y)
p(s(X)) > X
p(0) > 0
innermost
To remove rules and DPs from this DP problem we used the following monotonic and C_{E}compatible order: Polynomial ordering.
p(s(X)) > X
p(0) > 0
_{ }^{ }POL(DIFF(x_{1}, x_{2})) = x_{1} + x_{2}_{ }^{ } _{ }^{ }POL(0) = 0_{ }^{ } _{ }^{ }POL(s(x_{1})) = x_{1}_{ }^{ } _{ }^{ }POL(p(x_{1})) = x_{1}_{ }^{ }
p(s(X)) > X
R
↳OC
→TRS2
↳DPs
→DP Problem 1
↳UsableRules
→DP Problem 2
↳UsableRules
...
→DP Problem 5
↳Non Termination
DIFF(X, Y) > DIFF(p(X), Y)
p(0) > 0
innermost
DIFF(X, Y) > DIFF(p(X), Y)
p(0) > 0