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

Innermost Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

PLUS(s(X), Y) -> PLUS(X, Y)
MIN(s(X), s(Y)) -> MIN(X, Y)
MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
MIN(min(X, Y), Z) -> PLUS(Y, Z)
QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
QUOT(s(X), s(Y)) -> MIN(X, Y)

Furthermore, R contains three SCCs.


   R
DPs
       →DP Problem 1
Forward Instantiation Transformation
       →DP Problem 2
Nar
       →DP Problem 3
Nar


Dependency Pair:

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


Rules:


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


Strategy:

innermost




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

PLUS(s(X), Y) -> PLUS(X, Y)
one new Dependency Pair is created:

PLUS(s(s(X'')), Y'') -> PLUS(s(X''), Y'')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 4
Forward Instantiation Transformation
       →DP Problem 2
Nar
       →DP Problem 3
Nar


Dependency Pair:

PLUS(s(s(X'')), Y'') -> PLUS(s(X''), Y'')


Rules:


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


Strategy:

innermost




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

PLUS(s(s(X'')), Y'') -> PLUS(s(X''), Y'')
one new Dependency Pair is created:

PLUS(s(s(s(X''''))), Y'''') -> PLUS(s(s(X'''')), Y'''')

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 5
Polynomial Ordering
       →DP Problem 2
Nar
       →DP Problem 3
Nar


Dependency Pair:

PLUS(s(s(s(X''''))), Y'''') -> PLUS(s(s(X'''')), Y'''')


Rules:


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

PLUS(s(s(s(X''''))), Y'''') -> PLUS(s(s(X'''')), Y'''')


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(PLUS(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
           →DP Problem 4
FwdInst
             ...
               →DP Problem 6
Dependency Graph
       →DP Problem 2
Nar
       →DP Problem 3
Nar


Dependency Pair:


Rules:


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


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Narrowing Transformation
       →DP Problem 3
Nar


Dependency Pairs:

MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
MIN(s(X), s(Y)) -> MIN(X, Y)


Rules:


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


Strategy:

innermost




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

MIN(min(X, Y), Z) -> MIN(X, plus(Y, Z))
one new Dependency Pair is created:

MIN(min(X, s(X'')), Z) -> MIN(X, s(plus(X'', Z)))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 7
Forward Instantiation Transformation
       →DP Problem 3
Nar


Dependency Pair:

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


Rules:


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


Strategy:

innermost




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

MIN(s(X), s(Y)) -> MIN(X, Y)
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 7
FwdInst
             ...
               →DP Problem 8
Forward Instantiation Transformation
       →DP Problem 3
Nar


Dependency Pair:

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


Rules:


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


Strategy:

innermost




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

MIN(s(s(X'')), s(s(Y''))) -> MIN(s(X''), s(Y''))
one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 7
FwdInst
             ...
               →DP Problem 9
Polynomial Ordering
       →DP Problem 3
Nar


Dependency Pair:

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


Rules:


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(MIN(x1, x2))=  1 + x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
           →DP Problem 7
FwdInst
             ...
               →DP Problem 10
Dependency Graph
       →DP Problem 3
Nar


Dependency Pair:


Rules:


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


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Narrowing Transformation


Dependency Pair:

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


Rules:


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


Strategy:

innermost




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

QUOT(s(X), s(Y)) -> QUOT(min(X, Y), s(Y))
three new Dependency Pairs are created:

QUOT(s(X''), s(0)) -> QUOT(X'', s(0))
QUOT(s(s(X'')), s(s(Y''))) -> QUOT(min(X'', Y''), s(s(Y'')))
QUOT(s(min(X'', Y'')), s(Z)) -> QUOT(min(X'', plus(Y'', Z)), s(Z))

The transformation is resulting in three new DP problems:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
Forward Instantiation Transformation
           →DP Problem 12
Nar
           →DP Problem 13
Nar


Dependency Pair:

QUOT(s(X''), s(0)) -> QUOT(X'', s(0))


Rules:


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


Strategy:

innermost




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

QUOT(s(X''), s(0)) -> QUOT(X'', s(0))
one new Dependency Pair is created:

QUOT(s(s(X'''')), s(0)) -> QUOT(s(X''''), s(0))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
FwdInst
             ...
               →DP Problem 14
Polynomial Ordering
           →DP Problem 12
Nar
           →DP Problem 13
Nar


Dependency Pair:

QUOT(s(s(X'''')), s(0)) -> QUOT(s(X''''), s(0))


Rules:


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

QUOT(s(s(X'''')), s(0)) -> QUOT(s(X''''), s(0))


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(QUOT(x1, x2))=  1 + x1  
  POL(0)=  0  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
FwdInst
             ...
               →DP Problem 19
Dependency Graph
           →DP Problem 12
Nar
           →DP Problem 13
Nar


Dependency Pair:


Rules:


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


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
FwdInst
           →DP Problem 12
Narrowing Transformation
           →DP Problem 13
Nar


Dependency Pair:

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


Rules:


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


Strategy:

innermost




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

QUOT(s(s(X'')), s(s(Y''))) -> QUOT(min(X'', Y''), s(s(Y'')))
three new Dependency Pairs are created:

QUOT(s(s(X''')), s(s(0))) -> QUOT(X''', s(s(0)))
QUOT(s(s(s(X'))), s(s(s(Y')))) -> QUOT(min(X', Y'), s(s(s(Y'))))
QUOT(s(s(min(X', Y'))), s(s(Z))) -> QUOT(min(X', plus(Y', Z)), s(s(Z)))

The transformation is resulting in three new DP problems:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
FwdInst
           →DP Problem 12
Nar
             ...
               →DP Problem 15
Polynomial Ordering
           →DP Problem 13
Nar


Dependency Pair:

QUOT(s(s(X''')), s(s(0))) -> QUOT(X''', s(s(0)))


Rules:


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

QUOT(s(s(X''')), s(s(0))) -> QUOT(X''', s(s(0)))


There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(QUOT(x1, x2))=  1 + x1  
  POL(0)=  0  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
FwdInst
           →DP Problem 12
Nar
             ...
               →DP Problem 16
Polynomial Ordering
           →DP Problem 13
Nar


Dependency Pair:

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


Rules:


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


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

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


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(Z)=  1  
  POL(plus(x1, x2))=  1  
  POL(QUOT(x1, x2))=  x1  
  POL(0)=  1  
  POL(min(x1, x2))=  x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
FwdInst
           →DP Problem 12
Nar
             ...
               →DP Problem 17
Polynomial Ordering
           →DP Problem 13
Nar


Dependency Pair:

QUOT(s(s(min(X', Y'))), s(s(Z))) -> QUOT(min(X', plus(Y', Z)), s(s(Z)))


Rules:


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

QUOT(s(s(min(X', Y'))), s(s(Z))) -> QUOT(min(X', plus(Y', Z)), s(s(Z)))


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

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


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(plus(x1, x2))=  0  
  POL(Z)=  0  
  POL(QUOT(x1, x2))=  1 + x1  
  POL(0)=  0  
  POL(min(x1, x2))=  x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
FwdInst
           →DP Problem 12
Nar
           →DP Problem 13
Narrowing Transformation


Dependency Pair:

QUOT(s(min(X'', Y'')), s(Z)) -> QUOT(min(X'', plus(Y'', Z)), s(Z))


Rules:


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


Strategy:

innermost




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

QUOT(s(min(X'', Y'')), s(Z)) -> QUOT(min(X'', plus(Y'', Z)), s(Z))
one new Dependency Pair is created:

QUOT(s(min(X'', s(X'))), s(Z)) -> QUOT(min(X'', s(plus(X', Z))), s(Z))

The transformation is resulting in one new DP problem:



   R
DPs
       →DP Problem 1
FwdInst
       →DP Problem 2
Nar
       →DP Problem 3
Nar
           →DP Problem 11
FwdInst
           →DP Problem 12
Nar
           →DP Problem 13
Nar
             ...
               →DP Problem 18
Polynomial Ordering


Dependency Pair:

QUOT(s(min(X'', s(X'))), s(Z)) -> QUOT(min(X'', s(plus(X', Z))), s(Z))


Rules:


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

QUOT(s(min(X'', s(X'))), s(Z)) -> QUOT(min(X'', s(plus(X', Z))), s(Z))


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

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


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(plus(x1, x2))=  0  
  POL(Z)=  0  
  POL(QUOT(x1, x2))=  x1 + x2  
  POL(0)=  0  
  POL(min(x1, x2))=  x1  
  POL(s(x1))=  1 + x1  

resulting in one new DP problem.


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