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)))

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

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Remaining

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)))

The following dependency pair can be strictly oriented:

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

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

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

     ↳DPs

       →DP Problem 1

         ↳AFS

           →DP Problem 4

             ↳Dependency Graph

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Remaining

Dependency Pair:

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)))

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳Argument Filtering and Ordering

       →DP Problem 3

         ↳Remaining

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)))

The following dependency pair can be strictly oriented:

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

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

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

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

           →DP Problem 5

             ↳Dependency Graph

       →DP Problem 3

         ↳Remaining

Dependency Pair:

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)))

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Remaining Obligation(s)

The following remains to be proven:
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)))

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