BEST_CASE(Omega(n^3),?)

Solution:
---------

  "0" :: [] -(0)-> "nat"(0, 0, 0)
  "And" :: ["bool_expr"(0, 0, 0) x "bool_expr"(0, 0, 0)] -(0)-> "bool_expr"(0, 0, 0)
  "Cons" :: ["__ANY_TYPE__"(0, 0, 0) x "list"(4, 0, 2)] -(3)-> "list"(2, 0, 1)
  "Cons" :: ["__ANY_TYPE__"(0, 0, 0) x "list"(1, 0, 0)] -(1)-> "list"(1, 0, 0)
  "Cons" :: ["__ANY_TYPE__"(0, 0, 0) x "list"(0, 0, 0)] -(0)-> "list"(0, 0, 0)
  "Cons" :: ["__ANY_TYPE__"(0, 0, 0) x "list"(2, 0, 0)] -(2)-> "list"(2, 0, 0)
  "False" :: [] -(0)-> "bool"(15, 15, 15)
  "False" :: [] -(0)-> "bool"(15, 15, 1)
  "False" :: [] -(0)-> "bool"(15, 15, 6)
  "False" :: [] -(0)-> "bool"(0, 0, 0)
  "False" :: [] -(0)-> "bool"(0, 0, 5)
  "Nil" :: [] -(0)-> "list"(2, 0, 1)
  "Nil" :: [] -(0)-> "list"(1, 0, 0)
  "Nil" :: [] -(0)-> "list"(0, 0, 0)
  "Not" :: ["bool_expr"(0, 0, 0)] -(0)-> "bool_expr"(0, 0, 0)
  "Or" :: ["bool_expr"(0, 0, 0) x "bool_expr"(0, 0, 0)] -(0)-> "bool_expr"(0, 0, 0)
  "Pair" :: ["__ANY_TYPE__"(0, 0, 0) x "__ANY_TYPE__"(0, 0, 0)] -(0)-> "pair"(0, 0, 0)
  "S" :: ["nat"(0, 0, 0)] -(0)-> "nat"(0, 0, 0)
  "True" :: [] -(0)-> "bool"(15, 15, 15)
  "True" :: [] -(0)-> "bool"(15, 15, 1)
  "True" :: [] -(0)-> "bool"(15, 15, 6)
  "True" :: [] -(0)-> "bool"(0, 0, 0)
  "True" :: [] -(0)-> "bool"(0, 0, 5)
  "Var" :: ["nat"(0, 0, 0)] -(0)-> "bool_expr"(0, 0, 0)
  "assoc#2" :: ["nat"(0, 0, 0) x "list"(1, 0, 0)] -(1)-> "bool"(0, 0, 0)
  "aux#2" :: ["list"(0, 0, 0) x "list"(1, 0, 0)] -(1)-> "list"(0, 0, 0)
  "bot[0]#1" :: [] -(0)-> "bool"(0, 0, 0)
  "concat#2" :: ["list"(1, 0, 0) x "list"(0, 0, 0)] -(1)-> "list"(0, 0, 0)
  "eqNat#2" :: ["nat"(0, 0, 0) x "nat"(0, 0, 0)] -(1)-> "bool"(0, 0, 5)
  "eval#2" :: ["list"(1, 0, 0) x "bool_expr"(0, 0, 0)] -(2)-> "bool"(0, 0, 0)
  "ite#3" :: ["bool"(15, 15, 6) x "bool"(0, 0, 0) x "bool"(0, 0, 0)] -(1)-> "bool"(0, 0, 0)
  "land#2" :: ["bool"(15, 15, 15) x "bool"(0, 0, 0)] -(1)-> "bool"(0, 0, 0)
  "lnot#1" :: ["bool"(15, 15, 1)] -(1)-> "bool"(0, 0, 0)
  "lor#2" :: ["bool"(15, 15, 15) x "bool"(0, 0, 0)] -(1)-> "bool"(0, 0, 0)
  "main" :: ["bool_expr"(0, 0, 0) x "list"(0, 0, 0) x "list"(1, 0, 1)] -(1)-> "list"(0, 0, 0)
  "table_make#3" :: ["list"(2, 0, 0) x "list"(2, 0, 1) x "bool_expr"(0, 0, 0)] -(4)-> "list"(0, 0, 0)


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




