WORST_CASE(?,O(n^1)) Solution: --------- "0" :: [] -(0)-> "nat"(15) "Cons" :: ["__ANY_TYPE__"(0) x "list"(3)] -(3)-> "list"(3) "Cons" :: ["__ANY_TYPE__"(0) x "list"(0)] -(0)-> "list"(0) "Lam1" :: ["closure"(1) x "closure"(1)] -(0)-> "closure"(1) "Lam2" :: [] -(0)-> "closure"(1) "Lam2" :: [] -(0)-> "closure"(7) "Lam3" :: ["__ANY_TYPE__"(0)] -(1)-> "closure"(1) "Nil" :: [] -(0)-> "list"(3) "Nil" :: [] -(0)-> "list"(15) "Nil" :: [] -(0)-> "list"(7) "S" :: ["nat"(0)] -(0)-> "nat"(15) "S" :: ["nat"(0)] -(0)-> "nat"(11) "apply#2" :: ["closure"(1) x "list"(0)] -(1)-> "list"(0) "main" :: [] -(16)-> "list"(0) "walk#1" :: ["list"(3)] -(2)-> "closure"(1) Cost Free Signatures: --------------------- "Cons" :: ["__ANY_TYPE__"_cf(0) x "list"_cf(0)] -(0)-> "list"_cf(0) "Lam1" :: ["closure"_cf(0) x "closure"_cf(0)] -(0)-> "closure"_cf(0) "Lam2" :: [] -(0)-> "closure"_cf(0) "Lam3" :: ["__ANY_TYPE__"_cf(0)] -(0)-> "closure"_cf(0) "Nil" :: [] -(0)-> "list"_cf(0) "apply#2" :: ["closure"_cf(0) x "list"_cf(0)] -(0)-> "list"_cf(0) "walk#1" :: ["list"_cf(0)] -(0)-> "closure"_cf(0) Base Constructors: ------------------ "\"0\"_nat" :: [] -(0)-> "nat"(1) "\"Cons\"_list" :: ["__ANY_TYPE__"(0) x "list"(1)] -(1)-> "list"(1) "\"Lam1\"_closure" :: ["closure"(1) x "closure"(1)] -(0)-> "closure"(1) "\"Lam2\"_closure" :: [] -(0)-> "closure"(1) "\"Lam3\"_closure" :: ["__ANY_TYPE__"(0)] -(1)-> "closure"(1) "\"Nil\"_list" :: [] -(0)-> "list"(1) "\"S\"_nat" :: ["nat"(0)] -(0)-> "nat"(1) Parsed Typed Term Rewrite System: --------------------------------- (STRATEGY INNERMOST) (VAR "v4" "v3" "v2" "v1") (DATATYPES "closure" = µX.< "Lam2", "Lam1"(X, X), "Lam3"("__ANY_TYPE__") > "list" = µX.< "Nil", "Cons"("__ANY_TYPE__", X) > "nat" = µX.< "S"(X), "0" >) (SIGNATURES "walk#1" :: ["list"] --> "closure" "apply#2" :: ["closure" x "list"] --> "list" "main" :: [] --> "list") (RULES "walk#1"("Nil"()) -> "Lam2"() "walk#1"("Cons"("v4","v3")) -> "Lam1"("walk#1"("v3"),"Lam3"("v4")) "apply#2"("Lam1"("v3","Lam3"("v2")),"v1") -> "apply#2"("v3","Cons"("v2","v1")) "apply#2"("Lam2"(),"Cons"("v1","v2")) -> "Cons"("v1","v2") "main"() -> "apply#2"("walk#1"("Cons"("S"("0"()),"Cons"("S"("S"("0"())),"Cons"("S"("S"("S"("0"()))),"Nil"())))),"Nil"())) WORST_CASE(?,O(n^1))