BEST_CASE(Omega(n^1),?)

Solution:
---------

  "0" :: [] -(0)-> "nat"(0)
  "Cons" :: ["__ANY_TYPE__"(0) x "list"(3)] -(3)-> "list"(3)
  "Cons" :: ["__ANY_TYPE__"(0) x "list"(4)] -(4)-> "list"(4)
  "Cons" :: ["__ANY_TYPE__"(0) x "list"(0)] -(0)-> "list"(0)
  "Cons" :: ["__ANY_TYPE__"(0) x "list"(1)] -(1)-> "list"(1)
  "False" :: [] -(0)-> "bool"(4)
  "False" :: [] -(0)-> "bool"(3)
  "Nil" :: [] -(0)-> "list"(3)
  "Nil" :: [] -(0)-> "list"(4)
  "Nil" :: [] -(0)-> "list"(1)
  "Nil" :: [] -(0)-> "list"(0)
  "Pair" :: ["__ANY_TYPE__"(2) x "__ANY_TYPE__"(0)] -(1)-> "pair"(1)
  "Pair" :: ["__ANY_TYPE__"(0) x "__ANY_TYPE__"(0)] -(0)-> "pair"(0)
  "S" :: ["nat"(0)] -(0)-> "nat"(0)
  "True" :: [] -(0)-> "bool"(4)
  "True" :: [] -(0)-> "bool"(1)
  "append#2" :: ["list"(1) x "list"(0)] -(1)-> "list"(0)
  "cond_partition_f_l_1" :: ["pair"(0) x "bool"(0) x "nat"(0)] -(3)-> "pair"(0)
  "cond_quicksort_gt_xyz_1" :: ["pair"(1) x "nat"(0)] -(2)-> "list"(0)
  "ite_b#2" :: ["bool"(4) x "pair"(0) x "pair"(0)] -(1)-> "pair"(0)
  "leqNat#2" :: ["nat"(0) x "nat"(0)] -(1)-> "bool"(3)
  "main" :: ["list"(3)] -(2)-> "list"(0)
  "main_xs_1" :: ["nat"(0)] -(0)-> "bool"(0)
  "partition#2" :: ["bool"(0) x "list"(4)] -(1)-> "pair"(0)
  "quicksort#2" :: ["list"(3)] -(1)-> "list"(0)


Cost Free Signatures:
---------------------




Base Constructors:
------------------
  "\"0\"_nat" :: [] -(0)-> "nat"(1)
  "\"Cons\"_list" :: ["__ANY_TYPE__"(0) x "list"(1)] -(1)-> "list"(1)
  "\"False\"_bool" :: [] -(0)-> "bool"(1)
  "\"Nil\"_list" :: [] -(0)-> "list"(1)
  "\"Pair\"_pair" :: ["__ANY_TYPE__"(2) x "__ANY_TYPE__"(0)] -(1)-> "pair"(1)
  "\"S\"_nat" :: ["nat"(15)] -(1)-> "nat"(1)
  "\"True\"_bool" :: [] -(0)-> "bool"(1)
  "\"main_xs_1\"_bool" :: ["nat"(0)] -(1)-> "bool"(1)



Parsed Typed Term Rewrite System:
---------------------------------

(STRATEGY
 INNERMOST)
(VAR
 "v3" "v2" "v1" "v4" "v6" "v23" "v19" "v8" "v10" "v12")
(DATATYPES
   "bool" = < "main_xs_1"("nat"), "True", "False" >
   "list" = µX.< "Cons"("__ANY_TYPE__", X), "Nil" >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "cond_quicksort_gt_xyz_1" :: ["pair" x "nat"] --> "list"
   "quicksort#2" :: ["list"] --> "list"
   "cond_partition_f_l_1" :: ["pair" x "bool" x "nat"] --> "pair"
   "partition#2" :: ["bool" x "list"] --> "pair"
   "append#2" :: ["list" x "list"] --> "list"
   "ite_b#2" :: ["bool" x "pair" x "pair"] --> "pair"
   "leqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "cond_quicksort_gt_xyz_1"("Pair"("v3","v2"),"v1") -> "append#2"("quicksort#2"("v3"),"Cons"("v1","quicksort#2"("v2")))
 "quicksort#2"("Nil"()) -> "Nil"()
 "quicksort#2"("Cons"("v4","v6")) -> "cond_quicksort_gt_xyz_1"("partition#2"("main_xs_1"("v4"),"v6"),"v4")
 "cond_partition_f_l_1"("Pair"("v23","v19"),"main_xs_1"("v4"),"v2") -> "ite_b#2"("leqNat#2"("v4","v2"),"Pair"("v23","Cons"("v2","v19")),"Pair"("Cons"("v2","v23"),"v19"))
 "partition#2"("main_xs_1"("v1"),"Nil"()) -> "Pair"("Nil"(),"Nil"())
 "partition#2"("main_xs_1"("v3"),"Cons"("v2","v1")) -> "cond_partition_f_l_1"("partition#2"("main_xs_1"("v3"),"v1"),"main_xs_1"("v3"),"v2")
 "append#2"("Nil"(),"Cons"("v2","v4")) -> "Cons"("v2","v4")
 "append#2"("Cons"("v8","v6"),"Cons"("v2","v4")) -> "Cons"("v8","append#2"("v6","Cons"("v2","v4")))
 "ite_b#2"("True"(),"Pair"("v8","Cons"("v10","v12")),"Pair"("Cons"("v2","v4"),"v6")) -> "Pair"("v8","Cons"("v10","v12"))
 "ite_b#2"("False"(),"Pair"("v8","Cons"("v10","v12")),"Pair"("Cons"("v2","v4"),"v6")) -> "Pair"("Cons"("v2","v4"),"v6")
 "leqNat#2"("0"(),"v8") -> "True"()
 "leqNat#2"("S"("v4"),"S"("v2")) -> "leqNat#2"("v2","v4")
 "leqNat#2"("S"("v12"),"0"()) -> "False"()
 "main"("v1") -> "quicksort#2"("v1"))


BEST_CASE(Omega(n^1),?)