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
Remaining


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: Homeomorphic Embedding Order with EMB
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
Remaining


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
Remaining


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: Homeomorphic Embedding Order with EMB
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
Remaining


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
Remaining Obligation(s)




The following remains to be proven:
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



Innermost Termination of R could not be shown.
Duration:
0:03 minutes