WORST_CASE(?,O(n^1))

Solution:
---------

  "0" :: [] -(0)-> "nat"(0)
  "0" :: [] -(0)-> "nat"(4)
  "0" :: [] -(0)-> "nat"(1)
  "Cons" :: ["__ANY_TYPE__"(4) x "list"(4)] -(4)-> "list"(4)
  "ConsTree" :: ["__ANY_TYPE__"(4) x "treelist"(4)] -(4)-> "treelist"(4)
  "False" :: [] -(0)-> "bool"(3)
  "False" :: [] -(0)-> "bool"(6)
  "False" :: [] -(0)-> "bool"(15)
  "Leaf" :: ["list"(4)] -(4)-> "tree"(4)
  "Nil" :: [] -(0)-> "list"(4)
  "NilTree" :: [] -(0)-> "treelist"(4)
  "Node" :: ["list"(4) x "treelist"(4)] -(4)-> "tree"(4)
  "S" :: ["nat"(0)] -(0)-> "nat"(0)
  "S" :: ["nat"(4)] -(4)-> "nat"(4)
  "S" :: ["nat"(1)] -(1)-> "nat"(1)
  "True" :: [] -(0)-> "bool"(3)
  "True" :: [] -(0)-> "bool"(6)
  "True" :: [] -(0)-> "bool"(15)
  "anyEq#2" :: ["nat"(0) x "list"(4)] -(2)-> "bool"(9)
  "bot[0]" :: [] -(0)-> "bool"(7)
  "bot[1]" :: [] -(0)-> "bool"(7)
  "eqNat#2" :: ["nat"(0) x "nat"(4)] -(1)-> "bool"(15)
  "ite#3" :: ["bool"(6) x "bool"(9)] -(2)-> "bool"(9)
  "ite2#3" :: ["bool"(3) x "bool"(1) x "bool"(1)] -(3)-> "bool"(1)
  "leqNat#2" :: ["nat"(0) x "nat"(1)] -(2)-> "bool"(14)
  "lookup#2" :: ["nat"(0) x "tree"(4)] -(0)-> "bool"(1)
  "main" :: ["nat"(6) x "tree"(10)] -(8)-> "bool"(0)


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




Base Constructors:
------------------
  "\"0\"_nat" :: [] -(0)-> "nat"(1)
  "\"Cons\"_list" :: ["__ANY_TYPE__"(1) x "list"(1)] -(1)-> "list"(1)
  "\"ConsTree\"_treelist" :: ["__ANY_TYPE__"(1) x "treelist"(1)] -(1)-> "treelist"(1)
  "\"False\"_bool" :: [] -(0)-> "bool"(1)
  "\"Leaf\"_tree" :: ["list"(1)] -(1)-> "tree"(1)
  "\"Nil\"_list" :: [] -(0)-> "list"(1)
  "\"NilTree\"_treelist" :: [] -(0)-> "treelist"(1)
  "\"Node\"_tree" :: ["list"(1) x "treelist"(1)] -(1)-> "tree"(1)
  "\"S\"_nat" :: ["nat"(1)] -(1)-> "nat"(1)
  "\"True\"_bool" :: [] -(0)-> "bool"(1)
  "\"bot[0]\"_bool" :: [] -(0)-> "bool"(1)
  "\"bot[1]\"_bool" :: [] -(0)-> "bool"(1)



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

(STRATEGY
 INNERMOST)
(VAR
 "v4" "v2" "v6" "v10" "v8" "v48" "v56" "v20" "v16" "v1")
(DATATYPES
   "bool" = < "bot[0]", "bot[1]", "False", "True" >
   "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) >
   "nat" = µX.< "0", "S"(X) >
   "tree" = < "Leaf"("list"), "Node"("list", "treelist") >
   "treelist" = µX.< "ConsTree"("__ANY_TYPE__", X), "NilTree" >)
(SIGNATURES
   "lookup#2" :: ["nat" x "tree"] --> "bool"
   "anyEq#2" :: ["nat" x "list"] --> "bool"
   "ite2#3" :: ["bool" x "bool" x "bool"] --> "bool"
   "ite#3" :: ["bool" x "bool"] --> "bool"
   "eqNat#2" :: ["nat" x "nat"] --> "bool"
   "leqNat#2" :: ["nat" x "nat"] --> "bool"
   "main" :: ["nat" x "tree"] --> "bool")
(RULES
 "lookup#2"("v4","Leaf"("v2")) -> "anyEq#2"("v4","v2")
 "lookup#2"("v6","Node"("Nil"(),"ConsTree"("v4","v2"))) -> "lookup#2"("v6","v4")
 "lookup#2"("v2","Node"("Nil"(),"NilTree"())) -> "bot[0]"()
 "lookup#2"("v10","Node"("Cons"("v8","v6"),"ConsTree"("v4","v2"))) -> "ite2#3"("leqNat#2"("v10","v8"),"lookup#2"("v10","v4"),"lookup#2"("v10","Node"("v6","v2")))
 "lookup#2"("v6","Node"("Cons"("v4","v2"),"NilTree"())) -> "bot[1]"()
 "anyEq#2"("v2","Nil"()) -> "False"()
 "anyEq#2"("v6","Cons"("v4","v2")) -> "ite#3"("eqNat#2"("v6","v4"),"anyEq#2"("v6","v2"))
 "ite2#3"("True"(),"v48","v56") -> "v48"
 "ite2#3"("False"(),"v48","v56") -> "v56"
 "ite#3"("True"(),"v4") -> "True"()
 "ite#3"("False"(),"v4") -> "v4"
 "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"()
 "leqNat#2"("v8","0"()) -> "True"()
 "leqNat#2"("S"("v4"),"S"("v2")) -> "leqNat#2"("v4","v2")
 "leqNat#2"("0"(),"S"("v16")) -> "False"()
 "main"("v2","v1") -> "lookup#2"("v2","v1"))


WORST_CASE(?,O(n^1))