Term Rewriting System R:
[x, a, k, y]
f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)

Innermost Termination of R to be shown. 



   R
     ↳Dependency Pair Analysis



R contains the following Dependency Pairs:

F(empty, cons(a, k)) -> F(cons(a, k), k)
F(cons(a, k), y) -> F(y, k)

Furthermore, R contains one SCC. 


   R
     ↳DPs
       →DP Problem 1
         ↳Forward Instantiation Transformation


Dependency Pairs:

F(cons(a, k), y) -> F(y, k)
F(empty, cons(a, k)) -> F(cons(a, k), k)


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, k), y) -> F(y, k)
two new Dependency Pairs are created:

F(cons(a, k''), cons(a'', k''')) -> F(cons(a'', k'''), k'')
F(cons(a, cons(a'', k'')), empty) -> F(empty, cons(a'', k''))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

F(cons(a, cons(a'', k'')), empty) -> F(empty, cons(a'', k''))
F(cons(a, k''), cons(a'', k''')) -> F(cons(a'', k'''), k'')
F(empty, cons(a, k)) -> F(cons(a, k), k)


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(empty, cons(a, k)) -> F(cons(a, k), k)
one new Dependency Pair is created:

F(empty, cons(a'', cons(a'''', k''''''))) -> F(cons(a'', cons(a'''', k'''''')), cons(a'''', k''''''))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

F(cons(a, k''), cons(a'', k''')) -> F(cons(a'', k'''), k'')
F(empty, cons(a'', cons(a'''', k''''''))) -> F(cons(a'', cons(a'''', k'''''')), cons(a'''', k''''''))
F(cons(a, cons(a'', k'')), empty) -> F(empty, cons(a'', k''))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, k''), cons(a'', k''')) -> F(cons(a'', k'''), k'')
two new Dependency Pairs are created:

F(cons(a, cons(a'''', k'''''')), cons(a''0, k'''0)) -> F(cons(a''0, k'''0), cons(a'''', k''''''))
F(cons(a, empty), cons(a''0, cons(a'''', k'''''))) -> F(cons(a''0, cons(a'''', k''''')), empty)

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

F(cons(a, cons(a'', k'')), empty) -> F(empty, cons(a'', k''))
F(cons(a, empty), cons(a''0, cons(a'''', k'''''))) -> F(cons(a''0, cons(a'''', k''''')), empty)
F(cons(a, cons(a'''', k'''''')), cons(a''0, k'''0)) -> F(cons(a''0, k'''0), cons(a'''', k''''''))
F(empty, cons(a'', cons(a'''', k''''''))) -> F(cons(a'', cons(a'''', k'''''')), cons(a'''', k''''''))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a'', k'')), empty) -> F(empty, cons(a'', k''))
one new Dependency Pair is created:

F(cons(a, cons(a'''', cons(a'''''', k''''''''))), empty) -> F(empty, cons(a'''', cons(a'''''', k'''''''')))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

F(cons(a, cons(a'''', k'''''')), cons(a''0, k'''0)) -> F(cons(a''0, k'''0), cons(a'''', k''''''))
F(empty, cons(a'', cons(a'''', k''''''))) -> F(cons(a'', cons(a'''', k'''''')), cons(a'''', k''''''))
F(cons(a, cons(a'''', cons(a'''''', k''''''''))), empty) -> F(empty, cons(a'''', cons(a'''''', k'''''''')))
F(cons(a, empty), cons(a''0, cons(a'''', k'''''))) -> F(cons(a''0, cons(a'''', k''''')), empty)


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a'''', k'''''')), cons(a''0, k'''0)) -> F(cons(a''0, k'''0), cons(a'''', k''''''))
two new Dependency Pairs are created:

F(cons(a, cons(a'''''', k'''''''')), cons(a''0'', cons(a''''''', k'''''''''))) -> F(cons(a''0'', cons(a''''''', k''''''''')), cons(a'''''', k''''''''))
F(cons(a, cons(a'''''', cons(a''''''', k''''''''))), cons(a''0'', empty)) -> F(cons(a''0'', empty), cons(a'''''', cons(a''''''', k'''''''')))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

F(cons(a, cons(a'''', cons(a'''''', k''''''''))), empty) -> F(empty, cons(a'''', cons(a'''''', k'''''''')))
F(cons(a, empty), cons(a''0, cons(a'''', k'''''))) -> F(cons(a''0, cons(a'''', k''''')), empty)
F(cons(a, cons(a'''''', cons(a''''''', k''''''''))), cons(a''0'', empty)) -> F(cons(a''0'', empty), cons(a'''''', cons(a''''''', k'''''''')))
F(cons(a, cons(a'''''', k'''''''')), cons(a''0'', cons(a''''''', k'''''''''))) -> F(cons(a''0'', cons(a''''''', k''''''''')), cons(a'''''', k''''''''))
F(empty, cons(a'', cons(a'''', k''''''))) -> F(cons(a'', cons(a'''', k'''''')), cons(a'''', k''''''))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(empty, cons(a'', cons(a'''', k''''''))) -> F(cons(a'', cons(a'''', k'''''')), cons(a'''', k''''''))
one new Dependency Pair is created:

F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))

The transformation is resulting in one new DP problem: 



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


Dependency Pairs:

F(cons(a, empty), cons(a''0, cons(a'''', k'''''))) -> F(cons(a''0, cons(a'''', k''''')), empty)
F(cons(a, cons(a'''''', cons(a''''''', k''''''''))), cons(a''0'', empty)) -> F(cons(a''0'', empty), cons(a'''''', cons(a''''''', k'''''''')))
F(cons(a, cons(a'''''', k'''''''')), cons(a''0'', cons(a''''''', k'''''''''))) -> F(cons(a''0'', cons(a''''''', k''''''''')), cons(a'''''', k''''''''))
F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))
F(cons(a, cons(a'''', cons(a'''''', k''''''''))), empty) -> F(empty, cons(a'''', cons(a'''''', k'''''''')))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, empty), cons(a''0, cons(a'''', k'''''))) -> F(cons(a''0, cons(a'''', k''''')), empty)
one new Dependency Pair is created:

F(cons(a, empty), cons(a''0', cons(a'''''', cons(a'''''''', k'''''''''')))) -> F(cons(a''0', cons(a'''''', cons(a'''''''', k''''''''''))), empty)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 8
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(cons(a, cons(a'''''', k'''''''')), cons(a''0'', cons(a''''''', k'''''''''))) -> F(cons(a''0'', cons(a''''''', k''''''''')), cons(a'''''', k''''''''))
F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))
F(cons(a, cons(a'''', cons(a'''''', k''''''''))), empty) -> F(empty, cons(a'''', cons(a'''''', k'''''''')))
F(cons(a, empty), cons(a''0', cons(a'''''', cons(a'''''''', k'''''''''')))) -> F(cons(a''0', cons(a'''''', cons(a'''''''', k''''''''''))), empty)
F(cons(a, cons(a'''''', cons(a''''''', k''''''''))), cons(a''0'', empty)) -> F(cons(a''0'', empty), cons(a'''''', cons(a''''''', k'''''''')))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a'''', cons(a'''''', k''''''''))), empty) -> F(empty, cons(a'''', cons(a'''''', k'''''''')))
one new Dependency Pair is created:

F(cons(a, cons(a''''', cons(a'''''''', cons(a'''''''''''', k'''''''''''''')))), empty) -> F(empty, cons(a''''', cons(a'''''''', cons(a'''''''''''', k''''''''''''''))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 9
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))
F(cons(a, cons(a''''', cons(a'''''''', cons(a'''''''''''', k'''''''''''''')))), empty) -> F(empty, cons(a''''', cons(a'''''''', cons(a'''''''''''', k''''''''''''''))))
F(cons(a, empty), cons(a''0', cons(a'''''', cons(a'''''''', k'''''''''')))) -> F(cons(a''0', cons(a'''''', cons(a'''''''', k''''''''''))), empty)
F(cons(a, cons(a'''''', cons(a''''''', k''''''''))), cons(a''0'', empty)) -> F(cons(a''0'', empty), cons(a'''''', cons(a''''''', k'''''''')))
F(cons(a, cons(a'''''', k'''''''')), cons(a''0'', cons(a''''''', k'''''''''))) -> F(cons(a''0'', cons(a''''''', k''''''''')), cons(a'''''', k''''''''))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a'''''', k'''''''')), cons(a''0'', cons(a''''''', k'''''''''))) -> F(cons(a''0'', cons(a''''''', k''''''''')), cons(a'''''', k''''''''))
two new Dependency Pairs are created:

