Term Rewriting System R:
[y, x, z]
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 Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

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)

Furthermore, R contains three SCCs.


   R
DPs
       →DP Problem 1
Argument Filtering and Ordering
       →DP Problem 2
AFS
       →DP Problem 3
AFS


Dependency Pair:

MINUSACTIVE(s(x), s(y)) -> MINUSACTIVE(x, y)


Rules:


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)


Strategy:

innermost




The following dependency pair can be strictly oriented:

MINUSACTIVE(s(x), s(y)) -> MINUSACTIVE(x, y)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
trivial

resulting in one new DP problem.
Used Argument Filtering System:
MINUSACTIVE(x1, x2) -> MINUSACTIVE(x1, x2)
s(x1) -> s(x1)


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 4
Dependency Graph
       →DP Problem 2
AFS
       →DP Problem 3
AFS


Dependency Pair:


Rules:


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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
Argument Filtering and Ordering
       →DP Problem 3
AFS


Dependency Pair:

GEACTIVE(s(x), s(y)) -> GEACTIVE(x, y)


Rules:


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)


Strategy:

innermost




The following dependency pair can be strictly oriented:

GEACTIVE(s(x), s(y)) -> GEACTIVE(x, y)


There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
trivial

resulting in one new DP problem.
Used Argument Filtering System:
GEACTIVE(x1, x2) -> GEACTIVE(x1, x2)
s(x1) -> s(x1)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
           →DP Problem 5
Dependency Graph
       →DP Problem 3
AFS


Dependency Pair:


Rules:


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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Argument Filtering and Ordering


Dependency Pairs:

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)


Rules:


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)


Strategy:

innermost




The following dependency pairs can be strictly oriented:

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)


The following usable rules for innermost w.r.t. to the AFS can be oriented:

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)
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)
minusactive(0, y) -> 0
minusactive(s(x), s(y)) -> minusactive(x, y)
minusactive(x, y) -> minus(x, y)


Used ordering: Lexicographic Path Order with Non-Strict Precedence with Quasi Precedence:
mark > false
{true, 0, div, divactive, DIVACTIVE} > {geactive, ge} > false
{true, 0, div, divactive, DIVACTIVE} > {ifactive, if, IFACTIVE} > MARK > false
{true, 0, div, divactive, DIVACTIVE} > s > false
minusactive > false
minus > false

resulting in one new DP problem.
Used Argument Filtering System:
MARK(x1) -> MARK(x1)
div(x1, x2) -> div(x1, x2)
DIVACTIVE(x1, x2) -> DIVACTIVE(x1, x2)
IFACTIVE(x1, x2, x3) -> IFACTIVE(x1, x2, x3)
s(x1) -> s(x1)
geactive(x1, x2) -> geactive(x1, x2)
minus(x1, x2) -> x1
mark(x1) -> x1
if(x1, x2, x3) -> if(x1, x2, x3)
ge(x1, x2) -> ge(x1, x2)
divactive(x1, x2) -> divactive(x1, x2)
ifactive(x1, x2, x3) -> ifactive(x1, x2, x3)
minusactive(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 6
Dependency Graph


Dependency Pair:


Rules:


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)


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

Innermost Termination of R successfully shown.
Duration:
0:12 minutes