Base Constructors:
------------------
  "\"0\"_nat" :: [] -(0)-> "nat"(1, 0, 0)
  "\"0\"_nat" :: [] -(0)-> "nat"(0, 1, 0)
  "\"0\"_nat" :: [] -(0)-> "nat"(0, 0, 1)
  "\"And\"_bool_expr" :: ["bool_expr"(0) x "bool_expr"(0)] -(1)-> "bool_expr"(1, 0, 0)
  "\"And\"_bool_expr" :: ["bool_expr"(0) x "bool_expr"(0)] -(1)-> "bool_expr"(0, 1, 0)
  "\"And\"_bool_expr" :: ["bool_expr"(0) x "bool_expr"(0)] -(1)-> "bool_expr"(0, 0, 1)
  "\"Cons\"_list" :: ["__ANY_TYPE__"(0, 0, 0) x "list"(1, 0, 0)] -(1)-> "list"(1, 0, 0)
  "\"Cons\"_list" :: ["__ANY_TYPE__"(0, 0, 0) x "list"(7, 9, 0)] -(1)-> "list"(0, 1, 0)
  "\"Cons\"_list" :: ["__ANY_TYPE__"(0, 0, 0) x "list"(2, 0, 2)] -(1)-> "list"(0, 0, 1)
  "\"False\"_bool" :: [] -(0)-> "bool"(1, 0, 0)
  "\"False\"_bool" :: [] -(0)-> "bool"(0, 1, 0)
  "\"False\"_bool" :: [] -(0)-> "bool"(0, 0, 1)
  "\"Nil\"_list" :: [] -(0)-> "list"(1, 0, 0)
  "\"Nil\"_list" :: [] -(0)-> "list"(0, 1, 0)
  "\"Nil\"_list" :: [] -(0)-> "list"(0, 0, 1)
  "\"Not\"_bool_expr" :: ["bool_expr"(0)] -(1)-> "bool_expr"(1, 0, 0)
  "\"Not\"_bool_expr" :: ["bool_expr"(0)] -(1)-> "bool_expr"(0, 1, 0)
  "\"Not\"_bool_expr" :: ["bool_expr"(0)] -(1)-> "bool_expr"(0, 0, 1)
  "\"Or\"_bool_expr" :: ["bool_expr"(0) x "bool_expr"(0)] -(1)-> "bool_expr"(1, 0, 0)
  "\"Or\"_bool_expr" :: ["bool_expr"(0) x "bool_expr"(0)] -(1)-> "bool_expr"(0, 1, 0)
  "\"Or\"_bool_expr" :: ["bool_expr"(0) x "bool_expr"(0)] -(1)-> "bool_expr"(0, 0, 1)
  "\"Pair\"_pair" :: ["__ANY_TYPE__"(0, 0, 0) x "__ANY_TYPE__"(15, 1, 0)] -(1)-> "pair"(1, 0, 0)
  "\"Pair\"_pair" :: ["__ANY_TYPE__"(0, 0, 0) x "__ANY_TYPE__"(12, 5, 0)] -(1)-> "pair"(0, 1, 0)
  "\"Pair\"_pair" :: ["__ANY_TYPE__"(0, 0, 0) x "__ANY_TYPE__"(0, 1, 4)] -(1)-> "pair"(0, 0, 1)
  "\"S\"_nat" :: ["nat"(1, 1, 1)] -(1)-> "nat"(1, 0, 0)
  "\"S\"_nat" :: ["nat"(0, 15, 1)] -(1)-> "nat"(0, 1, 0)
  "\"S\"_nat" :: ["nat"(0, 0, 8)] -(1)-> "nat"(0, 0, 1)
  "\"True\"_bool" :: [] -(0)-> "bool"(1, 0, 0)
  "\"True\"_bool" :: [] -(0)-> "bool"(0, 1, 0)
  "\"True\"_bool" :: [] -(0)-> "bool"(0, 0, 1)
  "\"Var\"_bool_expr" :: ["nat"(0)] -(1)-> "bool_expr"(1, 0, 0)
  "\"Var\"_bool_expr" :: ["nat"(0)] -(1)-> "bool_expr"(0, 1, 0)
  "\"Var\"_bool_expr" :: ["nat"(0)] -(1)-> "bool_expr"(0, 0, 1)
  "\"bot[0]#1\"_bool" :: [] -(0)-> "bool"(1, 0, 0)
  "\"bot[0]#1\"_bool" :: [] -(0)-> "bool"(0, 1, 0)
  "\"bot[0]#1\"_bool" :: [] -(0)-> "bool"(0, 0, 1)



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

