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.

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

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

R
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 w.r.t. to the implicit AFS can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(++'(x1, x2)) =  1 + x1 POL(++(x1, x2)) =  1 + x1 + x2 POL(nil) =  1

resulting in one new DP problem.

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

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

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

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

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

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

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

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

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

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

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

R
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 w.r.t. to the implicit AFS can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(unit(x1)) =  x1 POL(++(x1, x2)) =  1 + x1 + x2 POL(FLATTEN(x1)) =  1 + x1 POL(nil) =  1

resulting in one new DP problem.

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

R
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 w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(unit(x1)) =  1 + x1 POL(FLATTEN(x1)) =  1 + x1

resulting in one new DP problem.

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

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

R
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 w.r.t. to the implicit AFS can be oriented:

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

Used ordering: Polynomial ordering with Polynomial interpretation:
 POL(REV(x1)) =  1 + x1 POL(++(x1, x2)) =  1 + x1 + x2 POL(nil) =  1

resulting in one new DP problem.

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