WORST_CASE(?,O(n^2)) * Step 1: Desugar WORST_CASE(?,O(n^2)) + Considered Problem: let rec leqNat y x = match y with | 0 -> True | S(y') -> (match x with | S(x') -> leqNat x' y' | 0 -> False) ;; let rec eqNat x y = match y with | 0 -> (match x with | 0 -> True | S(x') -> False) | S(y') -> (match x with | S(x') -> eqNat x' y' | 0 -> False) ;; let rec geqNat x y = match y with | 0 -> True | S(y') -> (match x with | 0 -> False | S(x') -> geqNat x' y') ;; let rec ltNat x y = match y with | 0 -> False | S(y') -> (match x with | 0 -> True | S(x') -> ltNat x' y') ;; let rec gtNat x y = match x with | 0 -> False | S(x') -> (match y with | 0 -> True | S(y') -> gtNat x' y') ;; let ifz n th el = match n with | 0 -> th 0 | S(x) -> el x ;; let ite b th el = match b with | True()-> th | False()-> el ;; let minus n m = let rec minus' m n = match m with | 0 -> 0 | S(x) -> (match n with | 0 -> m | S(y) -> minus' x y) in Pair(minus' n m,m) ;; let rec plus n m = match m with | 0 -> n | S(x) -> S(plus n x) ;; type ('a,'b,'c) triple = Triple of 'a * 'b * 'c ;; let rec div_mod n m = match (minus n m) with | Pair(res,m) -> (match res with | 0 -> Triple (0,n,m) | S(x) -> (match (div_mod res m) with | Triple(a,rest,unusedM) -> Triple(plus S(0) a,rest,m))) ;; let rec mult n m = match n with | 0 -> 0 | S(x) -> S(plus (mult x m) m) ;; type bool = True | False ;; type 'a option = None | Some of 'a ;; type 'a list = Nil | Cons of 'a * 'a list ;; type nat = 0 | S of nat ;; type Unit = Unit ;; type ('a,'b) pair = Pair of 'a * 'b ;; let rec foldr f b xs = match xs with | Nil()-> b | Cons(x,xs) -> f x (foldr f b xs) ;; let product ms ns = foldr (fun m ps -> foldr (fun n xs -> Cons(Pair(m,n),xs)) ps ns) Nil ms ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^2)) + Considered Problem: λms : 'a17 list. λns : 'a17 list. (λfoldr : ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list. (λproduct : 'a17 list -> 'a17 list -> ('a17,'a17) pair list. product ms ns) (λms : 'a17 list. λns : 'a17 list. foldr (λm : 'a17. λps : ('a17,'a17) pair list. foldr (λn : 'a17. λxs : ('a17,'a17) pair list. Cons(Pair(m,n),xs)) ps ns) Nil ms)) (μfoldr : ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list. λf : 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list. λb : ('a17,'a17) pair list. λxs : 'a17 list. case xs of | Nil -> b | Cons -> λx : 'a17. λxs : 'a17 list. f x (foldr f b xs)) : 'a17 list -> 'a17 list -> ('a17 ,'a17) pair list where 0 :: nat Cons :: 'a -> 'a list -> 'a list False :: bool Nil :: 'a list None :: 'a option Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Some :: 'a -> 'a option Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple True :: bool Unit :: Unit + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_3(x0, x1) x3 -> x3 x0 x1 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(x2, x4, x5) x6 -> x2 product_ms_ns_2(x5) x6 x4 5: product_ms_ns(x2, x4) x5 -> product_ms_ns_1(x2, x4, x5) 6: product_ms(x2, x3) x4 -> x2 product_ms_ns(x2, x4) Nil() x3 7: product(x2) x3 -> product_ms(x2, x3) 8: main_2(x0, x1) x2 -> main_3(x0, x1) product(x2) 9: cond_foldr_f_b_xs(Nil(), x2, x3) -> x3 10: cond_foldr_f_b_xs(Cons(x5, x6), x2, x3) -> x2 x5 (foldr() x2 x3 x6) 11: foldr_f_b(x2, x3) x4 -> cond_foldr_f_b_xs(x4, x2, x3) 12: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 13: foldr_1() x2 -> foldr_f(x2) 14: foldr() x0 -> foldr_1() x0 15: main(x0, x1) -> main_2(x0, x1) foldr() where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list foldr_1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_2 :: 'a17 list -> 'a17 list -> (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_3 :: 'a17 list -> 'a17 list -> ('a17 list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list cond_foldr_f_b_xs :: 'a17 list -> ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_3(x0, x1) x3 -> x3 x0 x1 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(x2, x4, x5) x6 -> x2 product_ms_ns_2(x5) x6 x4 5: product_ms_ns(x2, x4) x5 -> product_ms_ns_1(x2, x4, x5) 6: product_ms(x2, x3) x4 -> x2 product_ms_ns(x2, x4) Nil() x3 7: product(x2) x3 -> product_ms(x2, x3) 8: main_2(x0, x2) x5 -> product(x5) x0 x2 9: cond_foldr_f_b_xs(Nil(), x2, x3) -> x3 10: cond_foldr_f_b_xs(Cons(x5, x6), x2, x3) -> x2 x5 (foldr() x2 x3 x6) 11: foldr_f_b(x2, x3) x4 -> cond_foldr_f_b_xs(x4, x2, x3) 12: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 13: foldr_1() x2 -> foldr_f(x2) 14: foldr() x4 -> foldr_f(x4) 15: main(x0, x2) -> main_3(x0, x2) product(foldr()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list foldr_1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_2 :: 'a17 list -> 'a17 list -> (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_3 :: 'a17 list -> 'a17 list -> ('a17 list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list cond_foldr_f_b_xs :: 'a17 list -> ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_3(x0, x1) x3 -> x3 x0 x1 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(x2, x4, x5) x6 -> x2 product_ms_ns_2(x5) x6 x4 5: product_ms_ns(x2, x4) x5 -> product_ms_ns_1(x2, x4, x5) 6: product_ms(x2, x3) x4 -> x2 product_ms_ns(x2, x4) Nil() x3 7: product(x2) x3 -> product_ms(x2, x3) 8: main_2(x6, x5) x4 -> product_ms(x4, x6) x5 9: cond_foldr_f_b_xs(Nil(), x2, x3) -> x3 10: cond_foldr_f_b_xs(Cons(x5, x6), x2, x3) -> x2 x5 (foldr() x2 x3 x6) 11: foldr_f_b(x2, x3) x4 -> cond_foldr_f_b_xs(x4, x2, x3) 12: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 13: foldr_1() x2 -> foldr_f(x2) 14: foldr() x4 -> foldr_f(x4) 15: main(x0, x2) -> product(foldr()) x0 x2 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list foldr_1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_2 :: 'a17 list -> 'a17 list -> (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_3 :: 'a17 list -> 'a17 list -> ('a17 list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list cond_foldr_f_b_xs :: 'a17 list -> ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_3(x0, x1) x3 -> x3 x0 x1 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(x2, x4, x5) x6 -> x2 product_ms_ns_2(x5) x6 x4 5: product_ms_ns(x2, x4) x5 -> product_ms_ns_1(x2, x4, x5) 6: product_ms(x2, x3) x4 -> x2 product_ms_ns(x2, x4) Nil() x3 7: product(x2) x3 -> product_ms(x2, x3) 8: main_2(x6, x8) x4 -> x4 product_ms_ns(x4, x8) Nil() x6 9: cond_foldr_f_b_xs(Nil(), x2, x3) -> x3 10: cond_foldr_f_b_xs(Cons(x5, x6), x2, x3) -> x2 x5 (foldr() x2 x3 x6) 11: foldr_f_b(x2, x3) x4 -> cond_foldr_f_b_xs(x4, x2, x3) 12: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 13: foldr_1() x2 -> foldr_f(x2) 14: foldr() x4 -> foldr_f(x4) 15: main(x6, x5) -> product_ms(foldr(), x6) x5 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list foldr_1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_2 :: 'a17 list -> 'a17 list -> (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_3 :: 'a17 list -> 'a17 list -> ('a17 list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list cond_foldr_f_b_xs :: 'a17 list -> ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_3(x0, x1) x3 -> x3 x0 x1 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(x2, x4, x5) x6 -> x2 product_ms_ns_2(x5) x6 x4 5: product_ms_ns(x2, x4) x5 -> product_ms_ns_1(x2, x4, x5) 6: product_ms(x2, x3) x4 -> x2 product_ms_ns(x2, x4) Nil() x3 7: product(x2) x3 -> product_ms(x2, x3) 8: main_2(x6, x8) x4 -> x4 product_ms_ns(x4, x8) Nil() x6 9: cond_foldr_f_b_xs(Nil(), x2, x3) -> x3 10: cond_foldr_f_b_xs(Cons(x5, x6), x2, x3) -> x2 x5 (foldr() x2 x3 x6) 11: foldr_f_b(x2, x3) x4 -> cond_foldr_f_b_xs(x4, x2, x3) 12: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 13: foldr_1() x2 -> foldr_f(x2) 14: foldr() x4 -> foldr_f(x4) 15: main(x6, x8) -> foldr() product_ms_ns(foldr(), x8) Nil() x6 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list foldr_1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_2 :: 'a17 list -> 'a17 list -> (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_3 :: 'a17 list -> 'a17 list -> ('a17 list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list cond_foldr_f_b_xs :: 'a17 list -> ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_3(x0, x1) x3 -> x3 x0 x1 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(x2, x4, x5) x6 -> x2 product_ms_ns_2(x5) x6 x4 5: product_ms_ns(x2, x4) x5 -> product_ms_ns_1(x2, x4, x5) 6: product_ms(x2, x3) x4 -> x2 product_ms_ns(x2, x4) Nil() x3 7: product(x2) x3 -> product_ms(x2, x3) 8: main_2(x6, x8) x4 -> x4 product_ms_ns(x4, x8) Nil() x6 9: cond_foldr_f_b_xs(Nil(), x2, x3) -> x3 10: cond_foldr_f_b_xs(Cons(x5, x6), x2, x3) -> x2 x5 (foldr() x2 x3 x6) 11: foldr_f_b(x4, x6) Nil() -> x6 12: foldr_f_b(x4, x6) Cons(x10, x12) -> x4 x10 (foldr() x4 x6 x12) 13: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 14: foldr_1() x2 -> foldr_f(x2) 15: foldr() x4 -> foldr_f(x4) 16: main(x6, x8) -> foldr() product_ms_ns(foldr(), x8) Nil() x6 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list foldr_1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_2 :: 'a17 list -> 'a17 list -> (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_3 :: 'a17 list -> 'a17 list -> ('a17 list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list cond_foldr_f_b_xs :: 'a17 list -> ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_3(x0, x1) x3 -> x3 x0 x1 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(x2, x4, x5) x6 -> x2 product_ms_ns_2(x5) x6 x4 5: product_ms_ns(x2, x4) x5 -> product_ms_ns_1(x2, x4, x5) 6: product_ms(x2, x3) x4 -> x2 product_ms_ns(x2, x4) Nil() x3 7: product(x2) x3 -> product_ms(x2, x3) 8: main_2(x6, x8) x4 -> x4 product_ms_ns(x4, x8) Nil() x6 11: foldr_f_b(x4, x6) Nil() -> x6 12: foldr_f_b(x4, x6) Cons(x10, x12) -> x4 x10 (foldr() x4 x6 x12) 13: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 14: foldr_1() x2 -> foldr_f(x2) 15: foldr() x4 -> foldr_f(x4) 16: main(x6, x8) -> foldr() product_ms_ns(foldr(), x8) Nil() x6 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list foldr_1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_2 :: 'a17 list -> 'a17 list -> (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_3 :: 'a17 list -> 'a17 list -> ('a17 list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^2)) + Considered Problem: 1: main_3(x0, x1) x3 -> x3 x0 x1 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(x2, x4, x5) x6 -> x2 product_ms_ns_2(x5) x6 x4 5: product_ms_ns(x2, x4) x5 -> product_ms_ns_1(x2, x4, x5) 6: product_ms(x2, x3) x4 -> x2 product_ms_ns(x2, x4) Nil() x3 7: product(x2) x3 -> product_ms(x2, x3) 8: main_2(x6, x8) x4 -> x4 product_ms_ns(x4, x8) Nil() x6 9: foldr_f_b(x4, x6) Nil() -> x6 10: foldr_f_b(x4, x6) Cons(x10, x12) -> x4 x10 (foldr() x4 x6 x12) 11: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 12: foldr_1() x2 -> foldr_f(x2) 13: foldr() x4 -> foldr_f(x4) 14: main(x6, x8) -> foldr() product_ms_ns(foldr(), x8) Nil() x6 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 list -> ('a17,'a17) pair list foldr_1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_2 :: 'a17 list -> 'a17 list -> (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list main_3 :: 'a17 list -> 'a17 list -> ('a17 list -> 'a17 list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Nil() | Cons(X{*},X{*}) | Nil() | Nil() | Nil() | Pair(X{*},X{*}) | Cons(X{*},X{*}) ,V{x2_4} -> V{x2_5} ,V{x2_5} -> foldr() ,V{x2_11} -> V{x4_13} ,V{x3_11} -> V{x6_4} | V{x6_10} | Nil() ,V{x4_4} -> V{x4_5} ,V{x4_5} -> V{x8_14} ,V{x4_9} -> V{x2_11} ,V{x4_10} -> V{x2_11} ,V{x4_13} -> product_ms_ns_2(V{x5_4}) | V{x4_10} | product_ms_ns(foldr(),V{x8_14}) ,V{x5_2} -> V{x5_3} ,V{x5_3} -> V{x5_4} ,V{x5_4} -> V{x5_5} ,V{x5_5} -> V{x10_10} ,V{x6_4} -> R{10} | R{9} ,V{x6_9} -> V{x3_11} ,V{x6_10} -> V{x3_11} ,V{x6_14} -> X{*} ,V{x7_2} -> V{x7_3} ,V{x7_3} -> V{x10_10} ,V{x8_2} -> R{10} | R{9} ,V{x8_14} -> X{*} ,V{x10_10} -> X{*} ,V{x12_10} -> X{*} ,R{0} -> R{14} | main(X{*},X{*}) ,R{2} -> Cons(Pair(V{x5_2},V{x7_2}),V{x8_2}) ,R{3} -> product_ms_ns_3(V{x5_3},V{x7_3}) ,R{4} -> R{10} | R{9} | @(R{11},V{x4_4}) | @(@(R{13},V{x6_4}),V{x4_4}) | @(@(@(V{x2_4},product_ms_ns_2(V{x5_4})),V{x6_4}),V{x4_4}) ,R{5} -> product_ms_ns_1(V{x2_5},V{x4_5},V{x5_5}) ,R{9} -> V{x6_9} ,R{10} -> R{2} | @(R{3},@(@(@(foldr(),V{x4_10}),V{x6_10}),V{x12_10})) | @(R{3},@(@(R{13},V{x6_10}),V{x12_10})) | @(R{3},@(R{11},V{x12_10})) | @(R{3},R{9}) | @(R{3},R{10}) | R{4} | @(R{5},R{9}) | @(R{5},R{10}) | @(@(V{x4_10},V{x10_10}),R{10}) | @(@(V{x4_10},V{x10_10}),R{9}) | @(R{5},@(R{11},V{x12_10})) | @(@(V{x4_10},V{x10_10}),@(R{11},V{x12_10})) | @(R{5},@(@(R{13},V{x6_10}),V{x12_10})) | @(@(V{x4_10},V{x10_10}),@(@(R{13},V{x6_10}),V{x12_10})) | @(R{5},@(@(@(foldr(),V{x4_10}),V{x6_10}),V{x12_10})) | @(@(V{x4_10},V{x10_10}),@(@(@(foldr(),V{x4_10}),V{x6_10}),V{x12_10})) ,R{11} -> foldr_f_b(V{x2_11},V{x3_11}) ,R{13} -> foldr_f(V{x4_13}) ,R{14} -> R{10} | R{9} | @(R{11},V{x6_14}) | @(@(R{13},Nil()),V{x6_14}) | @(@(@(foldr(),product_ms_ns(foldr(),V{x8_14})),Nil()),V{x6_14})} * Step 11: UncurryATRS WORST_CASE(?,O(n^2)) + Considered Problem: 2: product_ms_ns_3(x5, x7) x8 -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2(x5) x7 -> product_ms_ns_3(x5, x7) 4: product_ms_ns_1(foldr(), x3, x2) x1 -> foldr() product_ms_ns_2(x2) x1 x3 5: product_ms_ns(foldr(), x2) x1 -> product_ms_ns_1(foldr(), x2, x1) 9: foldr_f_b(x4, x6) Nil() -> x6 10: foldr_f_b(product_ms_ns_2(x4), x3) Cons(x2, x1) -> product_ms_ns_2(x4) x2 (foldr() product_ms_ns_2(x4) x3 x1) 11: foldr_f_b(product_ms_ns(foldr(), x4), x3) Cons(x2, x1) -> product_ms_ns(foldr(), x4) x2 (foldr() product_ms_ns(foldr(), x4) x3 x1) 12: foldr_f(x2) x3 -> foldr_f_b(x2, x3) 14: foldr() x4 -> foldr_f(x4) 15: main(x2, x1) -> foldr() product_ms_ns(foldr(), x1) Nil() x2 where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list + Applied Processor: UncurryATRS + Details: none * Step 12: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: product_ms_ns_3#1(x5, x7, x8) -> Cons(Pair(x5, x7), x8) 2: product_ms_ns_2#1(x5, x7) -> product_ms_ns_3(x5, x7) 3: product_ms_ns_2#2(x5, x7, x8) -> product_ms_ns_3#1(x5, x7, x8) 4: product_ms_ns_1#1(foldr(), x3, x2, x1) -> foldr#3(product_ms_ns_2(x2), x1, x3) 5: product_ms_ns#1(foldr(), x2, x1) -> product_ms_ns_1(foldr(), x2, x1) 6: product_ms_ns#2(foldr(), x2, x1, x3) -> product_ms_ns_1#1(foldr(), x2, x1, x3) 7: foldr_f_b#1(x4, x6, Nil()) -> x6 8: foldr_f_b#1(product_ms_ns_2(x4), x3, Cons(x2, x1)) -> product_ms_ns_2#2(x4, x2 , foldr#3(product_ms_ns_2(x4), x3 , x1)) 9: foldr_f_b#1(product_ms_ns(foldr(), x4), x3, Cons(x2, x1)) -> product_ms_ns#2(foldr(), x4 , x2 , foldr#3(product_ms_ns(foldr() , x4) , x3, x1)) 10: foldr_f#1(x2, x3) -> foldr_f_b(x2, x3) 11: foldr_f#2(x2, x3, x4) -> foldr_f_b#1(x2, x3, x4) 12: foldr#1(x4) -> foldr_f(x4) 13: foldr#2(x4, x5) -> foldr_f#1(x4, x5) 14: foldr#3(x4, x5, x6) -> foldr_f#2(x4, x5, x6) 15: main(x2, x1) -> foldr#3(product_ms_ns(foldr(), x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#2 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f#1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f#2 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f_b :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f_b#1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns#1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns#2 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1#1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2#1 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2#2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3#1 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 13: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: product_ms_ns_3#1(x5, x7, x8) -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_2#2(x5, x7, x8) -> product_ms_ns_3#1(x5, x7, x8) 4: product_ms_ns_1#1(foldr(), x3, x2, x1) -> foldr#3(product_ms_ns_2(x2), x1, x3) 6: product_ms_ns#2(foldr(), x2, x1, x3) -> product_ms_ns_1#1(foldr(), x2, x1, x3) 7: foldr_f_b#1(x4, x6, Nil()) -> x6 8: foldr_f_b#1(product_ms_ns_2(x4), x3, Cons(x2, x1)) -> product_ms_ns_2#2(x4, x2 , foldr#3(product_ms_ns_2(x4), x3 , x1)) 9: foldr_f_b#1(product_ms_ns(foldr(), x4), x3, Cons(x2, x1)) -> product_ms_ns#2(foldr(), x4 , x2 , foldr#3(product_ms_ns(foldr() , x4) , x3, x1)) 11: foldr_f#2(x2, x3, x4) -> foldr_f_b#1(x2, x3, x4) 14: foldr#3(x4, x5, x6) -> foldr_f#2(x4, x5, x6) 15: main(x2, x1) -> foldr#3(product_ms_ns(foldr(), x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f#2 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f_b#1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns#2 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1#1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2#2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3#1 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: product_ms_ns_3#1(x5, x7, x8) -> Cons(Pair(x5, x7), x8) 2: product_ms_ns_2#2(x10, x14, x16) -> Cons(Pair(x10, x14), x16) 3: product_ms_ns_1#1(foldr(), x3, x2, x1) -> foldr#3(product_ms_ns_2(x2), x1, x3) 4: product_ms_ns#2(foldr(), x6, x4, x2) -> foldr#3(product_ms_ns_2(x4), x2, x6) 5: foldr_f_b#1(x4, x6, Nil()) -> x6 6: foldr_f_b#1(product_ms_ns_2(x10), x7, Cons(x14, x3)) -> product_ms_ns_3#1(x10, x14 , foldr#3(product_ms_ns_2(x10), x7 , x3)) 7: foldr_f_b#1(product_ms_ns(foldr(), x4), x7, Cons(x2, x3)) -> product_ms_ns_1#1(foldr(), x4 , x2 , foldr#3(product_ms_ns(foldr() , x4) , x7, x3)) 8: foldr_f#2(x8, x12, Nil()) -> x12 9: foldr_f#2(product_ms_ns_2(x8), x6, Cons(x4, x2)) -> product_ms_ns_2#2(x8, x4 , foldr#3(product_ms_ns_2(x8), x6, x2)) 10: foldr_f#2(product_ms_ns(foldr(), x8), x6, Cons(x4, x2)) -> product_ms_ns#2(foldr(), x8 , x4 , foldr#3(product_ms_ns(foldr() , x8), x6 , x2)) 11: foldr#3(x4, x6, x8) -> foldr_f_b#1(x4, x6, x8) 12: main(x2, x1) -> foldr#3(product_ms_ns(foldr(), x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f#2 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f_b#1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns#2 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1#1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2#2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3#1 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 15: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: product_ms_ns_3#1(x5, x7, x8) -> Cons(Pair(x5, x7), x8) 3: product_ms_ns_1#1(foldr(), x3, x2, x1) -> foldr#3(product_ms_ns_2(x2), x1, x3) 5: foldr_f_b#1(x4, x6, Nil()) -> x6 6: foldr_f_b#1(product_ms_ns_2(x10), x7, Cons(x14, x3)) -> product_ms_ns_3#1(x10, x14 , foldr#3(product_ms_ns_2(x10), x7 , x3)) 7: foldr_f_b#1(product_ms_ns(foldr(), x4), x7, Cons(x2, x3)) -> product_ms_ns_1#1(foldr(), x4 , x2 , foldr#3(product_ms_ns(foldr() , x4) , x7, x3)) 11: foldr#3(x4, x6, x8) -> foldr_f_b#1(x4, x6, x8) 12: main(x2, x1) -> foldr#3(product_ms_ns(foldr(), x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f_b#1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1#1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3#1 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: product_ms_ns_3#1(x5, x7, x8) -> Cons(Pair(x5, x7), x8) 2: product_ms_ns_1#1(foldr(), x3, x2, x1) -> foldr#3(product_ms_ns_2(x2), x1, x3) 3: foldr_f_b#1(x4, x6, Nil()) -> x6 4: foldr_f_b#1(product_ms_ns_2(x10), x15, Cons(x14, x7)) -> Cons(Pair(x10, x14) , foldr#3(product_ms_ns_2(x10), x15, x7)) 5: foldr_f_b#1(product_ms_ns(foldr(), x6), x15, Cons(x4, x7)) -> foldr#3(product_ms_ns_2(x4) , foldr#3(product_ms_ns(foldr(), x6) , x15, x7) , x6) 6: foldr#3(x8, x12, Nil()) -> x12 7: foldr#3(product_ms_ns_2(x20), x14, Cons(x28, x6)) -> product_ms_ns_3#1(x20, x28 , foldr#3(product_ms_ns_2(x20), x14 , x6)) 8: foldr#3(product_ms_ns(foldr(), x8), x14, Cons(x4, x6)) -> product_ms_ns_1#1(foldr(), x8 , x4 , foldr#3(product_ms_ns(foldr() , x8) , x14, x6)) 9: main(x2, x1) -> foldr#3(product_ms_ns(foldr(), x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr_f_b#1 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1#1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3#1 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: Inline WORST_CASE(?,O(n^2)) + Considered Problem: 1: product_ms_ns_3#1(x5, x7, x8) -> Cons(Pair(x5, x7), x8) 2: product_ms_ns_1#1(foldr(), x3, x2, x1) -> foldr#3(product_ms_ns_2(x2), x1, x3) 6: foldr#3(x8, x12, Nil()) -> x12 7: foldr#3(product_ms_ns_2(x20), x14, Cons(x28, x6)) -> product_ms_ns_3#1(x20, x28 , foldr#3(product_ms_ns_2(x20), x14 , x6)) 8: foldr#3(product_ms_ns(foldr(), x8), x14, Cons(x4, x6)) -> product_ms_ns_1#1(foldr(), x8 , x4 , foldr#3(product_ms_ns(foldr() , x8) , x14, x6)) 9: main(x2, x1) -> foldr#3(product_ms_ns(foldr(), x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1#1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3#1 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 18: UsableRules WORST_CASE(?,O(n^2)) + Considered Problem: 1: product_ms_ns_3#1(x5, x7, x8) -> Cons(Pair(x5, x7), x8) 2: product_ms_ns_1#1(foldr(), x3, x2, x1) -> foldr#3(product_ms_ns_2(x2), x1, x3) 3: foldr#3(x8, x12, Nil()) -> x12 4: foldr#3(product_ms_ns_2(x10), x29, Cons(x14, x13)) -> Cons(Pair(x10, x14), foldr#3(product_ms_ns_2(x10) , x29, x13)) 5: foldr#3(product_ms_ns(foldr(), x6), x29, Cons(x4, x13)) -> foldr#3(product_ms_ns_2(x4) , foldr#3(product_ms_ns(foldr(), x6), x29 , x13) , x6) 6: main(x2, x1) -> foldr#3(product_ms_ns(foldr(), x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_1#1 :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_3#1 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 19: Compression WORST_CASE(?,O(n^2)) + Considered Problem: 3: foldr#3(x8, x12, Nil()) -> x12 4: foldr#3(product_ms_ns_2(x10), x29, Cons(x14, x13)) -> Cons(Pair(x10, x14), foldr#3(product_ms_ns_2(x10) , x29, x13)) 5: foldr#3(product_ms_ns(foldr(), x6), x29, Cons(x4, x13)) -> foldr#3(product_ms_ns_2(x4) , foldr#3(product_ms_ns(foldr(), x6), x29 , x13) , x6) 6: main(x2, x1) -> foldr#3(product_ms_ns(foldr(), x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: (('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list) -> 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: Compression + Details: none * Step 20: ToTctProblem WORST_CASE(?,O(n^2)) + Considered Problem: 1: foldr#3(x8, x12, Nil()) -> x12 2: foldr#3(product_ms_ns_2(x10), x29, Cons(x14, x13)) -> Cons(Pair(x10, x14), foldr#3(product_ms_ns_2(x10) , x29, x13)) 3: foldr#3(product_ms_ns(x6), x29, Cons(x4, x13)) -> foldr#3(product_ms_ns_2(x4), foldr#3(product_ms_ns(x6) , x29, x13) , x6) 4: main(x2, x1) -> foldr#3(product_ms_ns(x1), Nil(), x2) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair foldr#3 :: ('a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list) -> ('a17,'a17) pair list -> 'a17 list -> ('a17,'a17) pair list main :: 'a17 list -> 'a17 list -> ('a17,'a17) pair list product_ms_ns :: 'a17 list -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list product_ms_ns_2 :: 'a17 -> 'a17 -> ('a17,'a17) pair list -> ('a17,'a17) pair list + Applied Processor: ToTctProblem + Details: none * Step 21: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) -> foldr#3(product_ms_ns_2(x4) ,foldr#3(product_ms_ns(x6),x29,x13) ,x6) foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) -> Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil,Pair} + 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) = {2}, uargs(foldr#3) = {2} Following symbols are considered usable: {foldr#3,main} TcT has computed the following interpretation: p(Cons) = x2 p(Nil) = 1 p(Pair) = 0 p(foldr#3) = x1*x2 + x2 p(main) = 3 + x1^2 p(product_ms_ns) = 1 p(product_ms_ns_2) = 0 Following rules are strictly oriented: main(x2,x1) = 3 + x2^2 > 2 = foldr#3(product_ms_ns(x1),Nil(),x2) Following rules are (at-least) weakly oriented: foldr#3(x8,x12,Nil()) = x12 + x12*x8 >= x12 = x12 foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) = 2*x29 >= 2*x29 = foldr#3(product_ms_ns_2(x4),foldr#3(product_ms_ns(x6),x29,x13),x6) foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) = x29 >= x29 = Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) * Step 22: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) -> foldr#3(product_ms_ns_2(x4) ,foldr#3(product_ms_ns(x6),x29,x13) ,x6) foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) -> Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) - Weak TRS: main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil,Pair} + 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) = {2}, uargs(foldr#3) = {2} Following symbols are considered usable: {foldr#3,main} TcT has computed the following interpretation: p(Cons) = 2 + x2 p(Nil) = 0 p(Pair) = 1 p(foldr#3) = 2*x1*x3 + x2 p(main) = 2*x1*x2 + x1^2 + x2 + 2*x2^2 p(product_ms_ns) = x1 p(product_ms_ns_2) = 1 Following rules are strictly oriented: foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) = 4 + 2*x13 + x29 > 2 + 2*x13 + x29 = Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) Following rules are (at-least) weakly oriented: foldr#3(x8,x12,Nil()) = x12 >= x12 = x12 foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) = 2*x13*x6 + x29 + 4*x6 >= 2*x13*x6 + x29 + 2*x6 = foldr#3(product_ms_ns_2(x4),foldr#3(product_ms_ns(x6),x29,x13),x6) main(x2,x1) = x1 + 2*x1*x2 + 2*x1^2 + x2^2 >= 2*x1*x2 = foldr#3(product_ms_ns(x1),Nil(),x2) * Step 23: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) -> foldr#3(product_ms_ns_2(x4) ,foldr#3(product_ms_ns(x6),x29,x13) ,x6) - Weak TRS: foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) -> Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil,Pair} + 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) = {2}, uargs(foldr#3) = {2} Following symbols are considered usable: {foldr#3,main} TcT has computed the following interpretation: p(Cons) = 1 + x2 p(Nil) = 0 p(Pair) = x2 p(foldr#3) = 2*x1*x3 + x2 + x3 p(main) = 2*x1 + 3*x1*x2 + 2*x2 p(product_ms_ns) = x1 p(product_ms_ns_2) = 0 Following rules are strictly oriented: foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) = 1 + x13 + 2*x13*x6 + x29 + 2*x6 > x13 + 2*x13*x6 + x29 + x6 = foldr#3(product_ms_ns_2(x4),foldr#3(product_ms_ns(x6),x29,x13),x6) Following rules are (at-least) weakly oriented: foldr#3(x8,x12,Nil()) = x12 >= x12 = x12 foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) = 1 + x13 + x29 >= 1 + x13 + x29 = Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) main(x2,x1) = 2*x1 + 3*x1*x2 + 2*x2 >= 2*x1*x2 + x2 = foldr#3(product_ms_ns(x1),Nil(),x2) * Step 24: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict TRS: foldr#3(x8,x12,Nil()) -> x12 - Weak TRS: foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) -> foldr#3(product_ms_ns_2(x4) ,foldr#3(product_ms_ns(x6),x29,x13) ,x6) foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) -> Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil,Pair} + 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) = {2}, uargs(foldr#3) = {2} Following symbols are considered usable: {foldr#3,main} TcT has computed the following interpretation: p(Cons) = 2 + x2 p(Nil) = 1 p(Pair) = 0 p(foldr#3) = x1*x3 + 2*x1^2 + x2 + x3 p(main) = 2 + 2*x1 + x1*x2 + x1^2 + 2*x2 + 2*x2^2 p(product_ms_ns) = x1 p(product_ms_ns_2) = 1 Following rules are strictly oriented: foldr#3(x8,x12,Nil()) = 1 + x12 + x8 + 2*x8^2 > x12 = x12 Following rules are (at-least) weakly oriented: foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) = 2 + x13 + x13*x6 + x29 + 2*x6 + 2*x6^2 >= 2 + x13 + x13*x6 + x29 + 2*x6 + 2*x6^2 = foldr#3(product_ms_ns_2(x4),foldr#3(product_ms_ns(x6),x29,x13),x6) foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) = 6 + 2*x13 + x29 >= 4 + 2*x13 + x29 = Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) main(x2,x1) = 2 + 2*x1 + x1*x2 + 2*x1^2 + 2*x2 + x2^2 >= 1 + x1*x2 + 2*x1^2 + x2 = foldr#3(product_ms_ns(x1),Nil(),x2) * Step 25: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: foldr#3(x8,x12,Nil()) -> x12 foldr#3(product_ms_ns(x6),x29,Cons(x4,x13)) -> foldr#3(product_ms_ns_2(x4) ,foldr#3(product_ms_ns(x6),x29,x13) ,x6) foldr#3(product_ms_ns_2(x10),x29,Cons(x14,x13)) -> Cons(Pair(x10,x14),foldr#3(product_ms_ns_2(x10),x29,x13)) main(x2,x1) -> foldr#3(product_ms_ns(x1),Nil(),x2) - Signature: {foldr#3/3,main/2} / {Cons/2,Nil/0,Pair/2,product_ms_ns/1,product_ms_ns_2/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil,Pair} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^2))