Termination Proof using AProVE

Term Rewriting System R:
[x, y, z]
flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

FLATTEN(unit(x)) -> FLATTEN(x)
FLATTEN(++(x, y)) -> ++'(flatten(x), flatten(y))
FLATTEN(++(x, y)) -> FLATTEN(x)
FLATTEN(++(x, y)) -> FLATTEN(y)
FLATTEN(++(unit(x), y)) -> ++'(flatten(x), flatten(y))
FLATTEN(++(unit(x), y)) -> FLATTEN(x)
FLATTEN(++(unit(x), y)) -> FLATTEN(y)
REV(++(x, y)) -> ++'(rev(y), rev(x))
REV(++(x, y)) -> REV(y)
REV(++(x, y)) -> REV(x)
++'(++(x, y), z) -> ++'(x, ++(y, z))
++'(++(x, y), z) -> ++'(y, z)

Furthermore, R contains three SCCs.

     ↳DPs

       →DP Problem 1

         ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

Dependency Pair:

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

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

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 4

             ↳Polynomial Ordering

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

Dependency Pair:

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

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

The following dependency pair can be strictly oriented:

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

Additionally, the following usable rules for innermost can be oriented:

++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(nil) = 1

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

           →DP Problem 4

             ↳Polo

...

               →DP Problem 5

                 ↳Dependency Graph

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

Dependency Pair:

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(x), y)) -> FLATTEN(y)
FLATTEN(++(unit(x), y)) -> FLATTEN(x)
FLATTEN(++(x, y)) -> FLATTEN(y)
FLATTEN(++(x, y)) -> FLATTEN(x)
FLATTEN(unit(x)) -> FLATTEN(x)

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(unit(x)) -> FLATTEN(x)

three new Dependency Pairs are created:

FLATTEN(unit(unit(x''))) -> FLATTEN(unit(x''))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(x), y)) -> FLATTEN(x)
FLATTEN(++(x, y)) -> FLATTEN(y)
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(unit(x''))) -> FLATTEN(unit(x''))
FLATTEN(++(x, y)) -> FLATTEN(x)
FLATTEN(++(unit(x), y)) -> FLATTEN(y)

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(++(x, y)) -> FLATTEN(x)

three new Dependency Pairs are created:

