BEST_CASE(Omega(n^1),?)

Solution:
---------

  "0" :: [] -(0)-> "nat"(0)
  "Cons" :: ["__ANY_TYPE__"(0) x "list"(0)] -(0)-> "list"(0)
  "Cons" :: ["__ANY_TYPE__"(0) x "list"(1)] -(1)-> "list"(1)
  "Nil" :: [] -(0)-> "list"(0)
  "Nil" :: [] -(0)-> "list"(1)
  "Pair" :: ["__ANY_TYPE__"(0) x "__ANY_TYPE__"(0)] -(0)-> "pair"(0)
  "S" :: ["nat"(0)] -(0)-> "nat"(0)
  "Triple" :: ["__ANY_TYPE__"(0) x "__ANY_TYPE__"(0)] -(0)-> "triple"(0)
  "add_1#3" :: ["list"(0) x "list"(0) x "nat"(0)] -(1)-> "list"(0)
  "add_int#2" :: ["list"(0) x "nat"(0)] -(1)-> "list"(0)
  "append#2" :: ["list"(1) x "list"(0)] -(1)-> "list"(0)
  "bot[0]" :: [] -(0)-> "list"(0)
  "bot[1]" :: [] -(0)-> "list"(0)
  "cond_add_b_c_carry_2" :: ["pair"(0) x "list"(0) x "list"(0)] -(1)-> "list"(0)
  "cond_add_int_b_n_1" :: ["pair"(0) x "list"(0)] -(1)-> "list"(0)
  "cond_div_mod_n_m" :: ["pair"(0) x "nat"(0)] -(1)-> "triple"(0)
  "cond_div_mod_n_m_2" :: ["triple"(0)] -(1)-> "triple"(0)
  "cond_mult_int_b_n_carry_1" :: ["pair"(0) x "nat"(0) x "list"(0)] -(1)-> "list"(0)
  "cond_split_n" :: ["triple"(0)] -(1)-> "pair"(0)
  "div_mod#2" :: ["nat"(0)] -(1)-> "triple"(0)
  "ite#3" :: ["list"(0) x "list"(0)] -(1)-> "list"(0)
  "main" :: ["list"(1) x "list"(0)] -(1)-> "list"(0)
  "minus'#2" :: ["nat"(0) x "nat"(0)] -(1)-> "nat"(0)
  "mult_1#3" :: ["list"(0) x "list"(0) x "list"(0)] -(1)-> "list"(0)
  "mult_3#2" :: ["nat"(0) x "nat"(0)] -(1)-> "nat"(0)
  "mult_int_1#3" :: ["list"(0) x "nat"(0) x "nat"(0)] -(1)-> "list"(0)
  "plus#2" :: ["nat"(0) x "nat"(0)] -(1)-> "nat"(0)
  "split#1" :: ["nat"(0)] -(1)-> "pair"(0)
  "zeros#1" :: ["list"(0)] -(1)-> "list"(0)


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



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


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

(STRATEGY
 INNERMOST)
(VAR
 "v4" "v2" "v59" "v8" "v9" "v36" "v38" "v68" "v6" "v3" "v1" "v5"
 "v65" "v19" "v39" "v20" "v28" "v32")
(DATATYPES
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X), "bot[0]", "bot[1]" >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >
   "triple" = < "Triple"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "mult_1#3" :: ["list" x "list" x "list"] --> "list"
   "zeros#1" :: ["list"] --> "list"
   "append#2" :: ["list" x "list"] --> "list"
   "cond_add_b_c_carry_2" :: ["pair" x "list" x "list"] --> "list"
   "add_1#3" :: ["list" x "list" x "nat"] --> "list"
   "cond_add_int_b_n_1" :: ["pair" x "list"] --> "list"
   "add_int#2" :: ["list" x "nat"] --> "list"
   "cond_mult_int_b_n_carry_1" :: ["pair" x "nat" x "list"] --> "list"
   "mult_int_1#3" :: ["list" x "nat" x "nat"] --> "list"
   "cond_split_n" :: ["triple"] --> "pair"
   "split#1" :: ["nat"] --> "pair"
   "mult_3#2" :: ["nat" x "nat"] --> "nat"
   "cond_div_mod_n_m_2" :: ["triple"] --> "triple"
   "cond_div_mod_n_m" :: ["pair" x "nat"] --> "triple"
   "div_mod#2" :: ["nat"] --> "triple"
   "plus#2" :: ["nat" x "nat"] --> "nat"
   "minus'#2" :: ["nat" x "nat"] --> "nat"
   "ite#3" :: ["list" x "list"] --> "list"
   "main" :: ["list" x "list"] --> "list")
