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
Usable Rules (Innermost)
       →DP Problem 2
UsableRules
       →DP Problem 3
Neg POLO


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




As we are in the innermost case, we can delete all 19 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
           →DP Problem 4
Size-Change Principle
       →DP Problem 2
UsableRules
       →DP Problem 3
Neg POLO


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. MINUSACTIVE(s(x), s(y)) -> MINUSACTIVE(x, y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
Usable Rules (Innermost)
       →DP Problem 3
Neg POLO


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




As we are in the innermost case, we can delete all 19 non-usable-rules.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
           →DP Problem 5
Size-Change Principle
       →DP Problem 3
Neg POLO


Dependency Pair:

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


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. GEACTIVE(s(x), s(y)) -> GEACTIVE(x, y)
and get the following Size-Change Graph(s):
{1} , {1}
1>1
2>2

which lead(s) to this/these maximal multigraph(s):
{1} , {1}
1>1
2>2

DP: empty set
Oriented Rules: none

We used the order Homeomorphic Embedding Order with Non-Strict Precedence.
trivial

with Argument Filtering System:
s(x1) -> s(x1)

We obtain no new DP problems.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
Negative Polynomial Order


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 Pair can be strictly oriented using the given order.

MARK(div(x, y)) -> MARK(x)


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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


Used ordering:
Polynomial Order with Interpretation:

POL( MARK(x1) ) = x1

POL( div(x1, x2) ) = x1 + 1

POL( DIVACTIVE(x1, x2) ) = 1

POL( IFACTIVE(x1, ..., x3) ) = x2 + x3

POL( s(x1) ) = x1

POL( minus(x1, x2) ) = 0

POL( 0 ) = 0

POL( if(x1, ..., x3) ) = x1 + x2 + x3

POL( ifactive(x1, ..., x3) ) = x1 + x2 + x3

POL( true ) = 0

POL( mark(x1) ) = x1

POL( divactive(x1, x2) ) = x1 + 1

POL( minusactive(x1, x2) ) = 0

POL( geactive(x1, x2) ) = 0

POL( false ) = 0

POL( ge(x1, x2) ) = 0


This results in one new DP problem.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
Neg POLO
           →DP Problem 6
Negative Polynomial Order


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)
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 using the given order.

MARK(if(x, y, z)) -> MARK(x)
MARK(if(x, y, z)) -> IFACTIVE(mark(x), y, z)


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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


Used ordering:
Polynomial Order with Interpretation:

POL( MARK(x1) ) = x1

POL( if(x1, ..., x3) ) = x1 + x2 + x3 + 1

POL( DIVACTIVE(x1, x2) ) = 0

POL( IFACTIVE(x1, ..., x3) ) = x2 + x3

POL( s(x1) ) = x1

POL( div(x1, x2) ) = 0

POL( 0 ) = 0

POL( ifactive(x1, ..., x3) ) = x1 + x2 + x3 + 1

POL( true ) = 0

POL( mark(x1) ) = x1 + 1

POL( divactive(x1, x2) ) = 1

POL( minus(x1, x2) ) = 0

POL( minusactive(x1, x2) ) = 0

POL( geactive(x1, x2) ) = 0

POL( false ) = 0

POL( ge(x1, x2) ) = 0


This results in one new DP problem.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
Neg POLO
           →DP Problem 6
Neg POLO
             ...
               →DP Problem 7
Negative Polynomial Order


Dependency Pairs:

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)


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 using the given order.

MARK(s(x)) -> MARK(x)


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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


Used ordering:
Polynomial Order with Interpretation:

POL( MARK(x1) ) = x1

POL( s(x1) ) = x1 + 1

POL( IFACTIVE(x1, ..., x3) ) = x2 + x3

POL( DIVACTIVE(x1, x2) ) = x1

POL( div(x1, x2) ) = x1

POL( minus(x1, x2) ) = 0

POL( 0 ) = 0

POL( mark(x1) ) = x1

POL( geactive(x1, x2) ) = 0

POL( ge(x1, x2) ) = 0

POL( true ) = 0

POL( false ) = 0

POL( ifactive(x1, ..., x3) ) = x2 + x3

POL( divactive(x1, x2) ) = x1

POL( minusactive(x1, x2) ) = 0

POL( if(x1, ..., x3) ) = x2 + x3


This results in one new DP problem.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
Neg POLO
           →DP Problem 6
Neg POLO
             ...
               →DP Problem 8
Negative Polynomial Order


Dependency Pairs:

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)


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 using the given order.

IFACTIVE(false, x, y) -> MARK(y)
IFACTIVE(true, x, y) -> MARK(x)


Moreover, the following usable rules (regarding the implicit AFS) are oriented.

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


Used ordering:
Polynomial Order with Interpretation:

POL( IFACTIVE(x1, ..., x3) ) = x2 + x3 + 1

POL( MARK(x1) ) = x1

POL( DIVACTIVE(x1, x2) ) = 1

POL( s(x1) ) = 0

POL( 0 ) = 0

POL( div(x1, x2) ) = 1

POL( geactive(x1, x2) ) = 0

POL( ge(x1, x2) ) = 0

POL( true ) = 0

POL( false ) = 0

POL( ifactive(x1, ..., x3) ) = 1

POL( mark(x1) ) = 1

POL( divactive(x1, x2) ) = 1

POL( minusactive(x1, x2) ) = 0

POL( if(x1, ..., x3) ) = 0

POL( minus(x1, x2) ) = 0


This results in one new DP problem.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
Neg POLO
           →DP Problem 6
Neg POLO
             ...
               →DP Problem 9
Dependency Graph


Dependency Pairs:

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)


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