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
Nar


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
Nar


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
Nar


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
Nar


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
Narrowing Transformation


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




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(div(x, y)) -> DIVACTIVE(mark(x), y)
six new Dependency Pairs are created:

MARK(div(0, y)) -> DIVACTIVE(0, y)
MARK(div(s(x''), y)) -> DIVACTIVE(s(mark(x'')), y)
MARK(div(minus(x'', y''), y)) -> DIVACTIVE(minusactive(x'', y''), y)
MARK(div(ge(x'', y''), y)) -> DIVACTIVE(geactive(x'', y''), y)
MARK(div(div(x'', y''), y)) -> DIVACTIVE(divactive(mark(x''), y''), y)
MARK(div(if(x'', y'', z'), y)) -> DIVACTIVE(ifactive(mark(x''), y'', z'), y)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Nar
           →DP Problem 6
Narrowing Transformation


Dependency Pairs:

MARK(div(if(x'', y'', z'), y)) -> DIVACTIVE(ifactive(mark(x''), y'', z'), y)
MARK(div(div(x'', y''), y)) -> DIVACTIVE(divactive(mark(x''), y''), y)
MARK(div(ge(x'', y''), y)) -> DIVACTIVE(geactive(x'', y''), y)
MARK(div(minus(x'', y''), y)) -> DIVACTIVE(minusactive(x'', y''), y)
IFACTIVE(false, x, y) -> MARK(y)
DIVACTIVE(s(x), s(y)) -> IFACTIVE(geactive(x, y), s(div(minus(x, y), s(y))), 0)
MARK(div(s(x''), y)) -> DIVACTIVE(s(mark(x'')), y)
IFACTIVE(true, x, y) -> MARK(x)
MARK(if(x, y, z)) -> IFACTIVE(mark(x), y, z)
MARK(div(x, y)) -> MARK(x)
MARK(s(x)) -> MARK(x)
MARK(if(x, y, z)) -> 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




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

MARK(if(x, y, z)) -> IFACTIVE(mark(x), y, z)
six new Dependency Pairs are created:

MARK(if(0, y, z)) -> IFACTIVE(0, y, z)
MARK(if(s(x''), y, z)) -> IFACTIVE(s(mark(x'')), y, z)
MARK(if(minus(x'', y''), y, z)) -> IFACTIVE(minusactive(x'', y''), y, z)
MARK(if(ge(x'', y''), y, z)) -> IFACTIVE(geactive(x'', y''), y, z)
MARK(if(div(x'', y''), y, z)) -> IFACTIVE(divactive(mark(x''), y''), y, z)
MARK(if(if(x'', y'', z''), y, z)) -> IFACTIVE(ifactive(mark(x''), y'', z''), y, z)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Nar
           →DP Problem 6
Nar
             ...
               →DP Problem 7
Narrowing Transformation


Dependency Pairs:

MARK(if(if(x'', y'', z''), y, z)) -> IFACTIVE(ifactive(mark(x''), y'', z''), y, z)
MARK(if(div(x'', y''), y, z)) -> IFACTIVE(divactive(mark(x''), y''), y, z)
MARK(if(ge(x'', y''), y, z)) -> IFACTIVE(geactive(x'', y''), y, z)
IFACTIVE(false, x, y) -> MARK(y)
MARK(if(minus(x'', y''), y, z)) -> IFACTIVE(minusactive(x'', y''), y, z)
MARK(div(div(x'', y''), y)) -> DIVACTIVE(divactive(mark(x''), y''), y)
MARK(div(ge(x'', y''), y)) -> DIVACTIVE(geactive(x'', y''), y)
MARK(div(minus(x'', y''), y)) -> DIVACTIVE(minusactive(x'', y''), y)
MARK(div(s(x''), y)) -> DIVACTIVE(s(mark(x'')), y)
MARK(if(x, y, z)) -> MARK(x)
MARK(div(x, y)) -> MARK(x)
MARK(s(x)) -> 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(if(x'', y'', z'), y)) -> DIVACTIVE(ifactive(mark(x''), y'', z'), 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




On this DP problem, a Narrowing SCC transformation can be performed.
As a result of transforming the rule

DIVACTIVE(s(x), s(y)) -> IFACTIVE(geactive(x, y), s(div(minus(x, y), s(y))), 0)
four new Dependency Pairs are created:

DIVACTIVE(s(x''), s(0)) -> IFACTIVE(true, s(div(minus(x'', 0), s(0))), 0)
DIVACTIVE(s(0), s(s(y''))) -> IFACTIVE(false, s(div(minus(0, s(y'')), s(s(y'')))), 0)
DIVACTIVE(s(s(x'')), s(s(y''))) -> IFACTIVE(geactive(x'', y''), s(div(minus(s(x''), s(y'')), s(s(y'')))), 0)
DIVACTIVE(s(x''), s(y'')) -> IFACTIVE(ge(x'', y''), s(div(minus(x'', y''), s(y''))), 0)

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Nar
           →DP Problem 6
Nar
             ...
               →DP Problem 8
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

MARK(if(div(x'', y''), y, z)) -> IFACTIVE(divactive(mark(x''), y''), y, z)
MARK(if(ge(x'', y''), y, z)) -> IFACTIVE(geactive(x'', y''), y, z)
MARK(if(minus(x'', y''), y, z)) -> IFACTIVE(minusactive(x'', y''), y, z)
MARK(div(if(x'', y'', z'), y)) -> DIVACTIVE(ifactive(mark(x''), y'', z'), y)
MARK(div(div(x'', y''), y)) -> DIVACTIVE(divactive(mark(x''), y''), y)
MARK(div(ge(x'', y''), y)) -> DIVACTIVE(geactive(x'', y''), y)
DIVACTIVE(s(s(x'')), s(s(y''))) -> IFACTIVE(geactive(x'', y''), s(div(minus(s(x''), s(y'')), s(s(y'')))), 0)
MARK(div(minus(x'', y''), y)) -> DIVACTIVE(minusactive(x'', y''), y)
IFACTIVE(false, x, y) -> MARK(y)
DIVACTIVE(s(0), s(s(y''))) -> IFACTIVE(false, s(div(minus(0, s(y'')), s(s(y'')))), 0)
DIVACTIVE(s(x''), s(0)) -> IFACTIVE(true, s(div(minus(x'', 0), s(0))), 0)
MARK(div(s(x''), y)) -> DIVACTIVE(s(mark(x'')), y)
MARK(if(x, y, z)) -> MARK(x)
MARK(div(x, y)) -> MARK(x)
MARK(s(x)) -> MARK(x)
IFACTIVE(true, x, y) -> MARK(x)
MARK(if(if(x'', y'', z''), y, z)) -> IFACTIVE(ifactive(mark(x''), y'', z''), y, z)


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:41 minutes