BEST_CASE(Omega(n^1),?) Solution: --------- "0" :: [] -(0)-> "nat"(0) "Cons" :: ["__ANY_TYPE__"(0) x "list"(0)] -(0)-> "list"(0) "Cons" :: ["__ANY_TYPE__"(0) x "list"(1)] -(1)-> "list"(1) "False" :: [] -(0)-> "bool"(0) "Nil" :: [] -(0)-> "list"(0) "Nil" :: [] -(0)-> "list"(1) "S" :: ["nat"(0)] -(0)-> "nat"(0) "True" :: [] -(0)-> "bool"(0) "cond_lcs_l1_l2" :: ["list"(0)] -(1)-> "nat"(0) "cond_lcstable_l1_l2_1" :: ["list"(0) x "list"(0) x "nat"(0)] -(1)-> "list"(0) "eqNat#2" :: ["nat"(0) x "nat"(0)] -(1)-> "bool"(0) "firstline#1" :: ["list"(1)] -(1)-> "list"(0) "gtNat#2" :: ["nat"(0) x "nat"(0)] -(1)-> "bool"(0) "ite#3" :: ["bool"(0) x "nat"(0) x "nat"(0)] -(1)-> "nat"(0) "lcstable#2" :: ["list"(0) x "list"(1)] -(1)-> "list"(0) "main" :: ["list"(0) x "list"(1)] -(1)-> "nat"(0) "max#2" :: ["nat"(0) x "nat"(0)] -(1)-> "nat"(0) "newline#3" :: ["nat"(0) x "list"(0) x "list"(0)] -(1)-> "list"(0) "newline_y_lastline_l_6#1" :: ["nat"(0) x "nat"(0) x "nat"(0) x "list"(0) x "list"(0)] -(1)-> "list"(0) Cost Free Signatures: --------------------- Used heuristics (no base constructurs) -------------------------------------- Parsed Typed Term Rewrite System: --------------------------------- (STRATEGY INNERMOST) (VAR "v25" "v26" "v28" "v4" "v3" "v2" "v1" "v6" "v5" "v7" "v10" "v8" "v12" "v14" "v40" "v48" "v16" "v20") (DATATYPES "bool" = < "True", "False" > "list" = µX.< "Cons"("__ANY_TYPE__", X), "Nil" > "nat" = µX.< "0", "S"(X) >) (SIGNATURES "cond_lcs_l1_l2" :: ["list"] --> "nat" "cond_lcstable_l1_l2_1" :: ["list" x "list" x "nat"] --> "list" "lcstable#2" :: ["list" x "list"] --> "list" "newline_y_lastline_l_6#1" :: ["nat" x "nat" x "nat" x "list" x "list"] --> "list" "max#2" :: ["nat" x "nat"] --> "nat" "newline#3" :: ["nat" x "list" x "list"] --> "list" "firstline#1" :: ["list"] --> "list" "ite#3" :: ["bool" x "nat" x "nat"] --> "nat" "gtNat#2" :: ["nat" x "nat"] --> "bool" "eqNat#2" :: ["nat" x "nat"] --> "bool" "main" :: ["list" x "list"] --> "nat") (RULES "cond_lcs_l1_l2"("Cons"("Nil"(),"v25")) -> "0"() "cond_lcs_l1_l2"("Cons"("Cons"("v26","v28"),"v25")) -> "v26" "cond_lcstable_l1_l2_1"("Cons"("v4","v3"),"v2","v1") -> "Cons"("newline#3"("v1","v4","v2"),"Cons"("v4","v3")) "lcstable#2"("Nil"(),"v2") -> "Cons"("firstline#1"("v2"),"Nil"()) "lcstable#2"("Cons"("v6","v4"),"v2") -> "cond_lcstable_l1_l2_1"("lcstable#2"("v4","v2"),"v2","v6") "newline_y_lastline_l_6#1"("v3","v2","v1","Nil"(),"Nil"()) -> "Cons"("ite#3"("eqNat#2"("v2","v3"),"S"("0"()),"max#2"("v1","0"())),"Nil"()) "newline_y_lastline_l_6#1"("v5","v4","v3","Nil"(),"Cons"("v2","v1")) -> "Cons"("ite#3"("eqNat#2"("v4","v5"),"S"("0"()),"max#2"("v3","v2")),"Cons"("v2","v1")) "newline_y_lastline_l_6#1"("v5","v4","v3","Cons"("v2","v1"),"Nil"()) -> "Cons"("ite#3"("eqNat#2"("v4","v5"),"S"("v2"),"max#2"("v3","0"())),"Nil"()) "newline_y_lastline_l_6#1"("v7","v6","v5","Cons"("v4","v3"),"Cons"("v2","v1")) -> "Cons"("ite#3"("eqNat#2"("v6","v7"),"S"("v4"),"max#2"("v5","v2")),"Cons"("v2","v1")) "max#2"("v4","v2") -> "ite#3"("gtNat#2"("v4","v2"),"v4","v2") "newline#3"("v4","v2","Nil"()) -> "Nil"() "newline#3"("v6","Nil"(),"Cons"("v4","v2")) -> "Nil"() "newline#3"("v10","Cons"("v8","v6"),"Cons"("v4","v2")) -> "newline_y_lastline_l_6#1"("v10","v4","v8","v6","newline#3"("v10","v6","v2")) "firstline#1"("Nil"()) -> "Nil"() "firstline#1"("Cons"("v12","v14")) -> "Cons"("0"(),"firstline#1"("v14")) "ite#3"("True"(),"v40","v48") -> "v40" "ite#3"("False"(),"v40","v48") -> "v48" "gtNat#2"("0"(),"v16") -> "False"() "gtNat#2"("S"("v20"),"0"()) -> "True"() "gtNat#2"("S"("v4"),"S"("v2")) -> "gtNat#2"("v4","v2") "eqNat#2"("0"(),"0"()) -> "True"() "eqNat#2"("S"("v16"),"0"()) -> "False"() "eqNat#2"("S"("v4"),"S"("v2")) -> "eqNat#2"("v4","v2") "eqNat#2"("0"(),"S"("v16")) -> "False"() "main"("v4","v2") -> "cond_lcs_l1_l2"("lcstable#2"("v4","v2"))) BEST_CASE(Omega(n^1),?)