Termination Proof using AProVE

Term Rewriting System R:
[y, x, u, v, z]
merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

MERGE(.(x, y), .(u, v)) -> IF(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))
MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
++'(.(x, y), z) -> ++'(y, z)

Furthermore, R contains two SCCs.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

Dependency Pairs:

MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)
MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

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

MERGE(.(x, y), .(u, v)) -> MERGE(y, .(u, v))

one new Dependency Pair is created:

MERGE(.(x, .(x'', y'')), .(u'', v'')) -> MERGE(.(x'', y''), .(u'', v''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 3

             ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

Dependency Pairs:

MERGE(.(x, .(x'', y'')), .(u'', v'')) -> MERGE(.(x'', y''), .(u'', v''))
MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

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

MERGE(.(x, y), .(u, v)) -> MERGE(.(x, y), v)

two new Dependency Pairs are created:

MERGE(.(x'', y''), .(u, .(u'', v''))) -> MERGE(.(x'', y''), .(u'', v''))
MERGE(.(x'', .(x'''', y'''')), .(u, .(u'''', v''''))) -> MERGE(.(x'', .(x'''', y'''')), .(u'''', v''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 3

             ↳FwdInst

...

               →DP Problem 4

                 ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

Dependency Pairs:

MERGE(.(x'', .(x'''', y'''')), .(u, .(u'''', v''''))) -> MERGE(.(x'', .(x'''', y'''')), .(u'''', v''''))
MERGE(.(x'', y''), .(u, .(u'', v''))) -> MERGE(.(x'', y''), .(u'', v''))
MERGE(.(x, .(x'', y'')), .(u'', v'')) -> MERGE(.(x'', y''), .(u'', v''))

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

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

MERGE(.(x, .(x'', y'')), .(u'', v'')) -> MERGE(.(x'', y''), .(u'', v''))

three new Dependency Pairs are created:

MERGE(.(x, .(x'''', .(x''''', y''''))), .(u'''', v'''')) -> MERGE(.(x'''', .(x''''', y'''')), .(u'''', v''''))
MERGE(.(x, .(x'''', y'''')), .(u''0, .(u'''', v''''))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x, .(x'''', .(x'''''', y''''''))), .(u''', .(u'''''', v''''''))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 3

             ↳FwdInst

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

Dependency Pairs:

MERGE(.(x, .(x'''', .(x'''''', y''''''))), .(u''', .(u'''''', v''''''))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x, .(x'''', y'''')), .(u''0, .(u'''', v''''))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x, .(x'''', .(x''''', y''''))), .(u'''', v'''')) -> MERGE(.(x'''', .(x''''', y'''')), .(u'''', v''''))
MERGE(.(x'', y''), .(u, .(u'', v''))) -> MERGE(.(x'', y''), .(u'', v''))
MERGE(.(x'', .(x'''', y'''')), .(u, .(u'''', v''''))) -> MERGE(.(x'', .(x'''', y'''')), .(u'''', v''''))

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

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

MERGE(.(x'', y''), .(u, .(u'', v''))) -> MERGE(.(x'', y''), .(u'', v''))

five new Dependency Pairs are created:

MERGE(.(x'''', y''''), .(u, .(u''0, .(u'''', v'''')))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x'''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u, .(u''', v'''))) -> MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u''', v'''))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u''', .(u'''''''', v'''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 3

             ↳FwdInst

...

               →DP Problem 6

                 ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

Dependency Pairs:

MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u''', .(u'''''''', v'''''''')))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u, .(u''', v'''))) -> MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u''', v'''))
MERGE(.(x'''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x'''', y''''), .(u, .(u''0, .(u'''', v'''')))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x, .(x'''', y'''')), .(u''0, .(u'''', v''''))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x, .(x'''', .(x''''', y''''))), .(u'''', v'''')) -> MERGE(.(x'''', .(x''''', y'''')), .(u'''', v''''))
MERGE(.(x'', .(x'''', y'''')), .(u, .(u'''', v''''))) -> MERGE(.(x'', .(x'''', y'''')), .(u'''', v''''))
MERGE(.(x, .(x'''', .(x'''''', y''''''))), .(u''', .(u'''''', v''''''))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

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

MERGE(.(x'', .(x'''', y'''')), .(u, .(u'''', v''''))) -> MERGE(.(x'', .(x'''', y'''')), .(u'''', v''''))

eight new Dependency Pairs are created:

MERGE(.(x''0, .(x'''''', y'''''')), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''0, .(x'''''', y'''''')), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x''''', .(x'''''''', y''''''))), .(u, .(u'''''', v''''''))) -> MERGE(.(x''', .(x''''', .(x'''''''', y''''''))), .(u'''''', v''''''))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u'''''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u'''''', .(u'''''''', v'''''''')))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''''0, .(u''0'', .(u'''''', v''''''))))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''''0, .(u''0'', .(u'''''', v''''''))))
MERGE(.(x''', .(x'''''', y''''')), .(u, .(u''''0, .(u'''''', .(u'''''''', v''''''''))))) -> MERGE(.(x''', .(x'''''', y''''')), .(u''''0, .(u'''''', .(u'''''''', v''''''''))))
MERGE(.(x''', .(x'''''', .(x'''''''''''', y''''''''))), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''''''', y''''''''))), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', .(x'''''''''', y''''''''''))), .(u, .(u''''0, .(u'''''', .(u'''''''''', v''''''''''))))) -> MERGE(.(x''', .(x'''''', .(x'''''''''', y''''''''''))), .(u''''0, .(u'''''', .(u'''''''''', v''''''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 3

             ↳FwdInst

...

               →DP Problem 7

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳FwdInst

Dependency Pairs:

MERGE(.(x''', .(x'''''', .(x'''''''''', y''''''''''))), .(u, .(u''''0, .(u'''''', .(u'''''''''', v''''''''''))))) -> MERGE(.(x''', .(x'''''', .(x'''''''''', y''''''''''))), .(u''''0, .(u'''''', .(u'''''''''', v''''''''''))))
MERGE(.(x''', .(x'''''', .(x'''''''''''', y''''''''))), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''''''', y''''''''))), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', y''''')), .(u, .(u''''0, .(u'''''', .(u'''''''', v''''''''))))) -> MERGE(.(x''', .(x'''''', y''''')), .(u''''0, .(u'''''', .(u'''''''', v''''''''))))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''''0, .(u''0'', .(u'''''', v''''''))))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''''0, .(u''0'', .(u'''''', v''''''))))
MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u'''''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u'''''', .(u'''''''', v'''''''')))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x''''', .(x'''''''', y''''''))), .(u, .(u'''''', v''''''))) -> MERGE(.(x''', .(x''''', .(x'''''''', y''''''))), .(u'''''', v''''''))
MERGE(.(x''0, .(x'''''', y'''''')), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''0, .(x'''''', y'''''')), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u, .(u''', v'''))) -> MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u''', v'''))
MERGE(.(x'''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x'''', y''''), .(u, .(u''0, .(u'''', v'''')))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x, .(x'''', .(x'''''', y''''''))), .(u''', .(u'''''', v''''''))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x, .(x'''', y'''')), .(u''0, .(u'''', v''''))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x, .(x'''', .(x''''', y''''))), .(u'''', v'''')) -> MERGE(.(x'''', .(x''''', y'''')), .(u'''', v''''))
MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u''', .(u'''''''', v'''''''')))

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

The following dependency pairs can be strictly oriented:

MERGE(.(x, .(x'''', .(x'''''', y''''''))), .(u''', .(u'''''', v''''''))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x, .(x'''', y'''')), .(u''0, .(u'''', v''''))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x, .(x'''', .(x''''', y''''))), .(u'''', v'''')) -> MERGE(.(x'''', .(x''''', y'''')), .(u'''', v''''))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(.(x₁, x₂)) = 1 + x₂

POL(MERGE(x₁, x₂)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 3

             ↳FwdInst

...

               →DP Problem 8

                 ↳Polynomial Ordering

       →DP Problem 2

         ↳FwdInst

Dependency Pairs:

MERGE(.(x''', .(x'''''', .(x'''''''''', y''''''''''))), .(u, .(u''''0, .(u'''''', .(u'''''''''', v''''''''''))))) -> MERGE(.(x''', .(x'''''', .(x'''''''''', y''''''''''))), .(u''''0, .(u'''''', .(u'''''''''', v''''''''''))))
MERGE(.(x''', .(x'''''', .(x'''''''''''', y''''''''))), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''''''', y''''''''))), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', y''''')), .(u, .(u''''0, .(u'''''', .(u'''''''', v''''''''))))) -> MERGE(.(x''', .(x'''''', y''''')), .(u''''0, .(u'''''', .(u'''''''', v''''''''))))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''''0, .(u''0'', .(u'''''', v''''''))))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''''0, .(u''0'', .(u'''''', v''''''))))
MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u'''''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u'''''', .(u'''''''', v'''''''')))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x''''', .(x'''''''', y''''''))), .(u, .(u'''''', v''''''))) -> MERGE(.(x''', .(x''''', .(x'''''''', y''''''))), .(u'''''', v''''''))
MERGE(.(x''0, .(x'''''', y'''''')), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''0, .(x'''''', y'''''')), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u, .(u''', v'''))) -> MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u''', v'''))
MERGE(.(x'''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x'''', y''''), .(u, .(u''0, .(u'''', v'''')))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u''', .(u'''''''', v'''''''')))

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

The following dependency pairs can be strictly oriented:

MERGE(.(x''', .(x'''''', .(x'''''''''', y''''''''''))), .(u, .(u''''0, .(u'''''', .(u'''''''''', v''''''''''))))) -> MERGE(.(x''', .(x'''''', .(x'''''''''', y''''''''''))), .(u''''0, .(u'''''', .(u'''''''''', v''''''''''))))
MERGE(.(x''', .(x'''''', .(x'''''''''''', y''''''''))), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''''''', y''''''''))), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', y''''')), .(u, .(u''''0, .(u'''''', .(u'''''''', v''''''''))))) -> MERGE(.(x''', .(x'''''', y''''')), .(u''''0, .(u'''''', .(u'''''''', v''''''''))))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''''0, .(u''0'', .(u'''''', v''''''))))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''''0, .(u''0'', .(u'''''', v''''''))))
MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u'''''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u'''''', .(u'''''''', v'''''''')))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x''''', .(x'''''''', y''''''))), .(u, .(u'''''', v''''''))) -> MERGE(.(x''', .(x''''', .(x'''''''', y''''''))), .(u'''''', v''''''))
MERGE(.(x''0, .(x'''''', y'''''')), .(u, .(u''''0, .(u'''''', v'''''')))) -> MERGE(.(x''0, .(x'''''', y'''''')), .(u''''0, .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u, .(u''', v'''))) -> MERGE(.(x''', .(x'''''''', .(x''''''''', y''''''))), .(u''', v'''))
MERGE(.(x'''', .(x'''''', y'''''')), .(u, .(u''', .(u'''''', v'''''')))) -> MERGE(.(x'''', .(x'''''', y'''''')), .(u''', .(u'''''', v'''''')))
MERGE(.(x'''', y''''), .(u, .(u''0, .(u'''', v'''')))) -> MERGE(.(x'''', y''''), .(u''0, .(u'''', v'''')))
MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u, .(u''', .(u'''''''', v'''''''')))) -> MERGE(.(x''', .(x'''''', .(x'''''''', y''''''''))), .(u''', .(u'''''''', v'''''''')))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(.(x₁, x₂)) = 1 + x₂

POL(MERGE(x₁, x₂)) = 1 + x₂

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 3

             ↳FwdInst

...

               →DP Problem 9

                 ↳Dependency Graph

       →DP Problem 2

         ↳FwdInst

Dependency Pair:

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳Forward Instantiation Transformation

Dependency Pair:

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

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳Forward Instantiation Transformation

Dependency Pair:

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

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

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

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

one new Dependency Pair is created:

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

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳FwdInst

...

               →DP Problem 11

                 ↳Polynomial Ordering

Dependency Pair:

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

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(++'(x₁, x₂)) = 1 + x₁

POL(.(x₁, x₂)) = 1 + x₂

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 10

             ↳FwdInst

...

               →DP Problem 12

                 ↳Dependency Graph

Dependency Pair:

Rules:

merge(nil, y) -> y
merge(x, nil) -> x
merge(.(x, y), .(u, v)) -> if(< (x, u), .(x, merge(y, .(u, v))), .(u, merge(.(x, y), v)))
++(nil, y) -> y
++(.(x, y), z) -> .(x, ++(y, z))
if(true, x, y) -> x
if(false, x, y) -> x

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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

POL(.(x₁, x₂))	= 1 + x₂
POL(MERGE(x₁, x₂))	= 1 + x₁

POL(++'(x₁, x₂))	= 1 + x₁
POL(.(x₁, x₂))	= 1 + x₂