Term Rewriting System R:
[x0, y, l12, l21, x, l, a4, l3, l', l1, l2, l5, a]
test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))

Termination of R to be shown.



   R
Dependency Pair Analysis



R contains the following Dependency Pairs:

APPEND(l12, l21) -> MATCH0(l12, l21, l12)
MATCH0(l12, l21, Cons(x, l)) -> APPEND(l, l21)
PART(a4, l3) -> MATCH1(a4, l3, l3)
MATCH1(a4, l3, Cons(x, l')) -> MATCH2(x, l', a4, l3, part(a4, l'))
MATCH1(a4, l3, Cons(x, l')) -> PART(a4, l')
MATCH2(x, l', a4, l3, Pair(l1, l2)) -> MATCH3(l1, l2, x, l', a4, l3, test(a4, x))
MATCH2(x, l', a4, l3, Pair(l1, l2)) -> TEST(a4, x)
QUICK(l5) -> MATCH4(l5, l5)
MATCH4(l5, Cons(a, l')) -> MATCH5(a, l', l5, part(a, l'))
MATCH4(l5, Cons(a, l')) -> PART(a, l')
MATCH5(a, l', l5, Pair(l1, l2)) -> APPEND(quick(l1), Cons(a, quick(l2)))
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l1)
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)

Furthermore, R contains three SCCs.


   R
DPs
       →DP Problem 1
Argument Filtering and Ordering
       →DP Problem 2
AFS
       →DP Problem 3
Remaining


Dependency Pairs:

MATCH0(l12, l21, Cons(x, l)) -> APPEND(l, l21)
APPEND(l12, l21) -> MATCH0(l12, l21, l12)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))





The following dependency pair can be strictly oriented:

MATCH0(l12, l21, Cons(x, l)) -> APPEND(l, l21)


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:
MATCH0(x1, x2, x3) -> x3
Cons(x1, x2) -> Cons(x1, x2)
APPEND(x1, x2) -> x1


   R
DPs
       →DP Problem 1
AFS
           →DP Problem 4
Dependency Graph
       →DP Problem 2
AFS
       →DP Problem 3
Remaining


Dependency Pair:

APPEND(l12, l21) -> MATCH0(l12, l21, l12)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
Argument Filtering and Ordering
       →DP Problem 3
Remaining


Dependency Pairs:

MATCH1(a4, l3, Cons(x, l')) -> PART(a4, l')
PART(a4, l3) -> MATCH1(a4, l3, l3)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))





The following dependency pair can be strictly oriented:

MATCH1(a4, l3, Cons(x, l')) -> PART(a4, 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:
MATCH1(x1, x2, x3) -> x3
Cons(x1, x2) -> Cons(x1, x2)
PART(x1, x2) -> x2


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
           →DP Problem 5
Dependency Graph
       →DP Problem 3
Remaining


Dependency Pair:

PART(a4, l3) -> MATCH1(a4, l3, l3)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))





Using the Dependency Graph resulted in no new DP problems.


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
Remaining Obligation(s)




The following remains to be proven:
Dependency Pairs:

MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l2)
MATCH5(a, l', l5, Pair(l1, l2)) -> QUICK(l1)
MATCH4(l5, Cons(a, l')) -> MATCH5(a, l', l5, part(a, l'))
QUICK(l5) -> MATCH4(l5, l5)


Rules:


test(x0, y) -> True
test(x0, y) -> False
append(l12, l21) -> match0(l12, l21, l12)
match0(l12, l21, Nil) -> l21
match0(l12, l21, Cons(x, l)) -> Cons(x, append(l, l21))
part(a4, l3) -> match1(a4, l3, l3)
match1(a4, l3, Nil) -> Pair(Nil, Nil)
match1(a4, l3, Cons(x, l')) -> match2(x, l', a4, l3, part(a4, l'))
match2(x, l', a4, l3, Pair(l1, l2)) -> match3(l1, l2, x, l', a4, l3, test(a4, x))
match3(l1, l2, x, l', a4, l3, False) -> Pair(Cons(x, l1), l2)
match3(l1, l2, x, l', a4, l3, True) -> Pair(l1, Cons(x, l2))
quick(l5) -> match4(l5, l5)
match4(l5, Nil) -> Nil
match4(l5, Cons(a, l')) -> match5(a, l', l5, part(a, l'))
match5(a, l', l5, Pair(l1, l2)) -> append(quick(l1), Cons(a, quick(l2)))




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