WORST_CASE(?,O(n^3)) Solution: --------- "0" :: [] -(0)-> "int"(4, 0, 2) "0" :: [] -(0)-> "int"(11, 1, 0) "0" :: [] -(0)-> "int"(12, 1, 0) "0" :: [] -(0)-> "int"(2, 0, 0) "0" :: [] -(0)-> "int"(12, 0, 0) "0" :: [] -(0)-> "int"(8, 0, 0) "0" :: [] -(0)-> "int"(1, 0, 0) "0" :: [] -(0)-> "int"(14, 8, 15) "0" :: [] -(0)-> "int"(15, 8, 8) "0" :: [] -(0)-> "int"(15, 13, 14) "0" :: [] -(0)-> "int"(15, 15, 14) "0" :: [] -(0)-> "int"(15, 14, 15) "0" :: [] -(0)-> "int"(15, 15, 15) "0" :: [] -(0)-> "int"(3, 8, 8) "0" :: [] -(0)-> "int"(8, 6, 12) "Cons" :: ["__ANY_TYPE__"(4, 0, 2) x "list"(2, 0, 0)] -(2)-> "list"(2, 0, 2) "Cons" :: ["__ANY_TYPE__"(11, 4, 0) x "list"(15, 4, 0)] -(11)-> "list"(11, 4, 0) "Cons" :: ["__ANY_TYPE__"(2, 0, 0) x "list"(2, 0, 0)] -(2)-> "list"(2, 0, 0) "Cons" :: ["__ANY_TYPE__"(12, 0, 10) x "list"(2, 0, 0)] -(2)-> "list"(2, 0, 10) "Cons" :: ["__ANY_TYPE__"(10, 0, 8) x "list"(2, 0, 0)] -(2)-> "list"(2, 0, 8) "Cons" :: ["__ANY_TYPE__"(7, 12, 4) x "list"(15, 12, 0)] -(3)-> "list"(3, 12, 4) "M" :: ["int"(12, 1, 0)] -(0)-> "int"(11, 1, 0) "Nil" :: [] -(0)-> "list"(11, 4, 0) "Nil" :: [] -(0)-> "list"(2, 0, 0) "Nil" :: [] -(0)-> "list"(15, 14, 14) "S" :: ["int"(4, 0, 0)] -(4)-> "int"(4, 0, 2) "S" :: ["int"(12, 0, 0)] -(12)-> "int"(12, 1, 0) "S" :: ["int"(11, 0, 0)] -(11)-> "int"(11, 1, 0) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 0, 0) "S" :: ["int"(12, 0, 0)] -(12)-> "int"(12, 0, 0) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 13, 4) "S" :: ["int"(8, 0, 0)] -(8)-> "int"(8, 0, 0) "S" :: ["int"(1, 0, 0)] -(1)-> "int"(1, 0, 0) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 9, 9) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 12, 4) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 1, 3) "S" :: ["int"(4, 0, 0)] -(4)-> "int"(4, 12, 6) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 13, 8) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 0, 1) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 14, 6) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 2, 10) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 0, 14) "S" :: ["int"(2, 0, 0)] -(2)-> "int"(2, 14, 7) "S" :: ["int"(1, 0, 0)] -(1)-> "int"(1, 7, 8) "S" :: ["int"(1, 0, 0)] -(1)-> "int"(1, 1, 6) "cond_scanr_f_z_xs_1" :: ["list"(2, 0, 2) x "int"(11, 1, 0)] -(9)-> "list"(2, 0, 0) "foldl#3" :: ["int"(1, 0, 0) x "list"(2, 0, 0)] -(7)-> "int"(0, 0, 0) "main" :: ["list"(13, 10, 14)] -(15)-> "int"(0, 0, 0) "max#2" :: ["int"(1, 0, 0) x "int"(2, 0, 0)] -(1)-> "int"(1, 0, 0) "minus#2" :: ["int"(2, 0, 0) x "int"(12, 0, 0)] -(10)-> "int"(2, 8, 5) "plus#2" :: ["int"(8, 0, 0) x "int"(2, 13, 4)] -(2)-> "int"(2, 0, 5) "scanr#3" :: ["list"(11, 4, 0)] -(7)-> "list"(2, 0, 0) Cost Free Signatures: --------------------- "0" :: [] -(0)-> "int"_cf(12, 15, 11) "0" :: [] -(0)-> "int"_cf(2, 0, 2) "0" :: [] -(0)-> "int"_cf(4, 0, 0) "0" :: [] -(0)-> "int"_cf(10, 10, 15) "0" :: [] -(0)-> "int"_cf(2, 12, 12) "0" :: [] -(0)-> "int"_cf(14, 14, 15) "0" :: [] -(0)-> "int"_cf(14, 14, 14) "0" :: [] -(0)-> "int"_cf(2, 0, 0) "0" :: [] -(0)-> "int"_cf(8, 8, 8) "0" :: [] -(0)-> "int"_cf(14, 8, 10) "0" :: [] -(0)-> "int"_cf(0, 0, 0) "Cons" :: ["__ANY_TYPE__"_cf(4, 0, 0) x "list"_cf(4, 0, 0)] -(4)-> "list"_cf(4, 0, 0) "Cons" :: ["__ANY_TYPE__"_cf(9, 2, 9) x "list"_cf(2, 2, 0)] -(0)-> "list"_cf(0, 2, 9) "Cons" :: ["__ANY_TYPE__"_cf(2, 0, 2) x "list"_cf(0, 0, 0)] -(0)-> "list"_cf(0, 0, 2) "Cons" :: ["__ANY_TYPE__"_cf(3, 0, 3) x "list"_cf(0, 0, 0)] -(0)-> "list"_cf(0, 0, 3) "Cons" :: ["__ANY_TYPE__"_cf(0, 0, 0) x "list"_cf(0, 0, 0)] -(0)-> "list"_cf(0, 0, 0) "Cons" :: ["__ANY_TYPE__"_cf(4, 0, 4) x "list"_cf(0, 0, 0)] -(0)-> "list"_cf(0, 0, 4) "M" :: ["int"_cf(4, 0, 0)] -(0)-> "int"_cf(4, 0, 0) "Nil" :: [] -(0)-> "list"_cf(4, 0, 0) "Nil" :: [] -(0)-> "list"_cf(15, 15, 7) "Nil" :: [] -(0)-> "list"_cf(0, 0, 0) "S" :: ["int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 0, 2) "S" :: ["int"_cf(4, 0, 0)] -(4)-> "int"_cf(4, 0, 0) "S" :: ["int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 8, 13) "S" :: ["int"_cf(0, 0, 0)] -(0)-> "int"_cf(0, 0, 0) "S" :: ["int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 0, 3) "S" :: ["int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 0, 0) "S" :: ["int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 1, 11) "S" :: ["int"_cf(4, 0, 0)] -(4)-> "int"_cf(4, 0, 4) "S" :: ["int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 7, 11) "S" :: ["int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 7, 14) "S" :: ["int"_cf(4, 0, 0)] -(4)-> "int"_cf(4, 12, 0) "S" :: ["int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 9, 9) "S" :: ["int"_cf(0, 0, 0)] -(0)-> "int"_cf(0, 8, 1) "cond_scanr_f_z_xs_1" :: ["list"_cf(0, 0, 2) x "int"_cf(4, 0, 0)] -(4)-> "list"_cf(0, 0, 2) "foldl#3" :: ["int"_cf(0, 0, 0) x "list"_cf(0, 0, 0)] -(0)-> "int"_cf(0, 0, 0) "max#2" :: ["int"_cf(0, 0, 0) x "int"_cf(0, 0, 0)] -(0)-> "int"_cf(0, 0, 0) "minus#2" :: ["int"_cf(2, 0, 0) x "int"_cf(2, 0, 0)] -(2)-> "int"_cf(2, 0, 3) "minus#2" :: ["int"_cf(0, 0, 0) x "int"_cf(0, 0, 0)] -(2)-> "int"_cf(0, 0, 0) "plus#2" :: ["int"_cf(4, 0, 0) x "int"_cf(2, 0, 0)] -(4)-> "int"_cf(2, 6, 9) "plus#2" :: ["int"_cf(0, 0, 0) x "int"_cf(0, 0, 0)] -(0)-> "int"_cf(0, 0, 0) "scanr#3" :: ["list"_cf(4, 0, 0)] -(0)-> "list"_cf(0, 0, 2) Base Constructors: ------------------ "\"0\"_int" :: [] -(0)-> "int"(1, 0, 0) "\"0\"_int" :: [] -(0)-> "int"(0, 1, 0) "\"0\"_int" :: [] -(0)-> "int"(0, 0, 1) "\"Cons\"_list" :: ["__ANY_TYPE__"(1, 0, 0) x "list"(1, 0, 0)] -(1)-> "list"(1, 0, 0) "\"Cons\"_list" :: ["__ANY_TYPE__"(0, 1, 0) x "list"(1, 1, 0)] -(0)-> "list"(0, 1, 0) "\"Cons\"_list" :: ["__ANY_TYPE__"(1, 0, 1) x "list"(0, 0, 0)] -(0)-> "list"(0, 0, 1) "\"M\"_int" :: ["int"(1, 0, 0)] -(0)-> "int"(1, 0, 0) "\"M\"_int" :: ["int"(1, 1, 0)] -(0)-> "int"(0, 1, 0) "\"M\"_int" :: ["int"(0, 0, 0)] -(0)-> "int"(0, 0, 1) "\"Nil\"_list" :: [] -(0)-> "list"(1, 0, 0) "\"Nil\"_list" :: [] -(0)-> "list"(0, 1, 0) "\"Nil\"_list" :: [] -(0)-> "list"(0, 0, 1) "\"S\"_int" :: ["int"(1, 0, 0)] -(1)-> "int"(1, 0, 0) "\"S\"_int" :: ["int"(0, 0, 0)] -(0)-> "int"(0, 1, 0) "\"S\"_int" :: ["int"(0, 0, 0)] -(0)-> "int"(0, 0, 1) Parsed Typed Term Rewrite System: --------------------------------- (STRATEGY INNERMOST) (VAR "v11" "v2" "v40" "v23" "v8" "v4" "v6" "v16" "v20" "v12" "v1") (DATATYPES "int" = µX.< "0", "S"(X), "M"(X) > "list" = µX.< "Cons"("__ANY_TYPE__", X), "Nil" >) (SIGNATURES "cond_scanr_f_z_xs_1" :: ["list" x "int"] --> "list" "scanr#3" :: ["list"] --> "list" "foldl#3" :: ["int" x "list"] --> "int" "minus#2" :: ["int" x "int"] --> "int" "plus#2" :: ["int" x "int"] --> "int" "max#2" :: ["int" x "int"] --> "int" "main" :: ["list"] --> "int") (RULES "cond_scanr_f_z_xs_1"("Cons"("0"(),"v11"),"0"()) -> "Cons"("0"(),"Cons"("0"(),"v11")) "cond_scanr_f_z_xs_1"("Cons"("S"("v2"),"v11"),"0"()) -> "Cons"("S"("v2"),"Cons"("S"("v2"),"v11")) "cond_scanr_f_z_xs_1"("Cons"("0"(),"v11"),"M"("v2")) -> "Cons"("0"(),"Cons"("0"(),"v11")) "cond_scanr_f_z_xs_1"("Cons"("S"("v40"),"v23"),"M"("0"())) -> "Cons"("S"("v40"),"Cons"("S"("v40"),"v23")) "cond_scanr_f_z_xs_1"("Cons"("S"("v8"),"v23"),"M"("S"("v4"))) -> "Cons"("minus#2"("v8","v4"),"Cons"("S"("v8"),"v23")) "cond_scanr_f_z_xs_1"("Cons"("0"(),"v11"),"S"("v2")) -> "Cons"("S"("v2"),"Cons"("0"(),"v11")) "cond_scanr_f_z_xs_1"("Cons"("S"("v2"),"v11"),"S"("v4")) -> "Cons"("plus#2"("S"("v4"),"S"("v2")),"Cons"("S"("v2"),"v11")) "scanr#3"("Nil"()) -> "Cons"("0"(),"Nil"()) "scanr#3"("Cons"("v4","v2")) -> "cond_scanr_f_z_xs_1"("scanr#3"("v2"),"v4") "foldl#3"("v2","Nil"()) -> "v2" "foldl#3"("v6","Cons"("v4","v2")) -> "foldl#3"("max#2"("v6","v4"),"v2") "minus#2"("0"(),"v16") -> "0"() "minus#2"("S"("v20"),"0"()) -> "S"("v20") "minus#2"("S"("v4"),"S"("v2")) -> "minus#2"("v4","v2") "plus#2"("0"(),"S"("v2")) -> "S"("v2") "plus#2"("S"("v4"),"S"("v2")) -> "S"("plus#2"("v4","S"("v2"))) "max#2"("0"(),"v8") -> "v8" "max#2"("S"("v12"),"0"()) -> "S"("v12") "max#2"("S"("v4"),"S"("v2")) -> "S"("max#2"("v4","v2")) "main"("v1") -> "foldl#3"("0"(),"scanr#3"("v1"))) WORST_CASE(?,O(n^3))