Termination Proof using AProVE

Term Rewriting System R:
[x₀, y, l1₂, l2₁, x, l, a₄, l₃, l', l1, l2, l₅, a]
test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Innermost Termination of R to be shown.

     ↳Dependency Pair Analysis

R contains the following Dependency Pairs:

APPEND(l1₂, l2₁) -> MATCH₀(l1₂, l2₁, l1₂)
MATCH₀(l1₂, l2₁, Cons(x, l)) -> APPEND(l, l2₁)
PART(a₄, l₃) -> MATCH₁(a₄, l₃, l₃)
MATCH₁(a₄, l₃, Cons(x, l')) -> MATCH₂(x, l', a₄, l₃, part(a₄, l'))
MATCH₁(a₄, l₃, Cons(x, l')) -> PART(a₄, l')
MATCH₂(x, l', a₄, l₃, Pair(l1, l2)) -> MATCH₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
MATCH₂(x, l', a₄, l₃, Pair(l1, l2)) -> TEST(a₄, x)
QUICK(l₅) -> MATCH₄(l₅, l₅)
MATCH₄(l₅, Cons(a, l')) -> MATCH₅(a, l', l₅, part(a, l'))
MATCH₄(l₅, Cons(a, l')) -> PART(a, l')
MATCH₅(a, l', l₅, Pair(l1, l2)) -> APPEND(quick(l1), Cons(a, quick(l2)))
MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l1)
MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l2)

Furthermore, R contains three SCCs.

     ↳DPs

       →DP Problem 1

         ↳Instantiation Transformation

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

Dependency Pairs:

MATCH₀(l1₂, l2₁, Cons(x, l)) -> APPEND(l, l2₁)
APPEND(l1₂, l2₁) -> MATCH₀(l1₂, l2₁, l1₂)

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₀(l1₂, l2₁, Cons(x, l)) -> APPEND(l, l2₁)

one new Dependency Pair is created:

MATCH₀(Cons(x', l'), l2_1'', Cons(x', l')) -> APPEND(l', l2_1'')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 4

             ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

Dependency Pairs:

MATCH₀(Cons(x', l'), l2_1'', Cons(x', l')) -> APPEND(l', l2_1'')
APPEND(l1₂, l2₁) -> MATCH₀(l1₂, l2₁, l1₂)

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

APPEND(l1₂, l2₁) -> MATCH₀(l1₂, l2₁, l1₂)

one new Dependency Pair is created:

APPEND(Cons(x'''', l''''), l2_1') -> MATCH₀(Cons(x'''', l''''), l2_1', Cons(x'''', l''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 5

                 ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

Dependency Pairs:

APPEND(Cons(x'''', l''''), l2_1') -> MATCH₀(Cons(x'''', l''''), l2_1', Cons(x'''', l''''))
MATCH₀(Cons(x', l'), l2_1'', Cons(x', l')) -> APPEND(l', l2_1'')

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₀(Cons(x', l'), l2_1'', Cons(x', l')) -> APPEND(l', l2_1'')

one new Dependency Pair is created:

MATCH₀(Cons(x', Cons(x'''''', l'''''')), l2_1'''', Cons(x', Cons(x'''''', l''''''))) -> APPEND(Cons(x'''''', l''''''), l2_1'''')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 6

                 ↳Forward Instantiation Transformation

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

Dependency Pairs:

MATCH₀(Cons(x', Cons(x'''''', l'''''')), l2_1'''', Cons(x', Cons(x'''''', l''''''))) -> APPEND(Cons(x'''''', l''''''), l2_1'''')
APPEND(Cons(x'''', l''''), l2_1') -> MATCH₀(Cons(x'''', l''''), l2_1', Cons(x'''', l''''))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

APPEND(Cons(x'''', l''''), l2_1') -> MATCH₀(Cons(x'''', l''''), l2_1', Cons(x'''', l''''))

one new Dependency Pair is created:

APPEND(Cons(x''''', Cons(x''''''''', l''''''''')), l2_1'') -> MATCH₀(Cons(x''''', Cons(x''''''''', l''''''''')), l2_1'', Cons(x''''', Cons(x''''''''', l''''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 7

                 ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

Dependency Pairs:

APPEND(Cons(x''''', Cons(x''''''''', l''''''''')), l2_1'') -> MATCH₀(Cons(x''''', Cons(x''''''''', l''''''''')), l2_1'', Cons(x''''', Cons(x''''''''', l''''''''')))
MATCH₀(Cons(x', Cons(x'''''', l'''''')), l2_1'''', Cons(x', Cons(x'''''', l''''''))) -> APPEND(Cons(x'''''', l''''''), l2_1'''')

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

MATCH₀(Cons(x', Cons(x'''''', l'''''')), l2_1'''', Cons(x', Cons(x'''''', l''''''))) -> APPEND(Cons(x'''''', l''''''), l2_1'''')

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

MATCH₀(x₁, x₂, x₃) -> x₁
Cons(x₁, x₂) -> Cons(x₁, x₂)
APPEND(x₁, x₂) -> x₁

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 8

                 ↳Dependency Graph

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

Dependency Pair:

APPEND(Cons(x''''', Cons(x''''''''', l''''''''')), l2_1'') -> MATCH₀(Cons(x''''', Cons(x''''''''', l''''''''')), l2_1'', Cons(x''''', Cons(x''''''''', l''''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Instantiation Transformation

       →DP Problem 3

         ↳Nar

Dependency Pairs:

MATCH₁(a₄, l₃, Cons(x, l')) -> PART(a₄, l')
PART(a₄, l₃) -> MATCH₁(a₄, l₃, l₃)

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₁(a₄, l₃, Cons(x, l')) -> PART(a₄, l')

one new Dependency Pair is created:

MATCH₁(a_4'', Cons(x', l''), Cons(x', l'')) -> PART(a_4'', l'')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 9

             ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Nar

Dependency Pairs:

MATCH₁(a_4'', Cons(x', l''), Cons(x', l'')) -> PART(a_4'', l'')
PART(a₄, l₃) -> MATCH₁(a₄, l₃, l₃)

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

PART(a₄, l₃) -> MATCH₁(a₄, l₃, l₃)

one new Dependency Pair is created:

PART(a_4', Cons(x'''', l''''')) -> MATCH₁(a_4', Cons(x'''', l'''''), Cons(x'''', l'''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 9

             ↳FwdInst

...

               →DP Problem 10

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Nar

Dependency Pairs:

PART(a_4', Cons(x'''', l''''')) -> MATCH₁(a_4', Cons(x'''', l'''''), Cons(x'''', l'''''))
MATCH₁(a_4'', Cons(x', l''), Cons(x', l'')) -> PART(a_4'', l'')

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₁(a_4'', Cons(x', l''), Cons(x', l'')) -> PART(a_4'', l'')

one new Dependency Pair is created:

MATCH₁(a_4'''', Cons(x', Cons(x'''''', l''''''')), Cons(x', Cons(x'''''', l'''''''))) -> PART(a_4'''', Cons(x'''''', l'''''''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 9

             ↳FwdInst

...

               →DP Problem 11

                 ↳Forward Instantiation Transformation

       →DP Problem 3

         ↳Nar

Dependency Pairs:

MATCH₁(a_4'''', Cons(x', Cons(x'''''', l''''''')), Cons(x', Cons(x'''''', l'''''''))) -> PART(a_4'''', Cons(x'''''', l'''''''))
PART(a_4', Cons(x'''', l''''')) -> MATCH₁(a_4', Cons(x'''', l'''''), Cons(x'''', l'''''))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

PART(a_4', Cons(x'''', l''''')) -> MATCH₁(a_4', Cons(x'''', l'''''), Cons(x'''', l'''''))

one new Dependency Pair is created:

PART(a_4'', Cons(x''''', Cons(x''''''''', l''''''''''))) -> MATCH₁(a_4'', Cons(x''''', Cons(x''''''''', l'''''''''')), Cons(x''''', Cons(x''''''''', l'''''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 9

             ↳FwdInst

...

               →DP Problem 12

                 ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳Nar

Dependency Pairs:

PART(a_4'', Cons(x''''', Cons(x''''''''', l''''''''''))) -> MATCH₁(a_4'', Cons(x''''', Cons(x''''''''', l'''''''''')), Cons(x''''', Cons(x''''''''', l'''''''''')))
MATCH₁(a_4'''', Cons(x', Cons(x'''''', l''''''')), Cons(x', Cons(x'''''', l'''''''))) -> PART(a_4'''', Cons(x'''''', l'''''''))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

The following dependency pair can be strictly oriented:

MATCH₁(a_4'''', Cons(x', Cons(x'''''', l''''''')), Cons(x', Cons(x'''''', l'''''''))) -> PART(a_4'''', Cons(x'''''', l'''''''))

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

MATCH₁(x₁, x₂, x₃) -> x₂
Cons(x₁, x₂) -> Cons(x₁, x₂)
PART(x₁, x₂) -> x₂

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 9

             ↳FwdInst

...

               →DP Problem 13

                 ↳Dependency Graph

       →DP Problem 3

         ↳Nar

Dependency Pair:

PART(a_4'', Cons(x''''', Cons(x''''''''', l''''''''''))) -> MATCH₁(a_4'', Cons(x''''', Cons(x''''''''', l'''''''''')), Cons(x''''', Cons(x''''''''', l'''''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Narrowing Transformation

Dependency Pairs:

MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l2)
MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l1)
MATCH₄(l₅, Cons(a, l')) -> MATCH₅(a, l', l₅, part(a, l'))
QUICK(l₅) -> MATCH₄(l₅, l₅)

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₄(l₅, Cons(a, l')) -> MATCH₅(a, l', l₅, part(a, l'))

one new Dependency Pair is created:

MATCH₄(l₅, Cons(a', l'')) -> MATCH₅(a', l'', l₅, match₁(a', l'', l''))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Narrowing Transformation

Dependency Pairs:

MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l1)
MATCH₄(l₅, Cons(a', l'')) -> MATCH₅(a', l'', l₅, match₁(a', l'', l''))
QUICK(l₅) -> MATCH₄(l₅, l₅)
MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l2)

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₄(l₅, Cons(a', l'')) -> MATCH₅(a', l'', l₅, match₁(a', l'', l''))

two new Dependency Pairs are created:

MATCH₄(l₅, Cons(a'', Nil)) -> MATCH₅(a'', Nil, l₅, Pair(Nil, Nil))
MATCH₄(l₅, Cons(a'', Cons(x', l'''))) -> MATCH₅(a'', Cons(x', l'''), l₅, match₂(x', l''', a'', Cons(x', l'''), part(a'', l''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 15

                 ↳Instantiation Transformation

Dependency Pairs:

MATCH₄(l₅, Cons(a'', Cons(x', l'''))) -> MATCH₅(a'', Cons(x', l'''), l₅, match₂(x', l''', a'', Cons(x', l'''), part(a'', l''')))
MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l2)
MATCH₄(l₅, Cons(a'', Nil)) -> MATCH₅(a'', Nil, l₅, Pair(Nil, Nil))
QUICK(l₅) -> MATCH₄(l₅, l₅)
MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l1)

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l1)

two new Dependency Pairs are created:

MATCH₅(a', Nil, l_5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l1')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 16

                 ↳Instantiation Transformation

Dependency Pairs:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l1')
MATCH₅(a', Nil, l_5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH₄(l₅, Cons(a'', Nil)) -> MATCH₅(a'', Nil, l₅, Pair(Nil, Nil))
QUICK(l₅) -> MATCH₄(l₅, l₅)
MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l2)
MATCH₄(l₅, Cons(a'', Cons(x', l'''))) -> MATCH₅(a'', Cons(x', l'''), l₅, match₂(x', l''', a'', Cons(x', l'''), part(a'', l''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a, l', l₅, Pair(l1, l2)) -> QUICK(l2)

two new Dependency Pairs are created:

MATCH₅(a', Nil, l_5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l2')

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 17

                 ↳Forward Instantiation Transformation

Dependency Pairs:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l2')
MATCH₄(l₅, Cons(a'', Cons(x', l'''))) -> MATCH₅(a'', Cons(x', l'''), l₅, match₂(x', l''', a'', Cons(x', l'''), part(a'', l''')))
MATCH₅(a', Nil, l_5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH₅(a', Nil, l_5'', Pair(Nil, Nil)) -> QUICK(Nil)
MATCH₄(l₅, Cons(a'', Nil)) -> MATCH₅(a'', Nil, l₅, Pair(Nil, Nil))
QUICK(l₅) -> MATCH₄(l₅, l₅)
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l1')

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

QUICK(l₅) -> MATCH₄(l₅, l₅)

two new Dependency Pairs are created:

QUICK(Cons(a'''', Nil)) -> MATCH₄(Cons(a'''', Nil), Cons(a'''', Nil))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 18

                 ↳Forward Instantiation Transformation

Dependency Pairs:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l1')
MATCH₄(l₅, Cons(a'', Cons(x', l'''))) -> MATCH₅(a'', Cons(x', l'''), l₅, match₂(x', l''', a'', Cons(x', l'''), part(a'', l''')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l2')

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l1')

one new Dependency Pair is created:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 19

                 ↳Forward Instantiation Transformation

Dependency Pairs:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l2')
MATCH₄(l₅, Cons(a'', Cons(x', l'''))) -> MATCH₅(a'', Cons(x', l'''), l₅, match₂(x', l''', a'', Cons(x', l'''), part(a'', l''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', l2')) -> QUICK(l2')

one new Dependency Pair is created:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 20

                 ↳Narrowing Transformation

Dependency Pairs:

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₄(l₅, Cons(a'', Cons(x', l'''))) -> MATCH₅(a'', Cons(x', l'''), l₅, match₂(x', l''', a'', Cons(x', l'''), part(a'', l''')))

one new Dependency Pair is created:

MATCH₄(l₅, Cons(a''', Cons(x', l''''))) -> MATCH₅(a''', Cons(x', l''''), l₅, match₂(x', l'''', a''', Cons(x', l''''), match₁(a''', l'''', l'''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 21

                 ↳Narrowing Transformation

Dependency Pairs:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH₄(l₅, Cons(a''', Cons(x', l''''))) -> MATCH₅(a''', Cons(x', l''''), l₅, match₂(x', l'''', a''', Cons(x', l''''), match₁(a''', l'''', l'''')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₄(l₅, Cons(a''', Cons(x', l''''))) -> MATCH₅(a''', Cons(x', l''''), l₅, match₂(x', l'''', a''', Cons(x', l''''), match₁(a''', l'''', l'''')))

two new Dependency Pairs are created:

MATCH₄(l₅, Cons(a'''', Cons(x', Nil))) -> MATCH₅(a'''', Cons(x', Nil), l₅, match₂(x', Nil, a'''', Cons(x', Nil), Pair(Nil, Nil)))
MATCH₄(l₅, Cons(a'''', Cons(x', Cons(x'', l'')))) -> MATCH₅(a'''', Cons(x', Cons(x'', l'')), l₅, match₂(x', Cons(x'', l''), a'''', Cons(x', Cons(x'', l'')), match₂(x'', l'', a'''', Cons(x'', l''), part(a'''', l''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 22

                 ↳Narrowing Transformation

Dependency Pairs:

MATCH₄(l₅, Cons(a'''', Cons(x', Cons(x'', l'')))) -> MATCH₅(a'''', Cons(x', Cons(x'', l'')), l₅, match₂(x', Cons(x'', l''), a'''', Cons(x', Cons(x'', l'')), match₂(x'', l'', a'''', Cons(x'', l''), part(a'''', l''))))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH₄(l₅, Cons(a'''', Cons(x', Nil))) -> MATCH₅(a'''', Cons(x', Nil), l₅, match₂(x', Nil, a'''', Cons(x', Nil), Pair(Nil, Nil)))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₄(l₅, Cons(a'''', Cons(x', Nil))) -> MATCH₅(a'''', Cons(x', Nil), l₅, match₂(x', Nil, a'''', Cons(x', Nil), Pair(Nil, Nil)))

one new Dependency Pair is created:

MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 23

                 ↳Narrowing Transformation

Dependency Pairs:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH₄(l₅, Cons(a'''', Cons(x', Cons(x'', l'')))) -> MATCH₅(a'''', Cons(x', Cons(x'', l'')), l₅, match₂(x', Cons(x'', l''), a'''', Cons(x', Cons(x'', l'')), match₂(x'', l'', a'''', Cons(x'', l''), part(a'''', l''))))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₄(l₅, Cons(a'''', Cons(x', Cons(x'', l'')))) -> MATCH₅(a'''', Cons(x', Cons(x'', l'')), l₅, match₂(x', Cons(x'', l''), a'''', Cons(x', Cons(x'', l'')), match₂(x'', l'', a'''', Cons(x'', l''), part(a'''', l''))))

one new Dependency Pair is created:

MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 24

                 ↳Instantiation Transformation

Dependency Pairs:

MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(Cons(a'''''', Cons(x''''', l''''''')), l2')) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

two new Dependency Pairs are created:

MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 25

                 ↳Instantiation Transformation

Dependency Pairs:

MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(Cons(a'''''', Cons(x''''', l''''''')))

two new Dependency Pairs are created:

MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 26

                 ↳Forward Instantiation Transformation

Dependency Pairs:

MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))
MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), Cons(a'''', Cons(x''', l''''')))

two new Dependency Pairs are created:

QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH₄(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH₄(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 27

                 ↳Forward Instantiation Transformation

Dependency Pairs:

MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH₄(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH₄(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a'''''''', Cons(x'''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))

two new Dependency Pairs are created:

MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 28

                 ↳Forward Instantiation Transformation

Dependency Pairs:

MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH₄(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH₄(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(Cons(a'''''''', Cons(x''''''', l'''''''')), l2'')) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))

two new Dependency Pairs are created:

MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 29

                 ↳Forward Instantiation Transformation

Dependency Pairs:

MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))
MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH₄(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH₄(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a'''''''', Cons(x'''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x'''''', l'''''''')))

two new Dependency Pairs are created:

MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 30

                 ↳Forward Instantiation Transformation

Dependency Pairs:

MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))
MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH₄(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))
MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH₄(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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

MATCH₅(a'', Cons(x'''0, Cons(x'''''', l'''''')), l_5''', Pair(l1'', Cons(a'''''''', Cons(x''''''', l'''''''')))) -> QUICK(Cons(a'''''''', Cons(x''''''', l'''''''')))

two new Dependency Pairs are created:

MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(l1'', Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))

The transformation is resulting in one new DP problem:

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

           →DP Problem 14

             ↳Nar

...

               →DP Problem 31

                 ↳Remaining Obligation(s)

The following remains to be proven:
Dependency Pairs:

MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(l1'', Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))
MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(l1'', Cons(a''''''''', Cons(x'''''''', Nil)))) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Cons(x''''''''', l'''''''''))))
MATCH₅(a'', Cons(x'''0, Nil), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₄(l₅, Cons(a''''', Cons(x'', Nil))) -> MATCH₅(a''''', Cons(x'', Nil), l₅, match₃(Nil, Nil, x'', Nil, a''''', Cons(x'', Nil), test(a''''', x'')))
QUICK(Cons(a''''', Cons(x''''', Nil))) -> MATCH₄(Cons(a''''', Cons(x''''', Nil)), Cons(a''''', Cons(x''''', Nil)))
MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(Cons(a''''''''', Cons(x'''''''', Nil)), l2'')) -> QUICK(Cons(a''''''''', Cons(x'''''''', Nil)))
MATCH₄(l₅, Cons(a''''', Cons(x', Cons(x'', l''')))) -> MATCH₅(a''''', Cons(x', Cons(x'', l''')), l₅, match₂(x', Cons(x'', l'''), a''''', Cons(x', Cons(x'', l''')), match₂(x'', l''', a''''', Cons(x'', l'''), match₁(a''''', l''', l'''))))
QUICK(Cons(a''''', Cons(x'''0, Cons(x''''', l'''''')))) -> MATCH₄(Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))), Cons(a''''', Cons(x'''0, Cons(x''''', l''''''))))
MATCH₅(a'', Cons(x'''0, Cons(x'''''''', l'''''')), l_5''', Pair(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))), l2'')) -> QUICK(Cons(a''''''''', Cons(x''''''''', Cons(x'''''''', l'''''''''))))

Rules:

test(x₀, y) -> True
test(x₀, y) -> False
append(l1₂, l2₁) -> match₀(l1₂, l2₁, l1₂)
match₀(l1₂, l2₁, Nil) -> l2₁
match₀(l1₂, l2₁, Cons(x, l)) -> Cons(x, append(l, l2₁))
part(a₄, l₃) -> match₁(a₄, l₃, l₃)
match₁(a₄, l₃, Nil) -> Pair(Nil, Nil)
match₁(a₄, l₃, Cons(x, l')) -> match₂(x, l', a₄, l₃, part(a₄, l'))
match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
match₃(l1, l2, x, l', a₄, l₃, False) -> Pair(Cons(x, l1), l2)
match₃(l1, l2, x, l', a₄, l₃, True) -> Pair(l1, Cons(x, l2))
quick(l₅) -> match₄(l₅, l₅)
match₄(l₅, Nil) -> Nil
match₄(l₅, Cons(a, l')) -> match₅(a, l', l₅, part(a, l'))
match₅(a, l', l₅, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Strategy:

innermost

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