R
↳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
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳Remaining
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)))
LEQ(s(X), s(Y)) -> LEQ(X, Y)
POL(LEQ(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
LEQ(x1, x2) -> LEQ(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 3
↳Dependency Graph
→DP Problem 2
↳Remaining
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)))
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Remaining Obligation(s)
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)))