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

         ↳Argument Filtering and Ordering

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

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

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

         ↳AFS

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

Strategy:

innermost

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

         ↳AFS

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

The following dependency pair can be strictly oriented:

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

There are no usable rules for innermost w.r.t. to the AFS that need to be oriented.
Used ordering: Polynomial ordering with Polynomial interpretation:

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

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

         ↳AFS

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

Strategy:

innermost

Using the Dependency Graph resulted in no new DP problems.

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳Argument Filtering and Ordering

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

The following dependency pair can be strictly oriented:

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

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

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

Used ordering: Polynomial ordering with Polynomial interpretation:

POL(Nil) = 0

POL(match_2(x₁)) = 1 + x₁

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

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

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

POL(QUICK(x₁)) = x₁

resulting in one new DP problem.
Used Argument Filtering System:

MATCH₅(x₁, x₂, x₃, x₄) -> x₄
Pair(x₁, x₂) -> Pair(x₁, x₂)
QUICK(x₁) -> QUICK(x₁)
MATCH₄(x₁, x₂) -> x₂
Cons(x₁, x₂) -> Cons(x₂)
part(x₁, x₂) -> x₂
match₁(x₁, x₂, x₃) -> x₃
match₂(x₁, x₂, x₃, x₄, x₅) -> match₂(x₅)
match₃(x₁, x₂, x₃, x₄, x₅, x₆, x₇) -> match₃(x₁, x₂)

     ↳DPs

       →DP Problem 1

         ↳AFS

       →DP Problem 2

         ↳AFS

       →DP Problem 3

         ↳AFS

           →DP Problem 6

             ↳Dependency Graph

Dependency Pairs:

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

Using the Dependency Graph resulted in no new DP problems.

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

POL(Nil)	= 0
POL(match_2(x₁))	= 1 + x₁
POL(Pair(x₁, x₂))	= x₁ + x₂
POL(Cons(x₁))	= 1 + x₁
POL(match_3(x₁, x₂))	= 1 + x₁ + x₂
POL(QUICK(x₁))	= x₁