R
↳Dependency Pair Analysis
MINUS(s(X), s(Y)) -> MINUS(X, Y)
GEQ(s(X), s(Y)) -> GEQ(X, Y)
DIV(s(X), s(Y)) -> IF(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
DIV(s(X), s(Y)) -> GEQ(X, Y)
DIV(s(X), s(Y)) -> DIV(minus(X, Y), s(Y))
DIV(s(X), s(Y)) -> MINUS(X, Y)
R
↳DPs
→DP Problem 1
↳Argument Filtering and Ordering
→DP Problem 2
↳AFS
→DP Problem 3
↳FwdInst
MINUS(s(X), s(Y)) -> MINUS(X, Y)
minus(0, Y) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
geq(X, 0) -> true
geq(0, s(Y)) -> false
geq(s(X), s(Y)) -> geq(X, Y)
div(0, s(Y)) -> 0
div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) -> X
if(false, X, Y) -> Y
innermost
MINUS(s(X), s(Y)) -> MINUS(X, Y)
POL(MINUS(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
MINUS(x1, x2) -> MINUS(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳AFS
→DP Problem 3
↳FwdInst
minus(0, Y) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
geq(X, 0) -> true
geq(0, s(Y)) -> false
geq(s(X), s(Y)) -> geq(X, Y)
div(0, s(Y)) -> 0
div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) -> X
if(false, X, Y) -> Y
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳Argument Filtering and Ordering
→DP Problem 3
↳FwdInst
GEQ(s(X), s(Y)) -> GEQ(X, Y)
minus(0, Y) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
geq(X, 0) -> true
geq(0, s(Y)) -> false
geq(s(X), s(Y)) -> geq(X, Y)
div(0, s(Y)) -> 0
div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) -> X
if(false, X, Y) -> Y
innermost
GEQ(s(X), s(Y)) -> GEQ(X, Y)
POL(GEQ(x1, x2)) = x1 + x2 POL(s(x1)) = 1 + x1
GEQ(x1, x2) -> GEQ(x1, x2)
s(x1) -> s(x1)
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳FwdInst
minus(0, Y) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
geq(X, 0) -> true
geq(0, s(Y)) -> false
geq(s(X), s(Y)) -> geq(X, Y)
div(0, s(Y)) -> 0
div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) -> X
if(false, X, Y) -> Y
innermost
R
↳DPs
→DP Problem 1
↳AFS
→DP Problem 2
↳AFS
→DP Problem 3
↳Forward Instantiation Transformation
DIV(s(X), s(Y)) -> DIV(minus(X, Y), s(Y))
minus(0, Y) -> 0
minus(s(X), s(Y)) -> minus(X, Y)
geq(X, 0) -> true
geq(0, s(Y)) -> false
geq(s(X), s(Y)) -> geq(X, Y)
div(0, s(Y)) -> 0
div(s(X), s(Y)) -> if(geq(X, Y), s(div(minus(X, Y), s(Y))), 0)
if(true, X, Y) -> X
if(false, X, Y) -> Y
innermost
no new Dependency Pairs are created.
DIV(s(X), s(Y)) -> DIV(minus(X, Y), s(Y))