Termination Proof using AProVE

Term Rewriting System R:
[X, Y, L]
rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

REV1(X, cons(Y, L)) -> REV1(Y, L)
REV(cons(X, L)) -> REV1(X, L)
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV2(X, cons(Y, L)) -> REV(rev2(Y, L))
REV2(X, cons(Y, L)) -> REV2(Y, L)

Furthermore, R contains two SCCs.

     ↳DPs

       →DP Problem 1

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳Nar

Dependency Pair:

REV1(X, cons(Y, L)) -> REV1(Y, L)

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

The following dependency pair can be strictly oriented:

REV1(X, cons(Y, L)) -> REV1(Y, L)

There are no usable rules using the Ce-refinement that need to be oriented.
Used ordering: Homeomorphic Embedding Order with EMB
resulting in one new DP problem.
Used Argument Filtering System:

REV1(x₁, x₂) -> x₂
cons(x₁, x₂) -> cons(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 3

             ↳Dependency Graph

       →DP Problem 2

         ↳Nar

Dependency Pair:

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(rev2(Y, L))
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y, L)) -> REV(rev2(Y, L))

two new Dependency Pairs are created:

REV2(X, cons(Y', nil)) -> REV(nil)
REV2(X, cons(Y0, cons(Y'', L''))) -> REV(rev(cons(Y0, rev(rev2(Y'', L'')))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0, cons(Y'', L''))) -> REV(rev(cons(Y0, rev(rev2(Y'', L'')))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV2(X, cons(Y, L)) -> REV2(Y, L)

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y'', L''))) -> REV(rev(cons(Y0, rev(rev2(Y'', L'')))))

three new Dependency Pairs are created:

REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y0, cons(Y''', nil))) -> REV(rev(cons(Y0, rev(nil))))
REV2(X, cons(Y0, cons(Y''', cons(Y', L')))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev2(Y', L'))))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 5

                 ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0, cons(Y''', cons(Y', L')))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev2(Y', L'))))))))
REV2(X, cons(Y0, cons(Y''', nil))) -> REV(rev(cons(Y0, rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y''', nil))) -> REV(rev(cons(Y0, rev(nil))))

two new Dependency Pairs are created:

REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0, cons(Y''', nil))) -> REV(rev(cons(Y0, nil)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 6

                 ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0, cons(Y''', nil))) -> REV(rev(cons(Y0, nil)))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y0, cons(Y''', cons(Y', L')))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev2(Y', L'))))))))

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y''', cons(Y', L')))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev2(Y', L'))))))))

four new Dependency Pairs are created:

REV2(X, cons(Y0', cons(Y'''', cons(Y'', L'')))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L'')))))), rev2(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', L'')))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(rev2(Y'', L''))), rev2(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(nil)))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1, L''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev2(Y1, L'')))))))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 7

                 ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1, L''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev2(Y1, L'')))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(nil)))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', L'')))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(rev2(Y'', L''))), rev2(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', L'')))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L'')))))), rev2(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y0, cons(Y''', nil))) -> REV(rev(cons(Y0, nil)))

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y''', nil))) -> REV(rev(cons(Y0, nil)))

one new Dependency Pair is created:

REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', nil), rev2(Y0', nil)))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 8

                 ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', nil), rev2(Y0', nil)))
REV2(X, cons(Y0, cons(Y''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(nil)))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', L'')))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(rev2(Y'', L''))), rev2(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', L'')))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L'')))))), rev2(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1, L''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev2(Y1, L'')))))))))))

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(nil)))))))

three new Dependency Pairs are created:

REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(nil))))), rev2(Y0', rev(rev(cons(Y'''', rev(nil)))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil)))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', nil))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 9

                 ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0, cons(Y''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', nil))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(nil))))), rev2(Y0', rev(rev(cons(Y'''', rev(nil)))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1, L''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev2(Y1, L'')))))))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', L'')))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(rev2(Y'', L''))), rev2(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', L'')))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L'')))))), rev2(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', nil), rev2(Y0', nil)))

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1, L''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev2(Y1, L'')))))))))))

five new Dependency Pairs are created:

REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L'''))))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))), rev2(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(rev2(Y1', L'''))), rev2(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y', L')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(rev2(Y', L'))))))))))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 10

                 ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y', L')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(rev2(Y', L'))))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(rev2(Y1', L'''))), rev2(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))), rev2(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L'''))))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(nil))))), rev2(Y0', rev(rev(cons(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', nil), rev2(Y0', nil)))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', L'')))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(rev2(Y'', L''))), rev2(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', L'')))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L'')))))), rev2(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y0, cons(Y''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', nil))))))

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', nil))))))

two new Dependency Pairs are created:

REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', nil)))), rev2(Y0', rev(rev(cons(Y'''', nil))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', nil), rev2(Y'''', nil))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 11

                 ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', nil), rev2(Y'''', nil))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', nil)))), rev2(Y0', rev(rev(cons(Y'''', nil))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(rev2(Y1', L'''))), rev2(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))), rev2(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L'''))))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(nil))))), rev2(Y0', rev(rev(cons(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', nil), rev2(Y0', nil)))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', L'')))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(rev2(Y'', L''))), rev2(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', L'')))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L'')))))), rev2(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y', L')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(rev2(Y', L'))))))))))))))

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(nil))))))))))

four new Dependency Pairs are created:

REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1', nil))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(nil)))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(nil))))), rev2(Y''''', rev(rev(cons(Y'''', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', nil)))))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 12

                 ↳Narrowing Transformation

Dependency Pairs:

REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', nil)))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(nil))))), rev2(Y''''', rev(rev(cons(Y'''', rev(nil))))))))))
REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1', nil))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(nil)))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(nil))))))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', nil)))), rev2(Y0', rev(rev(cons(Y'''', nil))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y', L')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(rev2(Y', L'))))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(rev2(Y1', L'''))), rev2(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))), rev2(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L'''))))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(nil))))), rev2(Y0', rev(rev(cons(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', nil), rev2(Y0', nil)))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', L'')))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(rev2(Y'', L''))), rev2(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', L'')))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L'')))))), rev2(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', nil), rev2(Y'''', nil))))))

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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

REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y', L')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(rev2(Y', L'))))))))))))))

six new Dependency Pairs are created:

REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1'', cons(Y'0, L'')))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L'')))))))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L''))))))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1'', cons(Y'0, L'')))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L''))))))))), rev2(Y''''', rev(rev(cons(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L''))))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1'', cons(Y'0, L'')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L'')))))), rev2(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L''))))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1'', cons(Y'0, L'')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(cons(rev1(Y1'', rev(rev2(Y'0, L''))), rev2(Y1'', rev(rev2(Y'0, L''))))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y'0, nil)))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(nil)))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y'0, cons(Y1, L''))))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(rev(cons(Y'0, rev(rev2(Y1, L'')))))))))))))))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Nar

           →DP Problem 4

             ↳Nar

...

               →DP Problem 13

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y'0, cons(Y1, L''))))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(rev(cons(Y'0, rev(rev2(Y1, L'')))))))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', cons(Y'0, nil)))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(rev(cons(Y1', rev(nil)))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1'', cons(Y'0, L'')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', rev(cons(rev1(Y1'', rev(rev2(Y'0, L''))), rev2(Y1'', rev(rev2(Y'0, L''))))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1'', cons(Y'0, L'')))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L'')))))), rev2(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L''))))))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1'', cons(Y'0, L'')))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L''))))))))), rev2(Y''''', rev(rev(cons(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L''))))))))))))))
REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1'', cons(Y'0, L'')))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L'')))))))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev(cons(Y1'', rev(rev2(Y'0, L''))))))))))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(nil))))), rev2(Y''''', rev(rev(cons(Y'''', rev(nil))))))))))
REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1', nil))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(nil)))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(nil))))))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', nil), rev2(Y'''', nil))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', nil)))), rev2(Y0', rev(rev(cons(Y'''', nil))))))
REV2(X, cons(Y0, cons(Y''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(cons(rev1(Y'''', rev(rev2(Y1', L'''))), rev2(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(rev(cons(Y0, rev(cons(rev1(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))), rev2(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0', cons(Y''''', cons(Y'''', cons(Y1', L'''))))) -> REV(cons(rev1(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L'''))))))))), rev2(Y0', rev(rev(cons(Y''''', rev(rev(cons(Y'''', rev(rev2(Y1', L''')))))))))))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', nil)))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(nil)), rev2(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', nil)))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(nil))))), rev2(Y0', rev(rev(cons(Y'''', rev(nil)))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', nil), rev2(Y0', nil)))
REV2(X, cons(Y0, cons(Y'''', cons(Y'', L'')))) -> REV(rev(cons(Y0, rev(cons(rev1(Y'''', rev(rev2(Y'', L''))), rev2(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y'''', cons(Y'', L'')))) -> REV(cons(rev1(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L'')))))), rev2(Y0', rev(rev(cons(Y'''', rev(rev2(Y'', L''))))))))
REV2(X, cons(Y0', cons(Y''', nil))) -> REV(cons(rev1(Y0', rev(nil)), rev2(Y0', rev(nil))))
REV2(X, cons(Y0', cons(Y''', L'''))) -> REV(cons(rev1(Y0', rev(rev2(Y''', L'''))), rev2(Y0', rev(rev2(Y''', L''')))))
REV2(X, cons(Y, L)) -> REV2(Y, L)
REV2(X, cons(Y, L)) -> REV(cons(X, rev(rev2(Y, L))))
REV(cons(X, L)) -> REV2(X, L)
REV2(X, cons(Y0, cons(Y''', cons(Y'', cons(Y1', nil))))) -> REV(rev(cons(Y0, rev(rev(cons(Y''', rev(rev(cons(Y'', nil)))))))))

Rules:

rev1(0, nil) -> 0
rev1(s(X), nil) -> s(X)
rev1(X, cons(Y, L)) -> rev1(Y, L)
rev(nil) -> nil
rev(cons(X, L)) -> cons(rev1(X, L), rev2(X, L))
rev2(X, nil) -> nil
rev2(X, cons(Y, L)) -> rev(cons(X, rev(rev2(Y, L))))

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