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) "Nil" :: [] -(0)-> "list"(1) "Nil" :: [] -(0)-> "list"(0) "S" :: ["nat"(0)] -(0)-> "nat"(0) "main" :: ["list"(1) x "nat"(0)] -(1)-> "list"(0) "map#2" :: ["nat"(0) x "list"(1)] -(1)-> "list"(0) "plus_x" :: ["nat"(0)] -(0)-> "nat"(0) "plus_x#1" :: ["nat"(0) x "nat"(0)] -(1)-> "nat"(0) Cost Free Signatures: --------------------- Used heuristics (no base constructurs) -------------------------------------- Parsed Typed Term Rewrite System: --------------------------------- (STRATEGY INNERMOST) (VAR "v8" "v12" "v14" "v2" "v6" "v4" "v5") (DATATYPES "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) > "nat" = µX.< "0", "S"(X), "plus_x"(X) >) (SIGNATURES "plus_x#1" :: ["nat" x "nat"] --> "nat" "map#2" :: ["nat" x "list"] --> "list" "main" :: ["list" x "nat"] --> "list") (RULES "plus_x#1"("0"(),"v8") -> "v8" "plus_x#1"("S"("v12"),"v14") -> "S"("plus_x#1"("v12","v14")) "map#2"("plus_x"("v2"),"Nil"()) -> "Nil"() "map#2"("plus_x"("v6"),"Cons"("v4","v2")) -> "Cons"("plus_x#1"("v6","v4"),"map#2"("plus_x"("v6"),"v2")) "main"("v5","v12") -> "map#2"("plus_x"("v12"),"v5")) BEST_CASE(Omega(n^1),?)