BEST_CASE(Omega(n^1),?)

Solution:
---------

  "0" :: [] -(0)-> "nat"(0)
  "Cons" :: ["__ANY_TYPE__"(0) x "list"(1)] -(1)-> "list"(1)
  "Cons" :: ["__ANY_TYPE__"(0) x "list"(0)] -(0)-> "list"(0)
  "False" :: [] -(0)-> "bool"(0)
  "Nil" :: [] -(0)-> "list"(1)
  "Nil" :: [] -(0)-> "list"(0)
  "S" :: ["nat"(0)] -(0)-> "nat"(0)
  "True" :: [] -(0)-> "bool"(0)
  "cond_insert_ord_x_ys_1" :: ["bool"(0) x "nat"(0) x "nat"(0) x "list"(0)] -(1)-> "list"(0)
  "insert#3" :: ["nat"(0) x "list"(0)] -(1)-> "list"(0)
  "leq#2" :: ["nat"(0) x "nat"(0)] -(1)-> "bool"(0)
  "main" :: ["list"(1)] -(1)-> "list"(0)
  "sort#2" :: ["list"(1)] -(1)-> "list"(0)


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



Used heuristics (no base constructurs)
--------------------------------------


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

(STRATEGY
 INNERMOST)
(VAR
 "v4" "v2" "v3" "v1" "v6" "v8" "v12")
(DATATYPES
   "bool" = < "True", "False" >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >)
(SIGNATURES
   "sort#2" :: ["list"] --> "list"
   "cond_insert_ord_x_ys_1" :: ["bool" x "nat" x "nat" x "list"] --> "list"
   "insert#3" :: ["nat" x "list"] --> "list"
   "leq#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["list"] --> "list")
(RULES
 "sort#2"("Nil"()) -> "Nil"()
 "sort#2"("Cons"("v4","v2")) -> "insert#3"("v4","sort#2"("v2"))
 "cond_insert_ord_x_ys_1"("True"(),"v3","v2","v1") -> "Cons"("v3","Cons"("v2","v1"))
 "cond_insert_ord_x_ys_1"("False"(),"v3","v2","v1") -> "Cons"("v2","insert#3"("v3","v1"))
 "insert#3"("v2","Nil"()) -> "Cons"("v2","Nil"())
 "insert#3"("v6","Cons"("v4","v2")) -> "cond_insert_ord_x_ys_1"("leq#2"("v6","v4"),"v6","v4","v2")
 "leq#2"("0"(),"v8") -> "True"()
 "leq#2"("S"("v12"),"0"()) -> "False"()
 "leq#2"("S"("v4"),"S"("v2")) -> "leq#2"("v4","v2")
 "main"("v1") -> "sort#2"("v1"))


BEST_CASE(Omega(n^1),?)