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

                 ↳Polynomial 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:

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

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(MATCH_0(x₁, x₂, x₃)) = x₃

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

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

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Inst

           →DP Problem 4

             ↳FwdInst

...

               →DP Problem 8

                 ↳Dependency Graph

       →DP Problem 2

         ↳Inst

       →DP Problem 3

         ↳Nar

Dependency Pair:

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

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

                 ↳Polynomial 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:

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

There are no usable rules for innermost w.r.t. to the implicit AFS that need to be oriented.

Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

POL(MATCH_1(x₁, x₂, x₃)) = x₃

resulting in one new DP problem.

     ↳DPs

       →DP Problem 1

         ↳Inst

       →DP Problem 2

         ↳Inst

           →DP Problem 9

             ↳FwdInst

...

               →DP Problem 13

                 ↳Dependency Graph

       →DP Problem 3

         ↳Nar

Dependency Pair:

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

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

                 ↳Polynomial Ordering

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', 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(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

The following dependency pairs can be strictly oriented:

MATCH₅(a', Cons(x''', l'''''), l_5'', Pair(l1', Cons(a'''''', Cons(x''''', l''''''')))) -> QUICK(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''''''')))

Additionally, the following usable rules for innermost w.r.t. to the implicit AFS can be oriented:

match₂(x, l', a₄, l₃, Pair(l1, l2)) -> match₃(l1, l2, x, l', a₄, l₃, test(a₄, x))
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₃(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))

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(Nil) = 0

POL(MATCH_5(x₁, x₂, x₃, x₄)) = 1 + x₄

POL(match_2(x₁, x₂, x₃, x₄, x₅)) = 1 + x₅

POL(False) = 0

POL(MATCH_4(x₁, x₂)) = x₂

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

POL(match_3(x₁, x₂, x₃, x₄, x₅, x₆, x₇)) = 1 + x₁ + x₂

POL(QUICK(x₁)) = x₁

POL(test(x₁, x₂)) = 0

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

POL(True) = 0

POL(part(x₁, x₂)) = x₂

POL(match_1(x₁, x₂, x₃)) = x₃

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

                 ↳Dependency Graph

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''')))
QUICK(Cons(a'''', Cons(x''', l'''''))) -> MATCH₄(Cons(a'''', Cons(x''', l''''')), 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

Using the Dependency Graph resulted in no new DP problems.

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

POL(MATCH_0(x₁, x₂, x₃))	= x₃
POL(Cons(x₁, x₂))	= 1 + x₂
POL(APPEND(x₁, x₂))	= 1 + x₁

POL(PART(x₁, x₂))	= 1 + x₂
POL(Cons(x₁, x₂))	= 1 + x₂
POL(MATCH_1(x₁, x₂, x₃))	= x₃

POL(Nil)	= 0
POL(MATCH_5(x₁, x₂, x₃, x₄))	= 1 + x₄
POL(match_2(x₁, x₂, x₃, x₄, x₅))	= 1 + x₅
POL(False)	= 0
POL(MATCH_4(x₁, x₂))	= x₂
POL(Cons(x₁, x₂))	= 1 + x₂
POL(match_3(x₁, x₂, x₃, x₄, x₅, x₆, x₇))	= 1 + x₁ + x₂
POL(QUICK(x₁))	= x₁
POL(test(x₁, x₂))	= 0
POL(Pair(x₁, x₂))	= x₁ + x₂
POL(True)	= 0
POL(part(x₁, x₂))	= x₂
POL(match_1(x₁, x₂, x₃))	= x₃