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