Term Rewriting System R:
[X, Y]
min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

MIN(s(X), s(Y)) -> MIN(X, Y)
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
QUOT(s(X), s(Y)) -> MIN(X, Y)
LOG(s(s(X))) -> LOG(s(quot(X, s(s(0)))))
LOG(s(s(X))) -> QUOT(X, s(s(0)))

Furthermore, R contains three SCCs.


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


Dependency Pair:

MIN(s(X), s(Y)) -> MIN(X, Y)


Rules:


min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))


Strategy:

innermost




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


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


Dependency Pair:

MIN(s(X), s(Y)) -> MIN(X, Y)


Rule:

none


Strategy:

innermost




We number the DPs as follows:
  1. MIN(s(X), s(Y)) -> MIN(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
UsableRules


Dependency Pair:

QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))


Rules:


min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))


Strategy:

innermost




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


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


Dependency Pair:

QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))


Rules:


min(s(X), s(Y)) -> min(X, Y)
min(X, 0) -> X


Strategy:

innermost




The following Dependency Pair can be strictly oriented using the given order.

QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))


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

min(s(X), s(Y)) -> min(X, Y)
min(X, 0) -> X


Used ordering:
Polynomial Order with Interpretation:

POL( QUOT(x1, x2) ) = x1

POL( s(x1) ) = x1 + 1

POL( min(x1, x2) ) = x1


This results in one new DP problem.


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


Dependency Pair:


Rules:


min(s(X), s(Y)) -> min(X, Y)
min(X, 0) -> X


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


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


Dependency Pair:

LOG(s(s(X))) -> LOG(s(quot(X, s(s(0)))))


Rules:


min(X, 0) -> X
min(s(X), s(Y)) -> min(X, Y)
quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
log(s(0)) -> 0
log(s(s(X))) -> s(log(s(quot(X, s(s(0))))))


Strategy:

innermost




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


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


Dependency Pair:

LOG(s(s(X))) -> LOG(s(quot(X, s(s(0)))))


Rules:


quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
min(s(X), s(Y)) -> min(X, Y)
min(X, 0) -> X


Strategy:

innermost




The following Dependency Pair can be strictly oriented using the given order.

LOG(s(s(X))) -> LOG(s(quot(X, s(s(0)))))


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

quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
min(s(X), s(Y)) -> min(X, Y)
min(X, 0) -> X


Used ordering:
Polynomial Order with Interpretation:

POL( LOG(x1) ) = x1

POL( s(x1) ) = x1 + 1

POL( quot(x1, x2) ) = x1

POL( 0 ) = 0

POL( min(x1, x2) ) = x1


This results in one new DP problem.


   R
DPs
       →DP Problem 1
UsableRules
       →DP Problem 2
UsableRules
       →DP Problem 3
UsableRules
           →DP Problem 7
Neg POLO
             ...
               →DP Problem 8
Dependency Graph


Dependency Pair:


Rules:


quot(0, s(Y)) -> 0
quot(s(X), s(Y)) -> s(quot(min(X, Y), s(Y)))
min(s(X), s(Y)) -> min(X, Y)
min(X, 0) -> X


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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