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.



   R
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.


   R
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:



   R
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:



   R
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:



   R
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:



   R
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:



   R
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''''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(.(x1, x2))=  1 + x2  
  POL(MERGE(x1, x2))=  1 + x2  

resulting in one new DP problem.



   R
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'''''', 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''''))


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(.(x1, x2))=  1 + x2  
  POL(MERGE(x1, x2))=  1 + x1  

resulting in one new DP problem.



   R
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.


   R
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:



   R
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:



   R
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(++'(x1, x2))=  1 + x1  
  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


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