(RULES
 "mult_1#3"("Nil"(),"v4","v2") -> "v2"
 "mult_1#3"("Cons"("v4","v59"),"v8","v9") -> "mult_1#3"("v59","Cons"("0"(),"v8"),"add_1#3"("v9","mult_int_1#3"("v8","v4","0"()),"0"()))
 "zeros#1"("Nil"()) -> "Nil"()
 "zeros#1"("Cons"("v36","v38")) -> "Cons"("0"(),"zeros#1"("v38"))
 "append#2"("Nil"(),"v68") -> "v68"
 "append#2"("Cons"("v6","v4"),"v2") -> "Cons"("v6","append#2"("v4","v2"))
 "cond_add_b_c_carry_2"("Pair"("v4","v3"),"v2","v1") -> "Cons"("v4","add_1#3"("v2","v1","v3"))
 "add_1#3"("Nil"(),"v1","0"()) -> "Nil"()
 "add_1#3"("Nil"(),"v2","S"("v1")) -> "bot[0]"()
 "add_1#3"("Nil"(),"v1","S"("0"())) -> "Nil"()
 "add_1#3"("Cons"("v3","v2"),"Nil"(),"v1") -> "add_int#2"("Cons"("v3","v2"),"v1")
 "add_1#3"("Cons"("v5","v4"),"Cons"("v3","v2"),"v1") -> "cond_add_b_c_carry_2"("split#1"("plus#2"("plus#2"("v5","v3"),"v1")),"v4","v2")
 "cond_add_int_b_n_1"("Pair"("v3","v2"),"v1") -> "Cons"("v3","add_int#2"("v1","v2"))
 "add_int#2"("Nil"(),"0"()) -> "Nil"()
 "add_int#2"("Nil"(),"S"("v65")) -> "bot[1]"()
 "add_int#2"("Nil"(),"S"("0"())) -> "Nil"()
 "add_int#2"("Cons"("v9","v19"),"0"()) -> "ite#3"("Cons"("v9","v19"),"cond_add_int_b_n_1"("split#1"("plus#2"("0"(),"v9")),"v19"))
 "add_int#2"("Cons"("v19","v39"),"S"("v65")) -> "cond_add_int_b_n_1"("split#1"("plus#2"("S"("v65"),"v19")),"v39")
 "add_int#2"("Cons"("v9","v19"),"S"("0"())) -> "ite#3"("Cons"("v9","v19"),"cond_add_int_b_n_1"("split#1"("plus#2"("S"("0"()),"v9")),"v19"))
 "cond_mult_int_b_n_carry_1"("Pair"("v4","v3"),"v2","v1") -> "Cons"("v4","mult_int_1#3"("v1","v2","v3"))
 "mult_int_1#3"("Nil"(),"v19","0"()) -> "Nil"()
 "mult_int_1#3"("Nil"(),"v19","S"("v65")) -> "Cons"("S"("v65"),"Nil"())
 "mult_int_1#3"("Nil"(),"v19","S"("0"())) -> "Nil"()
 "mult_int_1#3"("Cons"("v2","v59"),"v4","v9") -> "cond_mult_int_b_n_carry_1"("split#1"("plus#2"("mult_3#2"("v4","v2"),"v9")),"v4","v59")
 "cond_split_n"("Triple"("v2","v1")) -> "Pair"("v1","v2")
 "split#1"("v1") -> "cond_split_n"("div_mod#2"("v1"))
 "mult_3#2"("0"(),"v2") -> "0"()
 "mult_3#2"("S"("v4"),"v2") -> "S"("plus#2"("mult_3#2"("v4","v2"),"v2"))
 "cond_div_mod_n_m_2"("Triple"("v2","v1")) -> "Triple"("plus#2"("S"("0"()),"v2"),"v1")
 "cond_div_mod_n_m"("Pair"("0"(),"S"("S"("S"("S"("S"("S"("S"("S"("S"("S"("0"()))))))))))),"v1") -> "Triple"("0"(),"v1")
 "cond_div_mod_n_m"("Pair"("S"("v2"),"S"("S"("S"("S"("S"("S"("S"("S"("S"("S"("0"()))))))))))),"v1") -> "cond_div_mod_n_m_2"("div_mod#2"("S"("v2")))
 "div_mod#2"("v4") -> "cond_div_mod_n_m"("Pair"("minus'#2"("v4","S"("S"("S"("S"("S"("S"("S"("S"("S"("S"("0"()))))))))))),"S"("S"("S"("S"("S"("S"("S"("S"("S"("S"("0"()))))))))))),"v4")
 "plus#2"("v20","0"()) -> "v20"
 "plus#2"("v4","S"("v2")) -> "S"("plus#2"("v4","v2"))
 "minus'#2"("0"(),"v28") -> "0"()
 "minus'#2"("S"("v32"),"0"()) -> "S"("v32")
 "minus'#2"("S"("v4"),"S"("v2")) -> "minus'#2"("v4","v2")
 "ite#3"("Cons"("v2","v3"),"v1") -> "Cons"("v2","v3")
 "main"("v2","v1") -> "mult_1#3"("v2","v1","zeros#1"("append#2"("v2","v1"))))


BEST_CASE(Omega(n^1),?)