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

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

The following remains to be proven:

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

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

The following remains to be proven:

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

     ↳DPs

       →DP Problem 1

         ↳Remaining Obligation(s)

       →DP Problem 2

         ↳Remaining Obligation(s)

       →DP Problem 3

         ↳Remaining Obligation(s)

The following remains to be proven:

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)))
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)))
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:07 minutes