FLATTEN(++(unit(unit(x'''')), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 7

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(unit(x'''')), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(unit(x''))) -> FLATTEN(unit(x''))
FLATTEN(++(unit(x), y)) -> FLATTEN(y)
FLATTEN(++(unit(x), y)) -> FLATTEN(x)
FLATTEN(++(x, y)) -> FLATTEN(y)
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(++(x, y)) -> FLATTEN(y)

eight new Dependency Pairs are created:

FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 8

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(x, unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(unit(x'''')), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(unit(unit(x''))) -> FLATTEN(unit(x''))
FLATTEN(++(unit(x), y)) -> FLATTEN(y)
FLATTEN(++(unit(x), y)) -> FLATTEN(x)
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(++(unit(x), y)) -> FLATTEN(x)

15 new Dependency Pairs are created:

FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(unit(unit(x''''))), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 9

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(unit(unit(x''''))), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(x, unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(unit(x'''')), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(unit(x''))) -> FLATTEN(unit(x''))
FLATTEN(++(unit(x), y)) -> FLATTEN(y)
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(++(unit(x), y)) -> FLATTEN(y)

30 new Dependency Pairs are created:

FLATTEN(++(unit(x), ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(x), unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(x), unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(x), ++(x'', ++(x'''', y'''')))) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(x''''), y'''')))) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(x'', unit(unit(x''''''))))) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(x'''''', y''''''))))) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(unit(x''''''), y''''''))))) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), ++(x'', ++(unit(unit(x'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''), y'''')), y''))) -> FLATTEN(++(unit(++(unit(x''''), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(unit(x''''''))), y''))) -> FLATTEN(++(unit(unit(unit(x''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(unit(++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(unit(x'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(unit(x'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(unit(x'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(unit(x'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 10

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(unit(x'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(unit(x'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(unit(x'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(unit(x'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(unit(++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(unit(x''''''))), y''))) -> FLATTEN(++(unit(unit(unit(x''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''), y'''')), y''))) -> FLATTEN(++(unit(++(unit(x''''), y'''')), y''))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(unit(x'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', unit(++(unit(x''''''), y''''''))))) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(x'''''', y''''''))))) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(unit(x''''''))))) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', ++(unit(x''''), y'''')))) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(x'''', y'''')))) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(x), unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(x), unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(unit(unit(x''''))), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(x, unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(unit(x''))) -> FLATTEN(unit(x''))
FLATTEN(++(unit(unit(x'''')), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(unit(unit(x''))) -> FLATTEN(unit(x''))

three new Dependency Pairs are created:

FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(unit(unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 11

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(unit(x'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(unit(x'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(unit(x'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(unit(x'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(unit(++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(unit(x''''''))), y''))) -> FLATTEN(++(unit(unit(unit(x''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''), y'''')), y''))) -> FLATTEN(++(unit(++(unit(x''''), y'''')), y''))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(unit(x'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', unit(++(unit(x''''''), y''''''))))) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(x'''''', y''''''))))) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(unit(x''''''))))) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', ++(unit(x''''), y'''')))) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(x'''', y'''')))) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(x), unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(x), unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(unit(unit(x''''))), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(unit(unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(unit(x'''')), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(++(unit(unit(x'''')), y)) -> FLATTEN(unit(unit(x'''')))

three new Dependency Pairs are created:

FLATTEN(++(unit(unit(unit(x''''''))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(unit(++(x'''''', y''''''))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 12

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(unit(x'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(unit(x'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(unit(x'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(unit(x'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(unit(++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(unit(x''''''))), y''))) -> FLATTEN(++(unit(unit(unit(x''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''), y'''')), y''))) -> FLATTEN(++(unit(++(unit(x''''), y'''')), y''))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(unit(x'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', unit(++(unit(x''''''), y''''''))))) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(x'''''', y''''''))))) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(unit(++(x'''''', y''''''))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(x''''''))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', unit(unit(x''''''))))) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', ++(unit(x''''), y'''')))) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(x'''', y'''')))) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(x), unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(x), unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(unit(unit(x''''))), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(x, unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(++(x, unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))

three new Dependency Pairs are created:

FLATTEN(++(x, unit(unit(unit(x''''''))))) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(x, unit(unit(++(x'''''', y''''''))))) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(x, unit(unit(++(unit(x''''''), y''''''))))) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 13

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(unit(x'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(unit(x'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(unit(x'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(unit(x'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(unit(++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(unit(x''''''))), y''))) -> FLATTEN(++(unit(unit(unit(x''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''), y'''')), y''))) -> FLATTEN(++(unit(++(unit(x''''), y'''')), y''))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(unit(x'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', unit(++(unit(x''''''), y''''''))))) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(x'''''', y''''''))))) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(x, unit(unit(++(unit(x''''''), y''''''))))) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(x, unit(unit(++(x'''''', y''''''))))) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(x, unit(unit(unit(x''''''))))) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(unit(++(x'''''', y''''''))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(x''''''))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', unit(unit(x''''''))))) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', ++(unit(x''''), y'''')))) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(x'''', y'''')))) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(x), unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(x), unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(unit(unit(x''''))), y)) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(++(unit(unit(unit(x''''))), y)) -> FLATTEN(unit(unit(x'''')))

three new Dependency Pairs are created:

FLATTEN(++(unit(unit(unit(unit(x'''''')))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(unit(unit(++(x'''''', y'''''')))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 14

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(unit(x'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(unit(x'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(unit(x'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(unit(x'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(unit(++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(unit(x''''''))), y''))) -> FLATTEN(++(unit(unit(unit(x''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''), y'''')), y''))) -> FLATTEN(++(unit(++(unit(x''''), y'''')), y''))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(unit(x'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', unit(++(unit(x''''''), y''''''))))) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(x'''''', y''''''))))) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(unit(unit(++(x'''''', y'''''')))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(unit(x'''''')))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(x, unit(unit(++(unit(x''''''), y''''''))))) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(x, unit(unit(++(x'''''', y''''''))))) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(x, unit(unit(unit(x''''''))))) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(unit(++(x'''''', y''''''))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(x''''''))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', unit(unit(x''''''))))) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', ++(unit(x''''), y'''')))) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(x'''', y'''')))) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(x), unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(x), unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(x), unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

FLATTEN(++(unit(x), unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))

three new Dependency Pairs are created:

FLATTEN(++(unit(x), unit(unit(unit(x''''''))))) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(x), unit(unit(++(x'''''', y''''''))))) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(x), unit(unit(++(unit(x''''''), y''''''))))) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 15

                 ↳Polynomial Ordering

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(unit(x'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(unit(x'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(unit(x'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(unit(x'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(unit(++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(unit(x''''''))), y''))) -> FLATTEN(++(unit(unit(unit(x''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''), y'''')), y''))) -> FLATTEN(++(unit(++(unit(x''''), y'''')), y''))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(unit(x'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', unit(++(unit(x''''''), y''''''))))) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(x'''''', y''''''))))) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(x), unit(unit(++(unit(x''''''), y''''''))))) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), unit(unit(++(x'''''', y''''''))))) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(x), unit(unit(unit(x''''''))))) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(unit(unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(unit(unit(++(x'''''', y'''''')))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(unit(x'''''')))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(x, unit(unit(++(unit(x''''''), y''''''))))) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(x, unit(unit(++(x'''''', y''''''))))) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(x, unit(unit(unit(x''''''))))) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(unit(++(x'''''', y''''''))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(unit(unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(++(unit(unit(unit(x''''''))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', unit(unit(x''''''))))) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', ++(unit(x''''), y'''')))) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(x'''', y'''')))) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(x), unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(x), unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

The following dependency pairs can be strictly oriented:

FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(x'''''''''', y'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(unit(x'''''''''')), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(unit(x''''''''), y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(++(x'''''''', y'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', unit(unit(x'''''''')))), y''))) -> FLATTEN(++(unit(++(x'''', unit(unit(x'''''''')))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(unit(x''''''''), y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(++(x'''''''', y'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(unit(x'''''''')), y'''')), y''))) -> FLATTEN(++(unit(++(unit(unit(x'''''''')), y'''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(unit(x''''''), y''''''))), y''))) -> FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(++(x'''''', y''''''))), y''))) -> FLATTEN(++(unit(unit(++(x'''''', y''''''))), y''))
FLATTEN(++(unit(x), ++(unit(unit(unit(x''''''))), y''))) -> FLATTEN(++(unit(unit(unit(x''''''))), y''))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''), y'''')), y''))) -> FLATTEN(++(unit(++(unit(x''''), y'''')), y''))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(unit(unit(x'''''''')), y'''')))) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(x), ++(x'', unit(++(unit(x''''''), y''''''))))) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), ++(x'', unit(++(x'''''', y''''''))))) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(x), unit(unit(++(unit(x''''''), y''''''))))) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(x), unit(unit(++(x'''''', y''''''))))) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(x), unit(unit(unit(x''''''))))) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(unit(unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(unit(unit(++(x'''''', y'''''')))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(unit(x'''''')))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(x, unit(unit(++(unit(x''''''), y''''''))))) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(x, unit(unit(++(x'''''', y''''''))))) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(x, unit(unit(unit(x''''''))))) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(unit(++(unit(x''''''), y''''''))), y)) -> FLATTEN(unit(unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(unit(++(x'''''', y''''''))), y)) -> FLATTEN(unit(unit(++(x'''''', y''''''))))
FLATTEN(++(unit(unit(unit(x''''''))), y)) -> FLATTEN(unit(unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', unit(unit(x''''''))))) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(x), ++(x'', ++(unit(x''''), y'''')))) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(x), ++(x'', ++(x'''', y'''')))) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(x), unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(x), unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(unit(x''''''''), y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(++(x'''''''', y'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(++(x'''''''', y'''''''')), y'''')))
FLATTEN(++(unit(++(x'', ++(unit(unit(x'''''''')), y''''))), y)) -> FLATTEN(++(x'', ++(unit(unit(x'''''''')), y'''')))
FLATTEN(++(unit(++(x'', unit(++(unit(x''''''), y'''''')))), y)) -> FLATTEN(++(x'', unit(++(unit(x''''''), y''''''))))
FLATTEN(++(unit(++(x'', unit(++(x'''''', y'''''')))), y)) -> FLATTEN(++(x'', unit(++(x'''''', y''''''))))
FLATTEN(++(unit(++(x'', unit(unit(x'''''')))), y)) -> FLATTEN(++(x'', unit(unit(x''''''))))
FLATTEN(++(unit(++(x'', ++(unit(x''''), y''''))), y)) -> FLATTEN(++(x'', ++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'', ++(x'''', y''''))), y)) -> FLATTEN(++(x'', ++(x'''', y'''')))
FLATTEN(++(unit(++(unit(++(unit(x''''''), y'''''')), y'')), y)) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(unit(++(unit(++(x'''''', y'''''')), y'')), y)) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(unit(x), ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(unit(++(unit(unit(x'''''')), y'')), y)) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(unit(unit(++(unit(x''''), y''''))), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(unit(++(x'''', y''''))), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(++(unit(x''), y'')), y)) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(unit(++(unit(x''''''), y'''''')), y''))) -> FLATTEN(++(unit(++(unit(x''''''), y'''''')), y''))
FLATTEN(++(x, ++(unit(++(x'''''', y'''''')), y''))) -> FLATTEN(++(unit(++(x'''''', y'''''')), y''))
FLATTEN(++(x, ++(unit(unit(x'''''')), y''))) -> FLATTEN(++(unit(unit(x'''''')), y''))
FLATTEN(++(x, unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(x, unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(x, ++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(++(x, ++(x'', y''))) -> FLATTEN(++(x'', y''))
FLATTEN(++(unit(++(unit(x''''), y'''')), y)) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(++(unit(++(x'''', y'''')), y)) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(++(unit(x), ++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))) -> FLATTEN(++(unit(++(x'''', ++(unit(++(unit(x''''''''''), y'''''''''')), y''''''))), y''))

Additionally, the following usable rules for innermost can be oriented:

++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(unit(x₁)) = x₁

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

POL(FLATTEN(x₁)) = 1 + x₁

POL(nil) = 1

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 16

                 ↳Dependency Graph

       →DP Problem 3

         ↳FwdInst

Dependency Pairs:

FLATTEN(unit(unit(++(unit(x''''), y'''')))) -> FLATTEN(unit(++(unit(x''''), y'''')))
FLATTEN(unit(unit(++(x'''', y'''')))) -> FLATTEN(unit(++(x'''', y'''')))
FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))
FLATTEN(unit(++(unit(x''), y''))) -> FLATTEN(++(unit(x''), y''))
FLATTEN(unit(++(x'', y''))) -> FLATTEN(++(x'', y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

Using the Dependency Graph the DP problem was split into 1 DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 17

                 ↳Polynomial Ordering

       →DP Problem 3

         ↳FwdInst

Dependency Pair:

FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

The following dependency pair can be strictly oriented:

FLATTEN(unit(unit(unit(x'''')))) -> FLATTEN(unit(unit(x'''')))

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(unit(x₁)) = 1 + x₁

POL(FLATTEN(x₁)) = 1 + x₁

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

           →DP Problem 6

             ↳FwdInst

...

               →DP Problem 18

                 ↳Dependency Graph

       →DP Problem 3

         ↳FwdInst

Dependency Pair:

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳Forward Instantiation Transformation

Dependency Pair:

REV(++(x, y)) -> REV(y)

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

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

REV(++(x, y)) -> REV(y)

one new Dependency Pair is created:

REV(++(x, ++(x'', y''))) -> REV(++(x'', y''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 19

             ↳Polynomial Ordering

Dependency Pair:

REV(++(x, ++(x'', y''))) -> REV(++(x'', y''))

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

The following dependency pair can be strictly oriented:

REV(++(x, ++(x'', y''))) -> REV(++(x'', y''))

Additionally, the following usable rules for innermost can be oriented:

++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(REV(x₁)) = x₁

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

POL(nil) = 1

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳FwdInst

       →DP Problem 2

         ↳FwdInst

       →DP Problem 3

         ↳FwdInst

           →DP Problem 19

             ↳Polo

...

               →DP Problem 20

                 ↳Dependency Graph

Dependency Pair:

Rules:

flatten(nil) -> nil
flatten(unit(x)) -> flatten(x)
flatten(++(x, y)) -> ++(flatten(x), flatten(y))
flatten(++(unit(x), y)) -> ++(flatten(x), flatten(y))
flatten(flatten(x)) -> flatten(x)
rev(nil) -> nil
rev(unit(x)) -> unit(x)
rev(++(x, y)) -> ++(rev(y), rev(x))
rev(rev(x)) -> x
++(x, nil) -> x
++(nil, y) -> y
++(++(x, y), z) -> ++(x, ++(y, z))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

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

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

POL(unit(x₁))	= x₁
POL(++(x₁, x₂))	= 1 + x₁ + x₂
POL(FLATTEN(x₁))	= 1 + x₁
POL(nil)	= 1

POL(REV(x₁))	= x₁
POL(++(x₁, x₂))	= 1 + x₁ + x₂
POL(nil)	= 1