WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + 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 list = Nil | Cons of 'a * 'a list ;; type nat = 0 | S of nat ;; type Unit = Unit ;; type ('a,'b) pair = Pair of 'a * 'b (* * * * * * * * * * * * Resource Aware ML * * * * * * * * * * * * * * * * Use Cases * * * * File: * example/list_map.raml * * Author: * Jan Hoffmann, Shu-Chun Weng (S(S(0))014) * * Description: * Some variations of list map. * *) ;; (* The usual list map function. *) let rec map f l = match l with | Nil()-> Nil | Cons(x,xs) -> let ys = map f xs in Cons(f x,ys) ;; (* The usual list rev_map function. *) let map_rev f l = let rec rmap l acc = match l with | Nil()-> acc | Cons(x,xs) -> let acc' = Cons(f x,acc) in rmap xs acc' in rmap l Nil ;; let main xs = let f x = mult x (mult x x) in let g x = plus x S(S(0)) in let h x = x in map h (map_rev h xs) ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λxs : 'a62 list. (λplus : nat -> nat -> nat. (λmult : nat -> nat -> nat. (λmap : ('a62 -> 'a62) -> 'a62 list -> 'a62 list. (λmap_rev : ('a62 -> 'a62) -> 'a62 list -> 'a62 list. (λmain : 'a62 list -> 'a62 list. main xs) (λxs : 'a62 list. (λf : nat -> nat. (λg : nat -> nat. (λh : 'a62 -> 'a62. map h (map_rev h xs)) (λx : 'a62. x)) (λx : nat. plus x S(S(0)))) (λx : nat. mult x (mult x x)))) (λf : 'a62 -> 'a62. λl : 'a62 list. (λrmap : 'a62 list -> 'a62 list -> 'a62 list. rmap l Nil) (μrmap : 'a62 list -> 'a62 list -> 'a62 list. λl : 'a62 list. λacc : 'a62 list. case l of | Nil -> acc | Cons -> λx : 'a62. λxs : 'a62 list. (λacc' : 'a62 list. rmap xs acc') Cons(f x,acc)))) (μmap : ('a62 -> 'a62) -> 'a62 list -> 'a62 list. λf : 'a62 -> 'a62. λl : 'a62 list. case l of | Nil -> Nil | Cons -> λx : 'a62. λxs : 'a62 list. (λys : 'a62 list. Cons(f x,ys)) (map f xs))) (μmult : nat -> nat -> nat. λn : nat. λm : nat. case n of | 0 -> 0 | S -> λx : nat. S(plus (mult x m) m))) (μplus : nat -> nat -> nat. λn : nat. λm : nat. case m of | 0 -> n | S -> λx : nat. S(plus n x)) : 'a62 list -> 'a62 list where 0 :: nat Cons :: 'a -> 'a list -> 'a list False :: bool Nil :: 'a list Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple True :: bool Unit :: Unit + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x3, x4, x5) x7 -> main_xs_2(x3, x4, x5) h() 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x1, x3, x4, x5) x6 -> main_xs_1(x3, x4, x5) g(x1) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x1, x2, x3, x4) x5 -> main_xs(x1, x3, x4, x5) f(x2) 9: main_4(x0, x1, x2, x3) x4 -> main_5(x0) main_6(x1, x2, x3, x4) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: cond_rmap_l_acc(Nil(), x4, x7) -> x7 13: cond_rmap_l_acc(Cons(x8, x9), x4, x7) -> rmap_l_acc_2(x4, x9) Cons(x4 x8, x7) 14: rmap_l(x4, x6) x7 -> cond_rmap_l_acc(x6, x4, x7) 15: rmap_1(x4) x6 -> rmap_l(x4, x6) 16: rmap(x4) x5 -> rmap_1(x4) x5 17: map_rev_f(x4) x5 -> map_rev_f_l(x5) rmap(x4) 18: map_rev() x4 -> map_rev_f(x4) 19: main_3(x0, x1, x2) x3 -> main_4(x0, x1, x2, x3) map_rev() 20: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 21: cond_map_f_l(Nil(), x3) -> Nil() 22: cond_map_f_l(Cons(x5, x6), x3) -> map_f_l_2(x3, x5) (map() x3 x6) 23: map_f(x3) x4 -> cond_map_f_l(x4, x3) 24: map_1() x3 -> map_f(x3) 25: map() x0 -> map_1() x0 26: main_2(x0, x1) x2 -> main_3(x0, x1, x2) map() 27: cond_mult_n_m(0(), x1, x3) -> 0() 28: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 29: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 30: mult_1(x1) x2 -> mult_n(x1, x2) 31: mult(x1) x2 -> mult_1(x1) x2 32: main_1(x0) x1 -> main_2(x0, x1) mult(x1) 33: cond_plus_n_m(0(), x1) -> x1 34: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 35: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 36: plus_1() x1 -> plus_n(x1) 37: plus() x0 -> plus_1() x0 38: main(x0) -> main_1(x0) plus() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list cond_rmap_l_acc :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list -> 'a62 list cond_map_f_l :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x3, x6, x8, x10) x13 -> main_xs_2(x6, x8, x10) h() 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x2, x5, x6, x8) x10 -> main_xs_1(x6, x8, x10) g(x2) 9: main_4(x0, x3, x5, x7) x9 -> main_6(x3, x5, x7, x9) x0 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: cond_rmap_l_acc(Nil(), x4, x7) -> x7 13: cond_rmap_l_acc(Cons(x17, x18), x8, x15) -> rmap(x8) x18 Cons(x8 x17, x15) 14: rmap_l(x4, x6) x7 -> cond_rmap_l_acc(x6, x4, x7) 15: rmap_1(x4) x6 -> rmap_l(x4, x6) 16: rmap(x8) x12 -> rmap_l(x8, x12) 17: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 18: map_rev() x4 -> map_rev_f(x4) 19: main_3(x0, x2, x4) x6 -> main_5(x0) main_6(x2, x4, x6, map_rev()) 20: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 21: cond_map_f_l(Nil(), x3) -> Nil() 22: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 23: map_f(x3) x4 -> cond_map_f_l(x4, x3) 24: map_1() x3 -> map_f(x3) 25: map() x6 -> map_f(x6) 26: main_2(x0, x2) x4 -> main_4(x0, x2, x4, map()) map_rev() 27: cond_mult_n_m(0(), x1, x3) -> 0() 28: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 29: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 30: mult_1(x1) x2 -> mult_n(x1, x2) 31: mult(x2) x4 -> mult_n(x2, x4) 32: main_1(x0) x2 -> main_3(x0, x2, mult(x2)) map() 33: cond_plus_n_m(0(), x1) -> x1 34: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 35: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 36: plus_1() x1 -> plus_n(x1) 37: plus() x2 -> plus_n(x2) 38: main(x0) -> main_2(x0, plus()) mult(plus()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list cond_rmap_l_acc :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list -> 'a62 list cond_map_f_l :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x7, x6, x8, x10) x27 -> x6 h() (x8 h() x10) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x5, x11, x12, x16) x20 -> x12 h() (x16 h() x20) 9: main_4(x20, x4, x10, x12) x16 -> main_xs_1(x12, x16, x20) g(x4) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: cond_rmap_l_acc(Nil(), x4, x7) -> x7 13: cond_rmap_l_acc(Cons(x17, x18), x8, x15) -> rmap(x8) x18 Cons(x8 x17, x15) 14: rmap_l(x4, x6) x7 -> cond_rmap_l_acc(x6, x4, x7) 15: rmap_1(x4) x6 -> rmap_l(x4, x6) 16: rmap(x8) x12 -> rmap_l(x8, x12) 17: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 18: map_rev() x4 -> map_rev_f(x4) 19: main_3(x0, x5, x9) x13 -> main_6(x5, x9, x13, map_rev()) x0 20: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 21: cond_map_f_l(Nil(), x3) -> Nil() 22: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 23: map_f(x3) x4 -> cond_map_f_l(x4, x3) 24: map_1() x3 -> map_f(x3) 25: map() x6 -> map_f(x6) 26: main_2(x0, x6) x10 -> main_6(x6, x10, map(), map_rev()) x0 27: cond_mult_n_m(0(), x1, x3) -> 0() 28: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 29: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 30: mult_1(x1) x2 -> mult_n(x1, x2) 31: mult(x2) x4 -> mult_n(x2, x4) 32: main_1(x0) x4 -> main_5(x0) main_6(x4, mult(x4), map(), map_rev()) 33: cond_plus_n_m(0(), x1) -> x1 34: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 35: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 36: plus_1() x1 -> plus_n(x1) 37: plus() x2 -> plus_n(x2) 38: main(x0) -> main_4(x0, plus(), mult(plus()), map()) map_rev() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list cond_rmap_l_acc :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list -> 'a62 list cond_map_f_l :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x7, x6, x8, x10) x27 -> x6 h() (x8 h() x10) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x5, x11, x12, x16) x20 -> x12 h() (x16 h() x20) 9: main_4(x20, x9, x21, x12) x16 -> x12 h() (x16 h() x20) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: cond_rmap_l_acc(Nil(), x4, x7) -> x7 13: cond_rmap_l_acc(Cons(x17, x18), x8, x15) -> rmap(x8) x18 Cons(x8 x17, x15) 14: rmap_l(x4, x6) x7 -> cond_rmap_l_acc(x6, x4, x7) 15: rmap_1(x4) x6 -> rmap_l(x4, x6) 16: rmap(x8) x12 -> rmap_l(x8, x12) 17: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 18: map_rev() x4 -> map_rev_f(x4) 19: main_3(x40, x10, x22) x24 -> x24 h() (map_rev() h() x40) 20: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 21: cond_map_f_l(Nil(), x3) -> Nil() 22: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 23: map_f(x3) x4 -> cond_map_f_l(x4, x3) 24: map_1() x3 -> map_f(x3) 25: map() x6 -> map_f(x6) 26: main_2(x40, x10) x22 -> map() h() (map_rev() h() x40) 27: cond_mult_n_m(0(), x1, x3) -> 0() 28: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 29: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 30: mult_1(x1) x2 -> mult_n(x1, x2) 31: mult(x2) x4 -> mult_n(x2, x4) 32: main_1(x0) x9 -> main_6(x9, mult(x9), map(), map_rev()) x0 33: cond_plus_n_m(0(), x1) -> x1 34: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 35: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 36: plus_1() x1 -> plus_n(x1) 37: plus() x2 -> plus_n(x2) 38: main(x40) -> main_xs_1(map(), map_rev(), x40) g(plus()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list cond_rmap_l_acc :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list -> 'a62 list cond_map_f_l :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x7, x6, x8, x10) x27 -> x6 h() (x8 h() x10) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x5, x11, x12, x16) x20 -> x12 h() (x16 h() x20) 9: main_4(x20, x9, x21, x12) x16 -> x12 h() (x16 h() x20) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: cond_rmap_l_acc(Nil(), x4, x7) -> x7 13: cond_rmap_l_acc(Cons(x17, x18), x8, x15) -> rmap(x8) x18 Cons(x8 x17, x15) 14: rmap_l(x4, x6) x7 -> cond_rmap_l_acc(x6, x4, x7) 15: rmap_1(x4) x6 -> rmap_l(x4, x6) 16: rmap(x8) x12 -> rmap_l(x8, x12) 17: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 18: map_rev() x4 -> map_rev_f(x4) 19: main_3(x81, x21, x45) x49 -> x49 h() (map_rev_f(h()) x81) 20: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 21: cond_map_f_l(Nil(), x3) -> Nil() 22: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 23: map_f(x3) x4 -> cond_map_f_l(x4, x3) 24: map_1() x3 -> map_f(x3) 25: map() x6 -> map_f(x6) 26: main_2(x81, x21) x45 -> map() h() (map_rev_f(h()) x81) 27: cond_mult_n_m(0(), x1, x3) -> 0() 28: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 29: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 30: mult_1(x1) x2 -> mult_n(x1, x2) 31: mult(x2) x4 -> mult_n(x2, x4) 32: main_1(x40) x10 -> map() h() (map_rev() h() x40) 33: cond_plus_n_m(0(), x1) -> x1 34: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 35: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 36: plus_1() x1 -> plus_n(x1) 37: plus() x2 -> plus_n(x2) 38: main(x20) -> map() h() (map_rev() h() x20) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list cond_rmap_l_acc :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list -> 'a62 list cond_map_f_l :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 8: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x7, x6, x8, x10) x27 -> x6 h() (x8 h() x10) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x5, x11, x12, x16) x20 -> x12 h() (x16 h() x20) 9: main_4(x20, x9, x21, x12) x16 -> x12 h() (x16 h() x20) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: cond_rmap_l_acc(Nil(), x4, x7) -> x7 13: cond_rmap_l_acc(Cons(x17, x18), x8, x15) -> rmap(x8) x18 Cons(x8 x17, x15) 14: rmap_l(x4, x6) x7 -> cond_rmap_l_acc(x6, x4, x7) 15: rmap_1(x4) x6 -> rmap_l(x4, x6) 16: rmap(x8) x12 -> rmap_l(x8, x12) 17: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 18: map_rev() x4 -> map_rev_f(x4) 19: main_3(x20, x43, x91) x99 -> x99 h() (rmap(h()) x20 Nil()) 20: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 21: cond_map_f_l(Nil(), x3) -> Nil() 22: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 23: map_f(x3) x4 -> cond_map_f_l(x4, x3) 24: map_1() x3 -> map_f(x3) 25: map() x6 -> map_f(x6) 26: main_2(x20, x43) x91 -> map() h() (rmap(h()) x20 Nil()) 27: cond_mult_n_m(0(), x1, x3) -> 0() 28: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 29: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 30: mult_1(x1) x2 -> mult_n(x1, x2) 31: mult(x2) x4 -> mult_n(x2, x4) 32: main_1(x81) x21 -> map() h() (map_rev_f(h()) x81) 33: cond_plus_n_m(0(), x1) -> x1 34: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 35: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 36: plus_1() x1 -> plus_n(x1) 37: plus() x2 -> plus_n(x2) 38: main(x41) -> map() h() (map_rev_f(h()) x41) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list cond_rmap_l_acc :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list -> 'a62 list cond_map_f_l :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 9: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x7, x6, x8, x10) x27 -> x6 h() (x8 h() x10) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x5, x11, x12, x16) x20 -> x12 h() (x16 h() x20) 9: main_4(x20, x9, x21, x12) x16 -> x12 h() (x16 h() x20) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: cond_rmap_l_acc(Nil(), x4, x7) -> x7 13: cond_rmap_l_acc(Cons(x17, x18), x8, x15) -> rmap(x8) x18 Cons(x8 x17, x15) 14: rmap_l(x4, x6) x7 -> cond_rmap_l_acc(x6, x4, x7) 15: rmap_1(x4) x6 -> rmap_l(x4, x6) 16: rmap(x8) x12 -> rmap_l(x8, x12) 17: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 18: map_rev() x4 -> map_rev_f(x4) 19: main_3(x20, x43, x91) x99 -> x99 h() (rmap(h()) x20 Nil()) 20: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 21: cond_map_f_l(Nil(), x3) -> Nil() 22: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 23: map_f(x3) x4 -> cond_map_f_l(x4, x3) 24: map_1() x3 -> map_f(x3) 25: map() x6 -> map_f(x6) 26: main_2(x20, x43) x91 -> map() h() (rmap(h()) x20 Nil()) 27: cond_mult_n_m(0(), x1, x3) -> 0() 28: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 29: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 30: mult_1(x1) x2 -> mult_n(x1, x2) 31: mult(x2) x4 -> mult_n(x2, x4) 32: main_1(x20) x43 -> map() h() (rmap(h()) x20 Nil()) 33: cond_plus_n_m(0(), x1) -> x1 34: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 35: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 36: plus_1() x1 -> plus_n(x1) 37: plus() x2 -> plus_n(x2) 38: main(x20) -> map() h() (rmap(h()) x20 Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list cond_rmap_l_acc :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list -> 'a62 list cond_map_f_l :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 10: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x7, x6, x8, x10) x27 -> x6 h() (x8 h() x10) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x5, x11, x12, x16) x20 -> x12 h() (x16 h() x20) 9: main_4(x20, x9, x21, x12) x16 -> x12 h() (x16 h() x20) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: cond_rmap_l_acc(Nil(), x4, x7) -> x7 13: cond_rmap_l_acc(Cons(x17, x18), x8, x15) -> rmap(x8) x18 Cons(x8 x17, x15) 14: rmap_l(x8, Nil()) x14 -> x14 15: rmap_l(x16, Cons(x34, x36)) x30 -> rmap(x16) x36 Cons(x16 x34, x30) 16: rmap_1(x4) x6 -> rmap_l(x4, x6) 17: rmap(x8) x12 -> rmap_l(x8, x12) 18: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 19: map_rev() x4 -> map_rev_f(x4) 20: main_3(x20, x43, x91) x99 -> x99 h() (rmap(h()) x20 Nil()) 21: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 22: cond_map_f_l(Nil(), x3) -> Nil() 23: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 24: map_f(x6) Nil() -> Nil() 25: map_f(x12) Cons(x20, x26) -> Cons(x12 x20, map() x12 x26) 26: map_1() x3 -> map_f(x3) 27: map() x6 -> map_f(x6) 28: main_2(x20, x43) x91 -> map() h() (rmap(h()) x20 Nil()) 29: cond_mult_n_m(0(), x1, x3) -> 0() 30: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 31: mult_n(x2, 0()) x6 -> 0() 32: mult_n(x2, S(x8)) x6 -> S(x2 (mult(x2) x8 x6) x6) 33: mult_1(x1) x2 -> mult_n(x1, x2) 34: mult(x2) x4 -> mult_n(x2, x4) 35: main_1(x20) x43 -> map() h() (rmap(h()) x20 Nil()) 36: cond_plus_n_m(0(), x1) -> x1 37: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 38: plus_n(x2) 0() -> x2 39: plus_n(x2) S(x6) -> S(plus() x2 x6) 40: plus_1() x1 -> plus_n(x1) 41: plus() x2 -> plus_n(x2) 42: main(x20) -> map() h() (rmap(h()) x20 Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list cond_rmap_l_acc :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list -> 'a62 list cond_map_f_l :: 'a62 list -> ('a62 -> 'a62) -> 'a62 list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 11: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x7, x6, x8, x10) x27 -> x6 h() (x8 h() x10) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x5, x11, x12, x16) x20 -> x12 h() (x16 h() x20) 9: main_4(x20, x9, x21, x12) x16 -> x12 h() (x16 h() x20) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 14: rmap_l(x8, Nil()) x14 -> x14 15: rmap_l(x16, Cons(x34, x36)) x30 -> rmap(x16) x36 Cons(x16 x34, x30) 16: rmap_1(x4) x6 -> rmap_l(x4, x6) 17: rmap(x8) x12 -> rmap_l(x8, x12) 18: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 19: map_rev() x4 -> map_rev_f(x4) 20: main_3(x20, x43, x91) x99 -> x99 h() (rmap(h()) x20 Nil()) 21: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 24: map_f(x6) Nil() -> Nil() 25: map_f(x12) Cons(x20, x26) -> Cons(x12 x20, map() x12 x26) 26: map_1() x3 -> map_f(x3) 27: map() x6 -> map_f(x6) 28: main_2(x20, x43) x91 -> map() h() (rmap(h()) x20 Nil()) 31: mult_n(x2, 0()) x6 -> 0() 32: mult_n(x2, S(x8)) x6 -> S(x2 (mult(x2) x8 x6) x6) 33: mult_1(x1) x2 -> mult_n(x1, x2) 34: mult(x2) x4 -> mult_n(x2, x4) 35: main_1(x20) x43 -> map() h() (rmap(h()) x20 Nil()) 38: plus_n(x2) 0() -> x2 39: plus_n(x2) S(x6) -> S(plus() x2 x6) 40: plus_1() x1 -> plus_n(x1) 41: plus() x2 -> plus_n(x2) 42: main(x20) -> map() h() (rmap(h()) x20 Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: NeededRules + Details: none * Step 12: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_5(x0) x5 -> x5 x0 2: main_xs_2(x3, x4, x5) x8 -> x3 x8 (x4 x8 x5) 3: h() x8 -> x8 4: main_xs_1(x6, x8, x10) x15 -> x6 h() (x8 h() x10) 5: g(x1) x7 -> x1 x7 S(S(0())) 6: main_xs(x7, x6, x8, x10) x27 -> x6 h() (x8 h() x10) 7: f(x2) x6 -> x2 x6 (x2 x6 x6) 8: main_6(x5, x11, x12, x16) x20 -> x12 h() (x16 h() x20) 9: main_4(x20, x9, x21, x12) x16 -> x12 h() (x16 h() x20) 10: map_rev_f_l(x5) x6 -> x6 x5 Nil() 11: rmap_l_acc_2(x4, x9) x10 -> rmap(x4) x9 x10 12: rmap_l(x8, Nil()) x14 -> x14 13: rmap_l(x16, Cons(x34, x36)) x30 -> rmap(x16) x36 Cons(x16 x34, x30) 14: rmap_1(x4) x6 -> rmap_l(x4, x6) 15: rmap(x8) x12 -> rmap_l(x8, x12) 16: map_rev_f(x9) x10 -> rmap(x9) x10 Nil() 17: map_rev() x4 -> map_rev_f(x4) 18: main_3(x20, x43, x91) x99 -> x99 h() (rmap(h()) x20 Nil()) 19: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 20: map_f(x6) Nil() -> Nil() 21: map_f(x12) Cons(x20, x26) -> Cons(x12 x20, map() x12 x26) 22: map_1() x3 -> map_f(x3) 23: map() x6 -> map_f(x6) 24: main_2(x20, x43) x91 -> map() h() (rmap(h()) x20 Nil()) 25: mult_n(x2, 0()) x6 -> 0() 26: mult_n(x2, S(x8)) x6 -> S(x2 (mult(x2) x8 x6) x6) 27: mult_1(x1) x2 -> mult_n(x1, x2) 28: mult(x2) x4 -> mult_n(x2, x4) 29: main_1(x20) x43 -> map() h() (rmap(h()) x20 Nil()) 30: plus_n(x2) 0() -> x2 31: plus_n(x2) S(x6) -> S(plus() x2 x6) 32: plus_1() x1 -> plus_n(x1) 33: plus() x2 -> plus_n(x2) 34: main(x20) -> map() h() (rmap(h()) x20 Nil()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_rev_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list g :: (nat -> nat -> nat) -> nat -> nat h :: 'a62 -> 'a62 map_rev_f_l :: 'a62 list -> ('a62 list -> 'a62 list -> 'a62 list) -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_rev :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list main_1 :: 'a62 list -> (nat -> nat -> nat) -> 'a62 list map_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat rmap_1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main_xs_1 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> (nat -> nat) -> 'a62 list rmap_l_acc_2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map_f_l_2 :: ('a62 -> 'a62) -> 'a62 -> 'a62 list -> 'a62 list main_2 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> 'a62 list main_xs_2 :: (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> ('a62 -> 'a62) -> 'a62 list main_3 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_4 :: 'a62 list -> (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list main_5 :: 'a62 list -> ('a62 list -> 'a62 list) -> 'a62 list main_6 :: (nat -> nat -> nat) -> (nat -> nat -> nat) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> (('a62 -> 'a62) -> 'a62 list -> 'a62 list) -> 'a62 list -> 'a62 list map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Nil() | S(X{*}) | S(X{*}) | 0() | Nil() | S(X{*}) | S(X{*}) | 0() | 0() | Nil() | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | Nil() | Cons(X{*},X{*}) | Nil() | Nil() | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | Nil() | 0() | S(X{*}) | S(X{*}) ,V{x6_20} -> V{x6_23} ,V{x6_23} -> V{x12_21} | h() ,V{x8_3} -> V{x20_21} | V{x34_13} ,V{x8_12} -> V{x8_15} ,V{x8_15} -> V{x16_13} | h() ,V{x12_15} -> V{x36_13} | V{x20_34} ,V{x12_21} -> V{x6_23} ,V{x14_12} -> Cons(R{3},V{x30_13}) | Nil() ,V{x16_13} -> V{x8_15} ,V{x20_21} -> R{3} ,V{x20_34} -> X{*} ,V{x26_21} -> V{x30_13} ,V{x30_13} -> Cons(R{3},V{x30_13}) | Nil() ,V{x34_13} -> X{*} ,V{x36_13} -> X{*} ,R{0} -> R{34} | main(X{*}) ,R{3} -> V{x8_3} ,R{12} -> V{x14_12} ,R{13} -> R{13} | R{12} | @(R{15},Cons(R{3},V{x30_13})) | @(@(rmap(V{x16_13}),V{x36_13}),Cons(R{3},V{x30_13})) | @(R{15},Cons(@(V{x16_13},V{x34_13}),V{x30_13})) | @(@(rmap(V{x16_13}),V{x36_13}),Cons(@(V{x16_13},V{x34_13}),V{x30_13})) ,R{15} -> rmap_l(V{x8_15},V{x12_15}) ,R{20} -> Nil() ,R{21} -> Cons(R{3},R{20}) | Cons(R{3},R{21}) | Cons(@(V{x12_21},V{x20_21}),R{21}) | Cons(@(V{x12_21},V{x20_21}),R{20}) | Cons(R{3},@(R{23},V{x26_21})) | Cons(@(V{x12_21},V{x20_21}),@(R{23},V{x26_21})) | Cons(R{3},@(@(map(),V{x12_21}),V{x26_21})) | Cons(@(V{x12_21},V{x20_21}),@(@(map(),V{x12_21}),V{x26_21})) ,R{23} -> map_f(V{x6_23}) ,R{34} -> R{21} | R{20} | @(R{23},R{12}) | @(R{23},R{13}) | @(@(map(),h()),R{13}) | @(@(map(),h()),R{12}) | @(R{23},@(R{15},Nil())) | @(@(map(),h()),@(R{15},Nil())) | @(R{23},@(@(rmap(h()),V{x20_34}),Nil())) | @(@(map(),h()),@(@(rmap(h()),V{x20_34}),Nil()))} * Step 13: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 3: h() x8 -> x8 12: rmap_l(h(), Nil()) x1 -> x1 13: rmap_l(h(), Cons(x3, x2)) x1 -> rmap(h()) x2 Cons(h() x3, x1) 15: rmap(h()) x1 -> rmap_l(h(), x1) 20: map_f(h()) Nil() -> Nil() 21: map_f(h()) Cons(x2, x1) -> Cons(h() x2, map() h() x1) 23: map() h() -> map_f(h()) 34: main(x1) -> map() h() (rmap(h()) x1 Nil()) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list h :: 'a62 -> 'a62 rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list map :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list rmap :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list main :: 'a62 list -> 'a62 list + Applied Processor: UncurryATRS + Details: none * Step 14: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: h#1(x8) -> x8 2: rmap_l#1(h(), Nil(), x1) -> x1 3: rmap_l#1(h(), Cons(x3, x2), x1) -> rmap#2(h(), x2, Cons(h#1(x3), x1)) 4: rmap#1(h(), x1) -> rmap_l(h(), x1) 5: rmap#2(h(), x1, x2) -> rmap_l#1(h(), x1, x2) 6: map_f#1(h(), Nil()) -> Nil() 7: map_f#1(h(), Cons(x2, x1)) -> Cons(h#1(x2), map#2(h(), x1)) 8: map#1(h()) -> map_f(h()) 9: map#2(h(), x0) -> map_f#1(h(), x0) 10: main(x1) -> map#2(h(), rmap#2(h(), x1, Nil())) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list h :: 'a62 -> 'a62 h#1 :: 'a62 -> 'a62 main :: 'a62 list -> 'a62 list map#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_f#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list rmap#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list rmap#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list rmap_l#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: h#1(x8) -> x8 2: rmap_l#1(h(), Nil(), x1) -> x1 3: rmap_l#1(h(), Cons(x16, x5), x3) -> rmap#2(h(), x5, Cons(x16, x3)) 4: rmap#1(h(), x1) -> rmap_l(h(), x1) 5: rmap#2(h(), x1, x2) -> rmap_l#1(h(), x1, x2) 6: map_f#1(h(), Nil()) -> Nil() 7: map_f#1(h(), Cons(x16, x3)) -> Cons(x16, map#2(h(), x3)) 8: map#1(h()) -> map_f(h()) 9: map#2(h(), x0) -> map_f#1(h(), x0) 10: main(x1) -> map#2(h(), rmap#2(h(), x1, Nil())) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list h :: 'a62 -> 'a62 h#1 :: 'a62 -> 'a62 main :: 'a62 list -> 'a62 list map#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_f :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_f#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list rmap#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list rmap#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list rmap_l :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list rmap_l#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 2: rmap_l#1(h(), Nil(), x1) -> x1 3: rmap_l#1(h(), Cons(x16, x5), x3) -> rmap#2(h(), x5, Cons(x16, x3)) 5: rmap#2(h(), x1, x2) -> rmap_l#1(h(), x1, x2) 6: map_f#1(h(), Nil()) -> Nil() 7: map_f#1(h(), Cons(x16, x3)) -> Cons(x16, map#2(h(), x3)) 9: map#2(h(), x0) -> map_f#1(h(), x0) 10: main(x1) -> map#2(h(), rmap#2(h(), x1, Nil())) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list h :: 'a62 -> 'a62 main :: 'a62 list -> 'a62 list map#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_f#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list rmap#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list rmap_l#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 17: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: rmap_l#1(h(), Nil(), x1) -> x1 2: rmap_l#1(h(), Cons(x16, x5), x3) -> rmap#2(h(), x5, Cons(x16, x3)) 3: rmap#2(h(), Nil(), x2) -> x2 4: rmap#2(h(), Cons(x32, x10), x6) -> rmap#2(h(), x10, Cons(x32, x6)) 5: map_f#1(h(), Nil()) -> Nil() 6: map_f#1(h(), Cons(x16, x3)) -> Cons(x16, map#2(h(), x3)) 7: map#2(h(), Nil()) -> Nil() 8: map#2(h(), Cons(x32, x6)) -> Cons(x32, map#2(h(), x6)) 9: main(x1) -> map#2(h(), rmap#2(h(), x1, Nil())) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list h :: 'a62 -> 'a62 main :: 'a62 list -> 'a62 list map#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list map_f#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list rmap#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list rmap_l#1 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 18: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 3: rmap#2(h(), Nil(), x2) -> x2 4: rmap#2(h(), Cons(x32, x10), x6) -> rmap#2(h(), x10, Cons(x32, x6)) 7: map#2(h(), Nil()) -> Nil() 8: map#2(h(), Cons(x32, x6)) -> Cons(x32, map#2(h(), x6)) 9: main(x1) -> map#2(h(), rmap#2(h(), x1, Nil())) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list h :: 'a62 -> 'a62 main :: 'a62 list -> 'a62 list map#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list rmap#2 :: ('a62 -> 'a62) -> 'a62 list -> 'a62 list -> 'a62 list + Applied Processor: Compression + Details: none * Step 19: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: rmap#2(Nil(), x2) -> x2 2: rmap#2(Cons(x32, x10), x6) -> rmap#2(x10, Cons(x32, x6)) 3: map#2(Nil()) -> Nil() 4: map#2(Cons(x32, x6)) -> Cons(x32, map#2(x6)) 5: main(x1) -> map#2(rmap#2(x1, Nil())) where Cons :: 'a -> 'a list -> 'a list Nil :: 'a list main :: 'a62 list -> 'a62 list map#2 :: 'a62 list -> 'a62 list rmap#2 :: 'a62 list -> 'a62 list -> 'a62 list + Applied Processor: ToTctProblem + Details: none * Step 20: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: main(x1) -> map#2(rmap#2(x1,Nil())) map#2(Cons(x32,x6)) -> Cons(x32,map#2(x6)) map#2(Nil()) -> Nil() rmap#2(Cons(x32,x10),x6) -> rmap#2(x10,Cons(x32,x6)) rmap#2(Nil(),x2) -> x2 - Signature: {main/1,map#2/1,rmap#2/2} / {Cons/2,Nil/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(Cons) = {2}, uargs(map#2) = {1} Following symbols are considered usable: {main,map#2,rmap#2} TcT has computed the following interpretation: p(Cons) = 4 + x1 + x2 p(Nil) = 1 p(main) = 15 + 8*x1 p(map#2) = 1 + 2*x1 p(rmap#2) = 4 + 4*x1 + 2*x2 Following rules are strictly oriented: main(x1) = 15 + 8*x1 > 13 + 8*x1 = map#2(rmap#2(x1,Nil())) map#2(Cons(x32,x6)) = 9 + 2*x32 + 2*x6 > 5 + x32 + 2*x6 = Cons(x32,map#2(x6)) map#2(Nil()) = 3 > 1 = Nil() rmap#2(Cons(x32,x10),x6) = 20 + 4*x10 + 4*x32 + 2*x6 > 12 + 4*x10 + 2*x32 + 2*x6 = rmap#2(x10,Cons(x32,x6)) rmap#2(Nil(),x2) = 8 + 2*x2 > x2 = x2 Following rules are (at-least) weakly oriented: * Step 21: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: main(x1) -> map#2(rmap#2(x1,Nil())) map#2(Cons(x32,x6)) -> Cons(x32,map#2(x6)) map#2(Nil()) -> Nil() rmap#2(Cons(x32,x10),x6) -> rmap#2(x10,Cons(x32,x6)) rmap#2(Nil(),x2) -> x2 - Signature: {main/1,map#2/1,rmap#2/2} / {Cons/2,Nil/0} - 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^1))