WORST_CASE(?,O(n^2)) * Step 1: Desugar WORST_CASE(?,O(n^2)) + Considered Problem: type nat = 0 | S of nat ;; type 'a list = Nil | Cons of 'a * 'a list ;; (* map f [] = []; map f (x:xs) = (f x) : (map f xs); append [] ys = ys; append (x:xs) ys = x : (append xs ys); prependAll xs ys = map (append xs) ys; *) let rec map f xs = match xs with | Nil -> Nil | Cons(x,xs') -> Cons(f x, map f xs') ;; let rec append xs ys = match xs with | Nil -> ys | Cons(x,xs') -> Cons(x, append xs' ys) ;; let prependAll xs ys = map (append xs) ys ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^2)) + Considered Problem: λxs : 'a2 list. λys : 'a2 list list. (λmap : ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list. (λappend : 'a2 list -> 'a2 list -> 'a2 list. (λprependAll : 'a2 list -> 'a2 list list -> 'a2 list list. prependAll xs ys) (λxs : 'a2 list. λys : 'a2 list list. map (append xs) ys)) (μappend : 'a2 list -> 'a2 list -> 'a2 list. λxs : 'a2 list. λys : 'a2 list. case xs of | Nil -> ys | Cons -> λx : 'a2. λxs' : 'a2 list. Cons(x,append xs' ys))) (μmap : ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list. λf : 'a2 list -> 'a2 list. λxs : 'a2 list list. case xs of | Nil -> Nil | Cons -> λx : 'a2 list. λxs' : 'a2 list list. Cons(f x,map f xs')) : 'a2 list -> 'a2 list list -> 'a2 list list where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5 3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4) 4: main_3(x0, x1, x2) x3 -> main_4(x0, x1) prependAll(x2, x3) 5: cond_append_xs_ys(Nil(), x4) -> x4 6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4) 7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4) 8: append_1() x3 -> append_xs(x3) 9: append() x0 -> append_1() x0 10: main_2(x0, x1) x2 -> main_3(x0, x1, x2) append() 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x0 -> map_1() x0 16: main(x0, x1) -> main_2(x0, x1) map() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_1 :: 'a2 list -> 'a2 list -> 'a2 list map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main_2 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> 'a2 list list main_3 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list list main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5 3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4) 4: main_3(x0, x2, x5) x7 -> prependAll(x5, x7) x0 x2 5: cond_append_xs_ys(Nil(), x4) -> x4 6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4) 7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4) 8: append_1() x3 -> append_xs(x3) 9: append() x6 -> append_xs(x6) 10: main_2(x0, x2) x4 -> main_4(x0, x2) prependAll(x4, append()) 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x4 -> map_f(x4) 16: main(x0, x2) -> main_3(x0, x2, map()) append() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_1 :: 'a2 list -> 'a2 list -> 'a2 list map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main_2 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> 'a2 list list main_3 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list list main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5 3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4) 4: main_3(x8, x5, x4) x6 -> prependAll_xs(x4, x6, x8) x5 5: cond_append_xs_ys(Nil(), x4) -> x4 6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4) 7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4) 8: append_1() x3 -> append_xs(x3) 9: append() x6 -> append_xs(x6) 10: main_2(x0, x2) x9 -> prependAll(x9, append()) x0 x2 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x4 -> map_f(x4) 16: main(x0, x4) -> prependAll(map(), append()) x0 x4 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_1 :: 'a2 list -> 'a2 list -> 'a2 list map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main_2 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> 'a2 list list main_3 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list list main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5 3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10 5: cond_append_xs_ys(Nil(), x4) -> x4 6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4) 7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4) 8: append_1() x3 -> append_xs(x3) 9: append() x6 -> append_xs(x6) 10: main_2(x8, x5) x4 -> prependAll_xs(x4, append(), x8) x5 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x4 -> map_f(x4) 16: main(x8, x9) -> prependAll_xs(map(), append(), x8) x9 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_1 :: 'a2 list -> 'a2 list -> 'a2 list map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main_2 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> 'a2 list list main_3 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list list main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5 3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10 5: cond_append_xs_ys(Nil(), x4) -> x4 6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4) 7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4) 8: append_1() x3 -> append_xs(x3) 9: append() x6 -> append_xs(x6) 10: main_2(x8, x10) x4 -> x4 (append() x8) x10 11: cond_map_f_xs(Nil(), x2) -> Nil() 12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 13: map_f(x2) x3 -> cond_map_f_xs(x3, x2) 14: map_1() x2 -> map_f(x2) 15: map() x4 -> map_f(x4) 16: main(x8, x10) -> map() (append() x8) x10 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_1 :: 'a2 list -> 'a2 list -> 'a2 list map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main_2 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> 'a2 list list main_3 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list list main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5 3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10 5: cond_append_xs_ys(Nil(), x4) -> x4 6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4) 7: append_xs(Nil()) x8 -> x8 8: append_xs(Cons(x10, x12)) x8 -> Cons(x10, append() x12 x8) 9: append_1() x3 -> append_xs(x3) 10: append() x6 -> append_xs(x6) 11: main_2(x8, x10) x4 -> x4 (append() x8) x10 12: cond_map_f_xs(Nil(), x2) -> Nil() 13: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5) 14: map_f(x4) Nil() -> Nil() 15: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10) 16: map_1() x2 -> map_f(x2) 17: map() x4 -> map_f(x4) 18: main(x8, x10) -> map() (append() x8) x10 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_1 :: 'a2 list -> 'a2 list -> 'a2 list map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main_2 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> 'a2 list list main_3 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list list main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5 3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10 7: append_xs(Nil()) x8 -> x8 8: append_xs(Cons(x10, x12)) x8 -> Cons(x10, append() x12 x8) 9: append_1() x3 -> append_xs(x3) 10: append() x6 -> append_xs(x6) 11: main_2(x8, x10) x4 -> x4 (append() x8) x10 14: map_f(x4) Nil() -> Nil() 15: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10) 16: map_1() x2 -> map_f(x2) 17: map() x4 -> map_f(x4) 18: main(x8, x10) -> map() (append() x8) x10 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_1 :: 'a2 list -> 'a2 list -> 'a2 list map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main_2 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> 'a2 list list main_3 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list list main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_4(x0, x1) x4 -> x4 x0 x1 2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5 3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4) 4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10 5: append_xs(Nil()) x8 -> x8 6: append_xs(Cons(x10, x12)) x8 -> Cons(x10, append() x12 x8) 7: append_1() x3 -> append_xs(x3) 8: append() x6 -> append_xs(x6) 9: main_2(x8, x10) x4 -> x4 (append() x8) x10 10: map_f(x4) Nil() -> Nil() 11: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10) 12: map_1() x2 -> map_f(x2) 13: map() x4 -> map_f(x4) 14: main(x8, x10) -> map() (append() x8) x10 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list -> 'a2 list list -> 'a2 list list append_1 :: 'a2 list -> 'a2 list -> 'a2 list map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main_2 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> 'a2 list list main_3 :: 'a2 list -> 'a2 list list -> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list) -> ('a2 list -> 'a2 list -> 'a2 list) -> 'a2 list list main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | Nil() | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() ,V{x4_10} -> V{x4_13} ,V{x4_11} -> V{x4_13} ,V{x4_13} -> V{x4_11} | R{8} ,V{x6_8} -> V{x12_6} | V{x8_14} ,V{x8_5} -> V{x8_6} | V{x8_11} ,V{x8_6} -> V{x8_6} | V{x8_11} ,V{x8_11} -> X{*} ,V{x8_14} -> X{*} ,V{x10_6} -> X{*} ,V{x10_11} -> X{*} ,V{x10_14} -> X{*} ,V{x12_6} -> X{*} ,R{0} -> R{14} | main(X{*},X{*}) ,R{5} -> V{x8_5} ,R{6} -> Cons(V{x10_6},R{6}) | Cons(V{x10_6},R{5}) | Cons(V{x10_6},@(R{8},V{x8_6})) | Cons(V{x10_6},@(@(append(),V{x12_6}),V{x8_6})) ,R{8} -> append_xs(V{x6_8}) ,R{10} -> Nil() ,R{11} -> Cons(R{6},R{10}) | Cons(R{5},R{10}) | Cons(R{6},R{11}) | Cons(R{5},R{11}) | Cons(@(V{x4_11},V{x8_11}),R{11}) | Cons(@(V{x4_11},V{x8_11}),R{10}) | Cons(R{6},@(R{13},V{x10_11})) | Cons(R{5},@(R{13},V{x10_11})) | Cons(@(V{x4_11},V{x8_11}),@(R{13},V{x10_11})) | Cons(R{6},@(@(map(),V{x4_11}),V{x10_11})) | Cons(R{5},@(@(map(),V{x4_11}),V{x10_11})) | Cons(@(V{x4_11},V{x8_11}),@(@(map(),V{x4_11}),V{x10_11})) ,R{13} -> map_f(V{x4_13}) ,R{14} -> R{11} | R{10} | @(R{13},V{x10_14}) | @(@(map(),R{8}),V{x10_14}) | @(@(map(),@(append(),V{x8_14})),V{x10_14})} * Step 11: UncurryATRS WORST_CASE(?,O(n^2)) + Considered Problem: 5: append_xs(Nil()) x8 -> x8 6: append_xs(Cons(x3, x2)) x1 -> Cons(x3, append() x2 x1) 8: append() x6 -> append_xs(x6) 10: map_f(append_xs(x1)) Nil() -> Nil() 11: map_f(append_xs(x3)) Cons(x2, x1) -> Cons(append_xs(x3) x2, map() append_xs(x3) x1) 13: map() append_xs(x1) -> map_f(append_xs(x1)) 14: main(x2, x1) -> map() (append() x2) x1 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list append_xs :: 'a2 list -> 'a2 list -> 'a2 list append :: 'a2 list -> 'a2 list -> 'a2 list map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list main :: 'a2 list -> 'a2 list list -> 'a2 list list + Applied Processor: UncurryATRS + Details: none * Step 12: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: append_xs#1(Nil(), x8) -> x8 2: append_xs#1(Cons(x3, x2), x1) -> Cons(x3, append#2(x2, x1)) 3: append#1(x6) -> append_xs(x6) 4: append#2(x6, x7) -> append_xs#1(x6, x7) 5: map_f#1(append_xs(x1), Nil()) -> Nil() 6: map_f#1(append_xs(x3), Cons(x2, x1)) -> Cons(append_xs#1(x3, x2), map#2(append_xs(x3), x1)) 7: map#1(append_xs(x1)) -> map_f(append_xs(x1)) 8: map#2(append_xs(x1), x2) -> map_f#1(append_xs(x1), x2) 9: main(x2, x1) -> map#2(append#1(x2), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list append#1 :: 'a2 list -> 'a2 list -> 'a2 list append#2 :: 'a2 list -> 'a2 list -> 'a2 list append_xs :: 'a2 list -> 'a2 list -> 'a2 list append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list main :: 'a2 list -> 'a2 list list -> 'a2 list list map#1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list map_f#1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 13: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: append_xs#1(Nil(), x8) -> x8 2: append_xs#1(Cons(x3, x2), x1) -> Cons(x3, append#2(x2, x1)) 3: append#1(x6) -> append_xs(x6) 4: append#2(x6, x7) -> append_xs#1(x6, x7) 5: map_f#1(append_xs(x1), Nil()) -> Nil() 6: map_f#1(append_xs(x3), Cons(x2, x1)) -> Cons(append_xs#1(x3, x2), map#2(append_xs(x3), x1)) 8: map#2(append_xs(x1), x2) -> map_f#1(append_xs(x1), x2) 9: main(x2, x1) -> map#2(append#1(x2), x1) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list append#1 :: 'a2 list -> 'a2 list -> 'a2 list append#2 :: 'a2 list -> 'a2 list -> 'a2 list append_xs :: 'a2 list -> 'a2 list -> 'a2 list append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list main :: 'a2 list -> 'a2 list list -> 'a2 list list map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list map_f#1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: append_xs#1(Nil(), x8) -> x8 2: append_xs#1(Cons(x7, x12), x14) -> Cons(x7, append_xs#1(x12, x14)) 3: append#1(x6) -> append_xs(x6) 4: append#2(x6, x7) -> append_xs#1(x6, x7) 5: map_f#1(append_xs(x1), Nil()) -> Nil() 6: map_f#1(append_xs(x3), Cons(x2, x1)) -> Cons(append_xs#1(x3, x2), map#2(append_xs(x3), x1)) 7: map#2(append_xs(x2), Nil()) -> Nil() 8: map#2(append_xs(x6), Cons(x4, x2)) -> Cons(append_xs#1(x6, x4), map#2(append_xs(x6), x2)) 9: main(x12, x3) -> map#2(append_xs(x12), x3) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list append#1 :: 'a2 list -> 'a2 list -> 'a2 list append#2 :: 'a2 list -> 'a2 list -> 'a2 list append_xs :: 'a2 list -> 'a2 list -> 'a2 list append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list main :: 'a2 list -> 'a2 list list -> 'a2 list list map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list map_f#1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 15: Compression WORST_CASE(?,O(n^2)) + Considered Problem: 1: append_xs#1(Nil(), x8) -> x8 2: append_xs#1(Cons(x7, x12), x14) -> Cons(x7, append_xs#1(x12, x14)) 7: map#2(append_xs(x2), Nil()) -> Nil() 8: map#2(append_xs(x6), Cons(x4, x2)) -> Cons(append_xs#1(x6, x4), map#2(append_xs(x6), x2)) 9: main(x12, x3) -> map#2(append_xs(x12), x3) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list append_xs :: 'a2 list -> 'a2 list -> 'a2 list append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list main :: 'a2 list -> 'a2 list list -> 'a2 list list map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list + Applied Processor: Compression + Details: none * Step 16: ToTctProblem WORST_CASE(?,O(n^2)) + Considered Problem: 1: append_xs#1(Nil(), x8) -> x8 2: append_xs#1(Cons(x7, x12), x14) -> Cons(x7, append_xs#1(x12, x14)) 3: map#2(append_xs(x2), Nil()) -> Nil() 4: map#2(append_xs(x6), Cons(x4, x2)) -> Cons(append_xs#1(x6, x4), map#2(append_xs(x6), x2)) 5: main(x12, x3) -> map#2(append_xs(x12), x3) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list append_xs :: 'a2 list -> 'a2 list -> 'a2 list append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list main :: 'a2 list -> 'a2 list list -> 'a2 list list map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list + Applied Processor: ToTctProblem + Details: none * Step 17: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14)) append_xs#1(Nil(),x8) -> x8 main(x12,x3) -> map#2(append_xs(x12),x3) map#2(append_xs(x2),Nil()) -> Nil() map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) - Signature: {append_xs#1/2,main/2,map#2/2} / {Cons/2,Nil/0,append_xs/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(0) F (TrsFun "append_xs") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "append_xs#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "main") :: ["A"(0) x "A"(0)] -(1)-> "A"(0) F (TrsFun "map#2") :: ["A"(0) x "A"(0)] -(1)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: map#2(append_xs(x2),Nil()) -> Nil() 2. Weak: append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14)) append_xs#1(Nil(),x8) -> x8 main(x12,x3) -> map#2(append_xs(x12),x3) map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) * Step 18: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14)) append_xs#1(Nil(),x8) -> x8 main(x12,x3) -> map#2(append_xs(x12),x3) map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) - Weak TRS: map#2(append_xs(x2),Nil()) -> Nil() - Signature: {append_xs#1/2,main/2,map#2/2} / {Cons/2,Nil/0,append_xs/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(0) F (TrsFun "append_xs") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "append_xs#1") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "main") :: ["A"(0) x "A"(0)] -(1)-> "A"(0) F (TrsFun "map#2") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: main(x12,x3) -> map#2(append_xs(x12),x3) 2. Weak: append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14)) append_xs#1(Nil(),x8) -> x8 map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) * Step 19: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14)) append_xs#1(Nil(),x8) -> x8 map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) - Weak TRS: main(x12,x3) -> map#2(append_xs(x12),x3) map#2(append_xs(x2),Nil()) -> Nil() - Signature: {append_xs#1/2,main/2,map#2/2} / {Cons/2,Nil/0,append_xs/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + Applied Processor: Ara {minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "Cons") :: ["A"(0) x "A"(0)] -(0)-> "A"(0) F (TrsFun "Cons") :: ["A"(0) x "A"(15)] -(15)-> "A"(15) F (TrsFun "Nil") :: [] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(15) F (TrsFun "Nil") :: [] -(0)-> "A"(7) F (TrsFun "append_xs") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "append_xs") :: ["A"(0)] -(0)-> "A"(4) F (TrsFun "append_xs") :: ["A"(0)] -(0)-> "A"(8) F (TrsFun "append_xs#1") :: ["A"(0) x "A"(0)] -(12)-> "A"(0) F (TrsFun "main") :: ["A"(14) x "A"(15)] -(14)-> "A"(0) F (TrsFun "map#2") :: ["A"(0) x "A"(15)] -(7)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (TrsFun \"Cons\")_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1) "F (TrsFun \"append_xs\")_A" :: ["A"(0)] -(0)-> "A"(1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: append_xs#1(Nil(),x8) -> x8 map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) 2. Weak: append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14)) * Step 20: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14)) - Weak TRS: append_xs#1(Nil(),x8) -> x8 main(x12,x3) -> map#2(append_xs(x12),x3) map#2(append_xs(x2),Nil()) -> Nil() map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) - Signature: {append_xs#1/2,main/2,map#2/2} / {Cons/2,Nil/0,append_xs/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(Cons) = {1,2} Following symbols are considered usable: {append_xs#1,main,map#2} TcT has computed the following interpretation: p(Cons) = 1 + x1 + x2 p(Nil) = 0 p(append_xs) = x1 p(append_xs#1) = 2*x1 + 2*x2 p(main) = 4 + 6*x1 + 5*x1*x2 + 7*x1^2 + 4*x2 p(map#2) = 2 + 4*x1 + 2*x1*x2 + 7*x1^2 + 2*x2 Following rules are strictly oriented: append_xs#1(Cons(x7,x12),x14) = 2 + 2*x12 + 2*x14 + 2*x7 > 1 + 2*x12 + 2*x14 + x7 = Cons(x7,append_xs#1(x12,x14)) Following rules are (at-least) weakly oriented: append_xs#1(Nil(),x8) = 2*x8 >= x8 = x8 main(x12,x3) = 4 + 6*x12 + 5*x12*x3 + 7*x12^2 + 4*x3 >= 2 + 4*x12 + 2*x12*x3 + 7*x12^2 + 2*x3 = map#2(append_xs(x12),x3) map#2(append_xs(x2),Nil()) = 2 + 4*x2 + 7*x2^2 >= 0 = Nil() map#2(append_xs(x6),Cons(x4,x2)) = 4 + 2*x2 + 2*x2*x6 + 2*x4 + 2*x4*x6 + 6*x6 + 7*x6^2 >= 3 + 2*x2 + 2*x2*x6 + 2*x4 + 6*x6 + 7*x6^2 = Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) * Step 21: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14)) append_xs#1(Nil(),x8) -> x8 main(x12,x3) -> map#2(append_xs(x12),x3) map#2(append_xs(x2),Nil()) -> Nil() map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2)) - Signature: {append_xs#1/2,main/2,map#2/2} / {Cons/2,Nil/0,append_xs/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))