Term Rewriting System R:
[x, y, z]
msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

MSORT(.(x, y)) -> MIN(x, y)
MSORT(.(x, y)) -> MSORT(del(min(x, y), .(x, y)))
MSORT(.(x, y)) -> DEL(min(x, y), .(x, y))
MIN(x, .(y, z)) -> MIN(x, z)
MIN(x, .(y, z)) -> MIN(y, z)
DEL(x, .(y, z)) -> DEL(x, z)

Furthermore, R contains three SCCs. 


   R
     ↳DPs
       →DP Problem 1
         ↳Forward Instantiation Transformation
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Rw


Dependency Pairs:

MIN(x, .(y, z)) -> MIN(y, z)
MIN(x, .(y, z)) -> MIN(x, z)


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




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

MIN(x, .(y, z)) -> MIN(x, z)
one new Dependency Pair is created:

MIN(x'', .(y, .(y'', z''))) -> MIN(x'', .(y'', z''))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

MIN(x'', .(y, .(y'', z''))) -> MIN(x'', .(y'', z''))
MIN(x, .(y, z)) -> MIN(y, z)


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




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

MIN(x, .(y, z)) -> MIN(y, z)
two new Dependency Pairs are created:

MIN(x, .(y0, .(y'', z''))) -> MIN(y0, .(y'', z''))
MIN(x, .(y0, .(y'', .(y'''', z'''')))) -> MIN(y0, .(y'', .(y'''', z'''')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 4
             ↳FwdInst
             ...
               →DP Problem 5
                 ↳Forward Instantiation Transformation
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Rw


Dependency Pairs:

MIN(x, .(y0, .(y'', .(y'''', z'''')))) -> MIN(y0, .(y'', .(y'''', z'''')))
MIN(x, .(y0, .(y'', z''))) -> MIN(y0, .(y'', z''))
MIN(x'', .(y, .(y'', z''))) -> MIN(x'', .(y'', z''))


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




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

MIN(x'', .(y, .(y'', z''))) -> MIN(x'', .(y'', z''))
three new Dependency Pairs are created:

MIN(x'''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x'''', .(y''0, .(y'''', z'''')))
MIN(x''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x''', .(y''0, .(y'''', z'''')))
MIN(x''', .(y, .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(x''', .(y''0, .(y'''', .(y'''''', z''''''))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 4
             ↳FwdInst
             ...
               →DP Problem 6
                 ↳Forward Instantiation Transformation
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Rw


Dependency Pairs:

MIN(x''', .(y, .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(x''', .(y''0, .(y'''', .(y'''''', z''''''))))
MIN(x''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x''', .(y''0, .(y'''', z'''')))
MIN(x'''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x'''', .(y''0, .(y'''', z'''')))
MIN(x, .(y0, .(y'', z''))) -> MIN(y0, .(y'', z''))
MIN(x, .(y0, .(y'', .(y'''', z'''')))) -> MIN(y0, .(y'', .(y'''', z'''')))


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




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

MIN(x, .(y0, .(y'', z''))) -> MIN(y0, .(y'', z''))
four new Dependency Pairs are created:

MIN(x, .(y0'', .(y''0, .(y'''', z'''')))) -> MIN(y0'', .(y''0, .(y'''', z'''')))
MIN(x, .(y0'', .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(y0'', .(y''0, .(y'''', .(y'''''', z''''''))))
MIN(x, .(y0', .(y''', .(y''0'', .(y'''''', z''''''))))) -> MIN(y0', .(y''', .(y''0'', .(y'''''', z''''''))))
MIN(x, .(y0', .(y''', .(y''0'', .(y'''''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y''0'', .(y'''''', .(y'''''''', z'''''''')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 4
             ↳FwdInst
             ...
               →DP Problem 7
                 ↳Forward Instantiation Transformation
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Rw


Dependency Pairs:

MIN(x, .(y0', .(y''', .(y''0'', .(y'''''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y''0'', .(y'''''', .(y'''''''', z'''''''')))))
MIN(x, .(y0', .(y''', .(y''0'', .(y'''''', z''''''))))) -> MIN(y0', .(y''', .(y''0'', .(y'''''', z''''''))))
MIN(x, .(y0'', .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(y0'', .(y''0, .(y'''', .(y'''''', z''''''))))
MIN(x, .(y0'', .(y''0, .(y'''', z'''')))) -> MIN(y0'', .(y''0, .(y'''', z'''')))
MIN(x''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x''', .(y''0, .(y'''', z'''')))
MIN(x'''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x'''', .(y''0, .(y'''', z'''')))
MIN(x, .(y0, .(y'', .(y'''', z'''')))) -> MIN(y0, .(y'', .(y'''', z'''')))
MIN(x''', .(y, .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(x''', .(y''0, .(y'''', .(y'''''', z''''''))))


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




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

MIN(x, .(y0, .(y'', .(y'''', z'''')))) -> MIN(y0, .(y'', .(y'''', z'''')))
five new Dependency Pairs are created:

MIN(x, .(y0'', .(y''0, .(y''''0, .(y'''''', z''''''))))) -> MIN(y0'', .(y''0, .(y''''0, .(y'''''', z''''''))))
MIN(x, .(y0', .(y''', .(y''''0, .(y'''''', z''''''))))) -> MIN(y0', .(y''', .(y''''0, .(y'''''', z''''''))))
MIN(x, .(y0', .(y''', .(y''''0, .(y'''''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y''''0, .(y'''''', .(y'''''''', z'''''''')))))
MIN(x, .(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', z'''''''')))))
MIN(x, .(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', .(y'''''''''', z''''''''''))))))) -> MIN(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', .(y'''''''''', z''''''''''))))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 4
             ↳FwdInst
             ...
               →DP Problem 8
                 ↳Polynomial Ordering
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Rw


Dependency Pairs:

MIN(x, .(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', .(y'''''''''', z''''''''''))))))) -> MIN(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', .(y'''''''''', z''''''''''))))))
MIN(x, .(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', z'''''''')))))
MIN(x, .(y0', .(y''', .(y''''0, .(y'''''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y''''0, .(y'''''', .(y'''''''', z'''''''')))))
MIN(x, .(y0', .(y''', .(y''''0, .(y'''''', z''''''))))) -> MIN(y0', .(y''', .(y''''0, .(y'''''', z''''''))))
MIN(x, .(y0'', .(y''0, .(y''''0, .(y'''''', z''''''))))) -> MIN(y0'', .(y''0, .(y''''0, .(y'''''', z''''''))))
MIN(x, .(y0', .(y''', .(y''0'', .(y'''''', z''''''))))) -> MIN(y0', .(y''', .(y''0'', .(y'''''', z''''''))))
MIN(x, .(y0'', .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(y0'', .(y''0, .(y'''', .(y'''''', z''''''))))
MIN(x, .(y0'', .(y''0, .(y'''', z'''')))) -> MIN(y0'', .(y''0, .(y'''', z'''')))
MIN(x''', .(y, .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(x''', .(y''0, .(y'''', .(y'''''', z''''''))))
MIN(x''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x''', .(y''0, .(y'''', z'''')))
MIN(x'''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x'''', .(y''0, .(y'''', z'''')))
MIN(x, .(y0', .(y''', .(y''0'', .(y'''''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y''0'', .(y'''''', .(y'''''''', z'''''''')))))


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




The following dependency pairs can be strictly oriented:

MIN(x, .(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', .(y'''''''''', z''''''''''))))))) -> MIN(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', .(y'''''''''', z''''''''''))))))
MIN(x, .(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y'''''', .(y''0'''', .(y'''''''', z'''''''')))))
MIN(x, .(y0', .(y''', .(y''''0, .(y'''''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y''''0, .(y'''''', .(y'''''''', z'''''''')))))
MIN(x, .(y0', .(y''', .(y''''0, .(y'''''', z''''''))))) -> MIN(y0', .(y''', .(y''''0, .(y'''''', z''''''))))
MIN(x, .(y0'', .(y''0, .(y''''0, .(y'''''', z''''''))))) -> MIN(y0'', .(y''0, .(y''''0, .(y'''''', z''''''))))
MIN(x, .(y0', .(y''', .(y''0'', .(y'''''', z''''''))))) -> MIN(y0', .(y''', .(y''0'', .(y'''''', z''''''))))
MIN(x, .(y0'', .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(y0'', .(y''0, .(y'''', .(y'''''', z''''''))))
MIN(x, .(y0'', .(y''0, .(y'''', z'''')))) -> MIN(y0'', .(y''0, .(y'''', z'''')))
MIN(x''', .(y, .(y''0, .(y'''', .(y'''''', z''''''))))) -> MIN(x''', .(y''0, .(y'''', .(y'''''', z''''''))))
MIN(x''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x''', .(y''0, .(y'''', z'''')))
MIN(x'''', .(y, .(y''0, .(y'''', z'''')))) -> MIN(x'''', .(y''0, .(y'''', z'''')))
MIN(x, .(y0', .(y''', .(y''0'', .(y'''''', .(y'''''''', z'''''''')))))) -> MIN(y0', .(y''', .(y''0'', .(y'''''', .(y'''''''', z'''''''')))))


There are no usable rules for innermost that need to be oriented.

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

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 4
             ↳FwdInst
             ...
               →DP Problem 9
                 ↳Dependency Graph
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Rw


Dependency Pair:


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Rw


Dependency Pair:

DEL(x, .(y, z)) -> DEL(x, z)


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




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

DEL(x, .(y, z)) -> DEL(x, z)
one new Dependency Pair is created:

DEL(x'', .(y, .(y'', z''))) -> DEL(x'', .(y'', z''))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 10
             ↳Forward Instantiation Transformation
       →DP Problem 3
         ↳Rw


Dependency Pair:

DEL(x'', .(y, .(y'', z''))) -> DEL(x'', .(y'', z''))


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




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

DEL(x'', .(y, .(y'', z''))) -> DEL(x'', .(y'', z''))
one new Dependency Pair is created:

DEL(x'''', .(y, .(y''0, .(y'''', z'''')))) -> DEL(x'''', .(y''0, .(y'''', z'''')))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 10
             ↳FwdInst
             ...
               →DP Problem 11
                 ↳Polynomial Ordering
       →DP Problem 3
         ↳Rw


Dependency Pair:

DEL(x'''', .(y, .(y''0, .(y'''', z'''')))) -> DEL(x'''', .(y''0, .(y'''', z'''')))


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




The following dependency pair can be strictly oriented:

DEL(x'''', .(y, .(y''0, .(y'''', z'''')))) -> DEL(x'''', .(y''0, .(y'''', z'''')))


There are no usable rules for innermost that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(DEL(x1, x2))=  1 + x2  
  POL(.(x1, x2))=  1 + x2  

resulting in one new DP problem. 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
           →DP Problem 10
             ↳FwdInst
             ...
               →DP Problem 12
                 ↳Dependency Graph
       →DP Problem 3
         ↳Rw


Dependency Pair:


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
       →DP Problem 2
         ↳FwdInst
       →DP Problem 3
         ↳Rewriting Transformation


Dependency Pair:

MSORT(.(x, y)) -> MSORT(del(min(x, y), .(x, y)))


Rules:


msort(nil) -> nil
msort(.(x, y)) -> .(min(x, y), msort(del(min(x, y), .(x, y))))
min(x, nil) -> x
min(x, .(y, z)) -> if(<=(x, y), min(x, z), min(y, z))
del(x, nil) -> nil
del(x, .(y, z)) -> if(=(x, y), z, .(y, del(x, z)))


Strategy:

innermost




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

MSORT(.(x, y)) -> MSORT(del(min(x, y), .(x, y)))
one new Dependency Pair is created:

MSORT(.(x, y)) -> MSORT(if(=(min(x, y), x), y, .(x, del(min(x, y), y))))

The transformation is resulting in no new DP problems.


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