BEST_CASE(Omega(n^1),?) Solution: --------- "0" :: [] -(0)-> "nat"(1) "0" :: [] -(0)-> "nat"(0) "Cons" :: ["__ANY_TYPE__"(0) x "list"(0)] -(0)-> "list"(0) "ConsL" :: ["__ANY_TYPE__"(0) x "llist"(0)] -(0)-> "llist"(0) "Nil" :: [] -(0)-> "list"(0) "S" :: ["nat"(1)] -(1)-> "nat"(1) "S" :: ["nat"(0)] -(0)-> "nat"(0) "bot[0]" :: [] -(0)-> "Unit"(0) "bot[3]" :: [] -(0)-> "Unit"(0) "bot[4]" :: [] -(0)-> "Unit"(0) "cond_take_l_n_xs" :: ["llist"(0) x "nat"(1)] -(1)-> "list"(0) "cond_zipwith_l_f_xs_ys" :: ["llist"(0) x "llist"(0)] -(1)-> "llist"(0) "cond_zipwith_l_f_xs_ys_1" :: ["llist"(0) x "nat"(0) x "llist"(0)] -(1)-> "llist"(0) "fibs" :: [] -(0)-> "llist"(0) "fibs_2" :: [] -(0)-> "llist"(0) "fibs_2#1" :: ["Unit"(0)] -(1)-> "llist"(0) "main" :: ["nat"(1)] -(1)-> "list"(0) "plus#2" :: ["nat"(0) x "nat"(0)] -(1)-> "nat"(0) "zipwith_l#3" :: ["llist"(0) x "llist"(0)] -(1)-> "llist"(0) "zipwith_l_f_xs_ys" :: ["llist"(0) x "llist"(0)] -(0)-> "llist"(0) "zipwith_l_f_xs_ys#1" :: ["llist"(0) x "llist"(0) x "Unit"(0)] -(1)-> "llist"(0) Cost Free Signatures: --------------------- Used heuristics (no base constructurs) -------------------------------------- Parsed Typed Term Rewrite System: --------------------------------- (STRATEGY INNERMOST) (VAR "v3" "v12" "v14" "v1" "v4" "v2" "v5" "v8") (DATATYPES "Unit" = < "bot[0]", "bot[3]", "bot[4]" > "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) > "llist" = µX.< "ConsL"("__ANY_TYPE__", X), "fibs", "fibs_2", "zipwith_l_f_xs_ys"(X, X) > "nat" = µX.< "S"(X), "0" >) (SIGNATURES "fibs_2#1" :: ["Unit"] --> "llist" "cond_take_l_n_xs" :: ["llist" x "nat"] --> "list" "plus#2" :: ["nat" x "nat"] --> "nat" "cond_zipwith_l_f_xs_ys_1" :: ["llist" x "nat" x "llist"] --> "llist" "cond_zipwith_l_f_xs_ys" :: ["llist" x "llist"] --> "llist" "zipwith_l_f_xs_ys#1" :: ["llist" x "llist" x "Unit"] --> "llist" "zipwith_l#3" :: ["llist" x "llist"] --> "llist" "main" :: ["nat"] --> "list") (RULES "fibs_2#1"("v3") -> "ConsL"("S"("0"()),"zipwith_l#3"("fibs"(),"fibs_2"())) "cond_take_l_n_xs"("ConsL"("v12","v14"),"0"()) -> "Nil"() "cond_take_l_n_xs"("ConsL"("0"(),"fibs_2"()),"S"("v1")) -> "Cons"("0"(),"cond_take_l_n_xs"("fibs_2#1"("bot[0]"()),"v1")) "cond_take_l_n_xs"("ConsL"("v4","zipwith_l_f_xs_ys"("v3","v2")),"S"("v1")) -> "Cons"("v4","cond_take_l_n_xs"("zipwith_l_f_xs_ys#1"("v3","v2","bot[0]"()),"v1")) "plus#2"("0"(),"v12") -> "v12" "plus#2"("S"("v4"),"v2") -> "S"("plus#2"("v4","v2")) "cond_zipwith_l_f_xs_ys_1"("ConsL"("v4","v3"),"v2","v1") -> "ConsL"("plus#2"("v2","v4"),"zipwith_l#3"("v1","v3")) "cond_zipwith_l_f_xs_ys"("ConsL"("v4","v3"),"zipwith_l_f_xs_ys"("v2","v1")) -> "cond_zipwith_l_f_xs_ys_1"("zipwith_l_f_xs_ys#1"("v2","v1","bot[3]"()),"v4","v3") "cond_zipwith_l_f_xs_ys"("ConsL"("v2","v1"),"fibs_2"()) -> "cond_zipwith_l_f_xs_ys_1"("fibs_2#1"("bot[3]"()),"v2","v1") "zipwith_l_f_xs_ys#1"("fibs"(),"v5","v3") -> "cond_zipwith_l_f_xs_ys"("ConsL"("0"(),"fibs_2"()),"v5") "zipwith_l_f_xs_ys#1"("fibs_2"(),"v2","v1") -> "cond_zipwith_l_f_xs_ys"("fibs_2#1"("bot[4]"()),"v2") "zipwith_l_f_xs_ys#1"("zipwith_l_f_xs_ys"("v4","v3"),"v2","v1") -> "cond_zipwith_l_f_xs_ys"("zipwith_l_f_xs_ys#1"("v4","v3","bot[4]"()),"v2") "zipwith_l#3"("v8","v4") -> "zipwith_l_f_xs_ys"("v8","v4") "main"("v12") -> "cond_take_l_n_xs"("ConsL"("0"(),"fibs_2"()),"v12")) BEST_CASE(Omega(n^1),?)