F(cons(a, cons(a''''''0, cons(a'''''''''', k''''''''''''))), cons(a''0'''', cons(a'''''''0, k'''''''''0))) -> F(cons(a''0'''', cons(a'''''''0, k'''''''''0)), cons(a''''''0, cons(a'''''''''', k'''''''''''')))
F(cons(a, cons(a''''''0, empty)), cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k''''''''''')))) -> F(cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k'''''''''''))), cons(a''''''0, empty))

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

F(cons(a, cons(a''''', cons(a'''''''', cons(a'''''''''''', k'''''''''''''')))), empty) -> F(empty, cons(a''''', cons(a'''''''', cons(a'''''''''''', k''''''''''''''))))
F(cons(a, empty), cons(a''0', cons(a'''''', cons(a'''''''', k'''''''''')))) -> F(cons(a''0', cons(a'''''', cons(a'''''''', k''''''''''))), empty)
F(cons(a, cons(a'''''', cons(a''''''', k''''''''))), cons(a''0'', empty)) -> F(cons(a''0'', empty), cons(a'''''', cons(a''''''', k'''''''')))
F(cons(a, cons(a''''''0, empty)), cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k''''''''''')))) -> F(cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k'''''''''''))), cons(a''''''0, empty))
F(cons(a, cons(a''''''0, cons(a'''''''''', k''''''''''''))), cons(a''0'''', cons(a'''''''0, k'''''''''0))) -> F(cons(a''0'''', cons(a'''''''0, k'''''''''0)), cons(a''''''0, cons(a'''''''''', k'''''''''''')))
F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a'''''', cons(a''''''', k''''''''))), cons(a''0'', empty)) -> F(cons(a''0'', empty), cons(a'''''', cons(a''''''', k'''''''')))
one new Dependency Pair is created:

F(cons(a, cons(a''''''1, cons(a'''''''', cons(a'''''''''', k'''''''''''')))), cons(a''0'''', empty)) -> F(cons(a''0'''', empty), cons(a''''''1, cons(a'''''''', cons(a'''''''''', k''''''''''''))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 11
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(cons(a, empty), cons(a''0', cons(a'''''', cons(a'''''''', k'''''''''')))) -> F(cons(a''0', cons(a'''''', cons(a'''''''', k''''''''''))), empty)
F(cons(a, cons(a''''''1, cons(a'''''''', cons(a'''''''''', k'''''''''''')))), cons(a''0'''', empty)) -> F(cons(a''0'''', empty), cons(a''''''1, cons(a'''''''', cons(a'''''''''', k''''''''''''))))
F(cons(a, cons(a''''''0, empty)), cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k''''''''''')))) -> F(cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k'''''''''''))), cons(a''''''0, empty))
F(cons(a, cons(a''''''0, cons(a'''''''''', k''''''''''''))), cons(a''0'''', cons(a'''''''0, k'''''''''0))) -> F(cons(a''0'''', cons(a'''''''0, k'''''''''0)), cons(a''''''0, cons(a'''''''''', k'''''''''''')))
F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))
F(cons(a, cons(a''''', cons(a'''''''', cons(a'''''''''''', k'''''''''''''')))), empty) -> F(empty, cons(a''''', cons(a'''''''', cons(a'''''''''''', k''''''''''''''))))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, empty), cons(a''0', cons(a'''''', cons(a'''''''', k'''''''''')))) -> F(cons(a''0', cons(a'''''', cons(a'''''''', k''''''''''))), empty)
one new Dependency Pair is created:

F(cons(a, empty), cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k''''''''''''''''))))) -> F(cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k'''''''''''''''')))), empty)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 12
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(cons(a, cons(a''''''0, empty)), cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k''''''''''')))) -> F(cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k'''''''''''))), cons(a''''''0, empty))
F(cons(a, cons(a''''''0, cons(a'''''''''', k''''''''''''))), cons(a''0'''', cons(a'''''''0, k'''''''''0))) -> F(cons(a''0'''', cons(a'''''''0, k'''''''''0)), cons(a''''''0, cons(a'''''''''', k'''''''''''')))
F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))
F(cons(a, cons(a''''', cons(a'''''''', cons(a'''''''''''', k'''''''''''''')))), empty) -> F(empty, cons(a''''', cons(a'''''''', cons(a'''''''''''', k''''''''''''''))))
F(cons(a, empty), cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k''''''''''''''''))))) -> F(cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k'''''''''''''''')))), empty)
F(cons(a, cons(a''''''1, cons(a'''''''', cons(a'''''''''', k'''''''''''')))), cons(a''0'''', empty)) -> F(cons(a''0'''', empty), cons(a''''''1, cons(a'''''''', cons(a'''''''''', k''''''''''''))))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a''''''0, cons(a'''''''''', k''''''''''''))), cons(a''0'''', cons(a'''''''0, k'''''''''0))) -> F(cons(a''0'''', cons(a'''''''0, k'''''''''0)), cons(a''''''0, cons(a'''''''''', k'''''''''''')))
two new Dependency Pairs are created:

F(cons(a, cons(a''''''0'', cons(a'''''''''''', k''''''''''''''))), cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k''''''''''''''')))) -> F(cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k'''''''''''''''))), cons(a''''''0'', cons(a'''''''''''', k'''''''''''''')))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''0'''''', cons(a'''''''0'', empty))) -> F(cons(a''0'''''', cons(a'''''''0'', empty)), cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 13
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(cons(a, cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''0'''''', cons(a'''''''0'', empty))) -> F(cons(a''0'''''', cons(a'''''''0'', empty)), cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', k''''''''''''''))), cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k''''''''''''''')))) -> F(cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k'''''''''''''''))), cons(a''''''0'', cons(a'''''''''''', k'''''''''''''')))
F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))
F(cons(a, cons(a''''', cons(a'''''''', cons(a'''''''''''', k'''''''''''''')))), empty) -> F(empty, cons(a''''', cons(a'''''''', cons(a'''''''''''', k''''''''''''''))))
F(cons(a, empty), cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k''''''''''''''''))))) -> F(cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k'''''''''''''''')))), empty)
F(cons(a, cons(a''''''1, cons(a'''''''', cons(a'''''''''', k'''''''''''')))), cons(a''0'''', empty)) -> F(cons(a''0'''', empty), cons(a''''''1, cons(a'''''''', cons(a'''''''''', k''''''''''''))))
F(cons(a, cons(a''''''0, empty)), cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k''''''''''')))) -> F(cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k'''''''''''))), cons(a''''''0, empty))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(empty, cons(a''', cons(a''''', cons(a'''''''''', k'''''''''''')))) -> F(cons(a''', cons(a''''', cons(a'''''''''', k''''''''''''))), cons(a''''', cons(a'''''''''', k'''''''''''')))
one new Dependency Pair is created:

F(empty, cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))) -> F(cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))), cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 14
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(cons(a, cons(a''''''0'', cons(a'''''''''''', k''''''''''''''))), cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k''''''''''''''')))) -> F(cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k'''''''''''''''))), cons(a''''''0'', cons(a'''''''''''', k'''''''''''''')))
F(empty, cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))) -> F(cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))), cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))
F(cons(a, cons(a''''', cons(a'''''''', cons(a'''''''''''', k'''''''''''''')))), empty) -> F(empty, cons(a''''', cons(a'''''''', cons(a'''''''''''', k''''''''''''''))))
F(cons(a, empty), cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k''''''''''''''''))))) -> F(cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k'''''''''''''''')))), empty)
F(cons(a, cons(a''''''1, cons(a'''''''', cons(a'''''''''', k'''''''''''')))), cons(a''0'''', empty)) -> F(cons(a''0'''', empty), cons(a''''''1, cons(a'''''''', cons(a'''''''''', k''''''''''''))))
F(cons(a, cons(a''''''0, empty)), cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k''''''''''')))) -> F(cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k'''''''''''))), cons(a''''''0, empty))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''0'''''', cons(a'''''''0'', empty))) -> F(cons(a''0'''''', cons(a'''''''0'', empty)), cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a''''', cons(a'''''''', cons(a'''''''''''', k'''''''''''''')))), empty) -> F(empty, cons(a''''', cons(a'''''''', cons(a'''''''''''', k''''''''''''''))))
one new Dependency Pair is created:

F(cons(a, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k''''''''''''''''''''))))), empty) -> F(empty, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k'''''''''''''''''''')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 15
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(empty, cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))) -> F(cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))), cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))
F(cons(a, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k''''''''''''''''''''))))), empty) -> F(empty, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k'''''''''''''''''''')))))
F(cons(a, empty), cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k''''''''''''''''))))) -> F(cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k'''''''''''''''')))), empty)
F(cons(a, cons(a''''''1, cons(a'''''''', cons(a'''''''''', k'''''''''''')))), cons(a''0'''', empty)) -> F(cons(a''0'''', empty), cons(a''''''1, cons(a'''''''', cons(a'''''''''', k''''''''''''))))
F(cons(a, cons(a''''''0, empty)), cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k''''''''''')))) -> F(cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k'''''''''''))), cons(a''''''0, empty))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''0'''''', cons(a'''''''0'', empty))) -> F(cons(a''0'''''', cons(a'''''''0'', empty)), cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', k''''''''''''''))), cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k''''''''''''''')))) -> F(cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k'''''''''''''''))), cons(a''''''0'', cons(a'''''''''''', k'''''''''''''')))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a''''''0, empty)), cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k''''''''''')))) -> F(cons(a''0'''', cons(a'''''''0, cons(a'''''''''', k'''''''''''))), cons(a''''''0, empty))
one new Dependency Pair is created:

F(cons(a, cons(a''''''0', empty)), cons(a''0'''''', cons(a'''''''0', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))) -> F(cons(a''0'''''', cons(a'''''''0', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''''''0', empty))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 16
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(cons(a, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k''''''''''''''''''''))))), empty) -> F(empty, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k'''''''''''''''''''')))))
F(cons(a, empty), cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k''''''''''''''''))))) -> F(cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k'''''''''''''''')))), empty)
F(cons(a, cons(a''''''1, cons(a'''''''', cons(a'''''''''', k'''''''''''')))), cons(a''0'''', empty)) -> F(cons(a''0'''', empty), cons(a''''''1, cons(a'''''''', cons(a'''''''''', k''''''''''''))))
F(cons(a, cons(a''''''0', empty)), cons(a''0'''''', cons(a'''''''0', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))) -> F(cons(a''0'''''', cons(a'''''''0', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''''''0', empty))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''0'''''', cons(a'''''''0'', empty))) -> F(cons(a''0'''''', cons(a'''''''0'', empty)), cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', k''''''''''''''))), cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k''''''''''''''')))) -> F(cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k'''''''''''''''))), cons(a''''''0'', cons(a'''''''''''', k'''''''''''''')))
F(empty, cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))) -> F(cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))), cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, cons(a''''''1, cons(a'''''''', cons(a'''''''''', k'''''''''''')))), cons(a''0'''', empty)) -> F(cons(a''0'''', empty), cons(a''''''1, cons(a'''''''', cons(a'''''''''', k''''''''''''))))
one new Dependency Pair is created:

F(cons(a, cons(a''''''1', cons(a''''''''', cons(a'''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))), cons(a''0''''', empty)) -> F(cons(a''0''''', empty), cons(a''''''1', cons(a''''''''', cons(a'''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))))

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 17
                 ↳Forward Instantiation Transformation


Dependency Pairs:

F(cons(a, empty), cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k''''''''''''''''))))) -> F(cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k'''''''''''''''')))), empty)
F(cons(a, cons(a''''''1', cons(a''''''''', cons(a'''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))), cons(a''0''''', empty)) -> F(cons(a''0''''', empty), cons(a''''''1', cons(a''''''''', cons(a'''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))))
F(cons(a, cons(a''''''0', empty)), cons(a''0'''''', cons(a'''''''0', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))) -> F(cons(a''0'''''', cons(a'''''''0', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''''''0', empty))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''0'''''', cons(a'''''''0'', empty))) -> F(cons(a''0'''''', cons(a'''''''0'', empty)), cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', k''''''''''''''))), cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k''''''''''''''')))) -> F(cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k'''''''''''''''))), cons(a''''''0'', cons(a'''''''''''', k'''''''''''''')))
F(empty, cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))) -> F(cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))), cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))
F(cons(a, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k''''''''''''''''''''))))), empty) -> F(empty, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k'''''''''''''''''''')))))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost




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

F(cons(a, empty), cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k''''''''''''''''))))) -> F(cons(a''0'', cons(a''''''0, cons(a'''''''''', cons(a'''''''''''''', k'''''''''''''''')))), empty)
one new Dependency Pair is created:

F(cons(a, empty), cons(a''0''', cons(a''''''0', cons(a'''''''''''', cons(a'''''''''''''''', cons(a'''''''''''''''''''', k'''''''''''''''''''''')))))) -> F(cons(a''0''', cons(a''''''0', cons(a'''''''''''', cons(a'''''''''''''''', cons(a'''''''''''''''''''', k''''''''''''''''''''''))))), empty)

The transformation is resulting in one new DP problem: 



   R
     ↳DPs
       →DP Problem 1
         ↳FwdInst
           →DP Problem 2
             ↳FwdInst
             ...
               →DP Problem 18
                 ↳Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

F(cons(a, cons(a''''''0', empty)), cons(a''0'''''', cons(a'''''''0', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))) -> F(cons(a''0'''''', cons(a'''''''0', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''''''0', empty))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k'''''''''''''')))), cons(a''0'''''', cons(a'''''''0'', empty))) -> F(cons(a''0'''''', cons(a'''''''0'', empty)), cons(a''''''0'', cons(a'''''''''''', cons(a''''''''''''', k''''''''''''''))))
F(cons(a, cons(a''''''0'', cons(a'''''''''''', k''''''''''''''))), cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k''''''''''''''')))) -> F(cons(a''0'''''', cons(a'''''''0'', cons(a''''''''''''', k'''''''''''''''))), cons(a''''''0'', cons(a'''''''''''', k'''''''''''''')))
F(empty, cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))) -> F(cons(a'''', cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))), cons(a'''''', cons(a''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))
F(cons(a, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k''''''''''''''''''''))))), empty) -> F(empty, cons(a'''''', cons(a''''''''', cons(a'''''''''''''', cons(a'''''''''''''''''', k'''''''''''''''''''')))))
F(cons(a, empty), cons(a''0''', cons(a''''''0', cons(a'''''''''''', cons(a'''''''''''''''', cons(a'''''''''''''''''''', k'''''''''''''''''''''')))))) -> F(cons(a''0''', cons(a''''''0', cons(a'''''''''''', cons(a'''''''''''''''', cons(a'''''''''''''''''''', k''''''''''''''''''''''))))), empty)
F(cons(a, cons(a''''''1', cons(a''''''''', cons(a'''''''''''', cons(a'''''''''''''''', k''''''''''''''''''))))), cons(a''0''''', empty)) -> F(cons(a''0''''', empty), cons(a''''''1', cons(a''''''''', cons(a'''''''''''', cons(a'''''''''''''''', k'''''''''''''''''')))))


Rules:


f(x, empty) -> x
f(empty, cons(a, k)) -> f(cons(a, k), k)
f(cons(a, k), y) -> f(y, k)


Strategy:

innermost



Innermost Termination of R could not be shown.
Duration:
0:02 minutes