(STRATEGY
 INNERMOST)
(VAR
 "v4" "v6" "v3" "v2" "v1" "v44" "v40" "v8" "v32" "v28" "v48" "v20")
(DATATYPES
   "bool" = < "True", "False", "bot[0]#1" >
   "bool_expr" = µX.< "Var"("nat"), "Not"(X), "And"(X, X), "Or"(X, X) >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >
   "pair" = < "Pair"("__ANY_TYPE__", "__ANY_TYPE__") >)
(SIGNATURES
   "table_make#3" :: ["list" x "list" x "bool_expr"] --> "list"
   "eval#2" :: ["list" x "bool_expr"] --> "bool"
   "concat#2" :: ["list" x "list"] --> "list"
   "aux#2" :: ["list" x "list"] --> "list"
   "assoc#2" :: ["nat" x "list"] --> "bool"
   "lor#2" :: ["bool" x "bool"] --> "bool"
   "land#2" :: ["bool" x "bool"] --> "bool"
   "lnot#1" :: ["bool"] --> "bool"
   "ite#3" :: ["bool" x "bool" x "bool"] --> "bool"
   "eqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["bool_expr" x "list" x "list"] --> "list")
(RULES
 "table_make#3"("v4","Nil"(),"v6") -> "Cons"("Pair"("aux#2"("Nil"(),"v4"),"eval#2"("v4","v6")),"Nil"())
 "table_make#3"("v4","Cons"("v3","v2"),"v1") -> "concat#2"("table_make#3"("Cons"("Pair"("v3","True"()),"v4"),"v2","v1"),"table_make#3"("Cons"("Pair"("v3","False"()),"v4"),"v2","v1"))
 "eval#2"("v4","Var"("v2")) -> "assoc#2"("v2","v4")
 "eval#2"("v4","Not"("v2")) -> "lnot#1"("eval#2"("v4","v2"))
 "eval#2"("v6","And"("v4","v2")) -> "land#2"("eval#2"("v6","v4"),"eval#2"("v6","v2"))
 "eval#2"("v6","Or"("v4","v2")) -> "lor#2"("eval#2"("v6","v4"),"eval#2"("v6","v2"))
 "concat#2"("Nil"(),"v44") -> "v44"
 "concat#2"("Cons"("v6","v4"),"v2") -> "Cons"("v6","concat#2"("v4","v2"))
 "aux#2"("v40","Nil"()) -> "v40"
 "aux#2"("v6","Cons"("v4","v2")) -> "aux#2"("Cons"("v4","v6"),"v2")
 "assoc#2"("v2","Nil"()) -> "bot[0]#1"()
 "assoc#2"("v8","Cons"("Pair"("v6","v4"),"v2")) -> "ite#3"("eqNat#2"("v6","v8"),"v4","assoc#2"("v8","v2"))
 "lor#2"("True"(),"v32") -> "True"()
 "lor#2"("False"(),"v32") -> "v32"
 "land#2"("False"(),"v28") -> "False"()
 "land#2"("True"(),"v28") -> "v28"
 "lnot#1"("True"()) -> "False"()
 "lnot#1"("False"()) -> "True"()
 "ite#3"("True"(),"v40","v48") -> "v40"
 "ite#3"("False"(),"v40","v48") -> "v48"
 "eqNat#2"("0"(),"0"()) -> "True"()
 "eqNat#2"("S"("v20"),"0"()) -> "False"()
 "eqNat#2"("S"("v4"),"S"("v2")) -> "eqNat#2"("v4","v2")
 "eqNat#2"("0"(),"S"("v20")) -> "False"()
 "main"("v3","v2","v1") -> "table_make#3"("v2","v1","v3"))


BEST_CASE(Omega(n^3),?)