R
↳Dependency Pair Analysis
MINUSACTIVE(s(x), s(y)) -> MINUSACTIVE(x, y)
MARK(s(x)) -> MARK(x)
MARK(minus(x, y)) -> MINUSACTIVE(x, y)
MARK(ge(x, y)) -> GEACTIVE(x, y)
MARK(div(x, y)) -> DIVACTIVE(mark(x), y)
MARK(div(x, y)) -> MARK(x)
MARK(if(x, y, z)) -> IFACTIVE(mark(x), y, z)
MARK(if(x, y, z)) -> MARK(x)
GEACTIVE(s(x), s(y)) -> GEACTIVE(x, y)
DIVACTIVE(s(x), s(y)) -> IFACTIVE(geactive(x, y), s(div(minus(x, y), s(y))), 0)
DIVACTIVE(s(x), s(y)) -> GEACTIVE(x, y)
IFACTIVE(true, x, y) -> MARK(x)
IFACTIVE(false, x, y) -> MARK(y)
R
↳DPs
→DP Problem 1
↳Polynomial Ordering
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
MINUSACTIVE(s(x), s(y)) -> MINUSACTIVE(x, y)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost
MINUSACTIVE(s(x), s(y)) -> MINUSACTIVE(x, y)
POL(s(x1)) = 1 + x1 POL(MINUS_ACTIVE(x1, x2)) = x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 4
↳Dependency Graph
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polynomial Ordering
→DP Problem 3
↳Polo
GEACTIVE(s(x), s(y)) -> GEACTIVE(x, y)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost
GEACTIVE(s(x), s(y)) -> GEACTIVE(x, y)
POL(GE_ACTIVE(x1, x2)) = x1 POL(s(x1)) = 1 + x1
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 5
↳Dependency Graph
→DP Problem 3
↳Polo
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polynomial Ordering
MARK(if(x, y, z)) -> MARK(x)
IFACTIVE(false, x, y) -> MARK(y)
MARK(if(x, y, z)) -> IFACTIVE(mark(x), y, z)
MARK(div(x, y)) -> MARK(x)
IFACTIVE(true, x, y) -> MARK(x)
DIVACTIVE(s(x), s(y)) -> IFACTIVE(geactive(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIVACTIVE(mark(x), y)
MARK(s(x)) -> MARK(x)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost
MARK(div(x, y)) -> MARK(x)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
POL(ge_active(x1, x2)) = 0 POL(MARK(x1)) = x1 POL(div_active(x1, x2)) = 1 + x1 POL(false) = 0 POL(minus(x1, x2)) = 0 POL(true) = 0 POL(mark(x1)) = x1 POL(minus_active(x1, x2)) = 0 POL(if(x1, x2, x3)) = x1 + x2 + x3 POL(0) = 0 POL(s(x1)) = x1 POL(ge(x1, x2)) = 0 POL(DIV_ACTIVE(x1, x2)) = 1 POL(if_active(x1, x2, x3)) = x1 + x2 + x3 POL(div(x1, x2)) = 1 + x1 POL(IF_ACTIVE(x1, x2, x3)) = x2 + x3
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 6
↳Polynomial Ordering
MARK(if(x, y, z)) -> MARK(x)
IFACTIVE(false, x, y) -> MARK(y)
MARK(if(x, y, z)) -> IFACTIVE(mark(x), y, z)
IFACTIVE(true, x, y) -> MARK(x)
DIVACTIVE(s(x), s(y)) -> IFACTIVE(geactive(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIVACTIVE(mark(x), y)
MARK(s(x)) -> MARK(x)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost
MARK(if(x, y, z)) -> MARK(x)
MARK(if(x, y, z)) -> IFACTIVE(mark(x), y, z)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
POL(ge_active(x1, x2)) = 0 POL(MARK(x1)) = x1 POL(div_active(x1, x2)) = 1 POL(false) = 0 POL(minus(x1, x2)) = 0 POL(true) = 0 POL(mark(x1)) = 1 + x1 POL(minus_active(x1, x2)) = 0 POL(if(x1, x2, x3)) = 1 + x1 + x2 + x3 POL(0) = 0 POL(s(x1)) = x1 POL(ge(x1, x2)) = 0 POL(DIV_ACTIVE(x1, x2)) = 0 POL(if_active(x1, x2, x3)) = 1 + x1 + x2 + x3 POL(div(x1, x2)) = 0 POL(IF_ACTIVE(x1, x2, x3)) = x2 + x3
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 6
↳Polo
...
→DP Problem 7
↳Polynomial Ordering
IFACTIVE(false, x, y) -> MARK(y)
IFACTIVE(true, x, y) -> MARK(x)
DIVACTIVE(s(x), s(y)) -> IFACTIVE(geactive(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIVACTIVE(mark(x), y)
MARK(s(x)) -> MARK(x)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost
MARK(s(x)) -> MARK(x)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
POL(ge_active(x1, x2)) = 0 POL(MARK(x1)) = x1 POL(false) = 0 POL(div_active(x1, x2)) = x1 POL(minus(x1, x2)) = 0 POL(true) = 0 POL(mark(x1)) = x1 POL(minus_active(x1, x2)) = 0 POL(if(x1, x2, x3)) = x2 + x3 POL(0) = 0 POL(s(x1)) = 1 + x1 POL(ge(x1, x2)) = 0 POL(DIV_ACTIVE(x1, x2)) = x1 POL(if_active(x1, x2, x3)) = x2 + x3 POL(div(x1, x2)) = x1 POL(IF_ACTIVE(x1, x2, x3)) = x2 + x3
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 6
↳Polo
...
→DP Problem 8
↳Polynomial Ordering
IFACTIVE(false, x, y) -> MARK(y)
IFACTIVE(true, x, y) -> MARK(x)
DIVACTIVE(s(x), s(y)) -> IFACTIVE(geactive(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIVACTIVE(mark(x), y)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost
IFACTIVE(false, x, y) -> MARK(y)
IFACTIVE(true, x, y) -> MARK(x)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
POL(ge_active(x1, x2)) = 0 POL(MARK(x1)) = x1 POL(false) = 0 POL(div_active(x1, x2)) = 1 POL(minus(x1, x2)) = 0 POL(true) = 0 POL(mark(x1)) = 1 POL(minus_active(x1, x2)) = 0 POL(if(x1, x2, x3)) = 0 POL(0) = 0 POL(s(x1)) = 0 POL(ge(x1, x2)) = 0 POL(DIV_ACTIVE(x1, x2)) = 1 POL(if_active(x1, x2, x3)) = 1 POL(div(x1, x2)) = 1 POL(IF_ACTIVE(x1, x2, x3)) = 1 + x2 + x3
R
↳DPs
→DP Problem 1
↳Polo
→DP Problem 2
↳Polo
→DP Problem 3
↳Polo
→DP Problem 6
↳Polo
...
→DP Problem 9
↳Dependency Graph
DIVACTIVE(s(x), s(y)) -> IFACTIVE(geactive(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(x, y)) -> DIVACTIVE(mark(x), y)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)
mark(0) -> 0
mark(s(x)) -> s(mark(x))
mark(minus(x, y)) -> minusactive(x, y)
mark(ge(x, y)) -> geactive(x, y)
mark(div(x, y)) -> divactive(mark(x), y)
mark(if(x, y, z)) -> ifactive(mark(x), y, z)
geactive(x, 0) -> true
geactive(0, s(y)) -> false
geactive(s(x), s(y)) -> geactive(x, y)
geactive(x, y) -> ge(x, y)
divactive(0, s(y)) -> 0
divactive(s(x), s(y)) -> ifactive(geactive(x, y), s(div(minus(x, y), s(y))), 0)
divactive(x, y) -> div(x, y)
ifactive(true, x, y) -> mark(x)
ifactive(false, x, y) -> mark(y)
ifactive(x, y, z) -> if(x, y, z)
innermost