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

Innermost 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
AFS


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

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


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(x1, x2))=  1 + x1 + x2  

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
AFS


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


Strategy:

innermost




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
AFS


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

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

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
AFS


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


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.


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


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


Strategy:

innermost




The following dependency pair can be strictly oriented:

MATCH4(l5, Cons(a, l')) -> MATCH5(a, l', l5, part(a, l'))


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

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


Used ordering: Polynomial ordering with Polynomial interpretation:
  POL(Nil)=  0  
  POL(match_2(x1))=  1 + x1  
  POL(Pair(x1, x2))=  x1 + x2  
  POL(Cons(x1))=  1 + x1  
  POL(match_3(x1, x2))=  1 + x1 + x2  
  POL(QUICK(x1))=  x1  

resulting in one new DP problem.
Used Argument Filtering System:
MATCH5(x1, x2, x3, x4) -> x4
Pair(x1, x2) -> Pair(x1, x2)
QUICK(x1) -> QUICK(x1)
MATCH4(x1, x2) -> x2
Cons(x1, x2) -> Cons(x2)
part(x1, x2) -> x2
match1(x1, x2, x3) -> x3
match2(x1, x2, x3, x4, x5) -> match2(x5)
match3(x1, x2, x3, x4, x5, x6, x7) -> match3(x1, x2)


   R
DPs
       →DP Problem 1
AFS
       →DP Problem 2
AFS
       →DP Problem 3
AFS
           →DP Problem 6
Dependency Graph


Dependency Pairs:

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


Strategy:

innermost




Using the Dependency Graph resulted in no new DP problems.

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