WORST_CASE(?,O(n^4)) * Step 1: Desugar WORST_CASE(?,O(n^4)) + 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) ;; let main xs = let f x = mult x (mult x x) in map f xs;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^4)) + Considered Problem: λxs : nat list. (λplus : nat -> nat -> nat. (λmult : nat -> nat -> nat. (λmap : (nat -> nat) -> nat list -> nat list. (λmain : nat list -> nat list. main xs) (λxs : nat list. (λf : nat -> nat. map f xs) (λx : nat. mult x (mult x x)))) (μmap : (nat -> nat) -> nat list -> nat list. λf : nat -> nat. λl : nat list. case l of | Nil -> Nil | Cons -> λx : nat. λxs : nat list. (λys : nat 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)) : nat list -> nat 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^4)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_xs(x3, x4) x5 -> x3 x5 x4 3: f(x2) x5 -> x2 x5 (x2 x5 x5) 4: main_5(x2, x3) x4 -> main_xs(x3, x4) f(x2) 5: main_3(x0, x2) x3 -> main_4(x0) main_5(x2, x3) 6: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 7: cond_map_f_l(Nil(), x3) -> Nil() 8: cond_map_f_l(Cons(x5, x6), x3) -> map_f_l_2(x3, x5) (map() x3 x6) 9: map_f(x3) x4 -> cond_map_f_l(x4, x3) 10: map_1() x3 -> map_f(x3) 11: map() x0 -> map_1() x0 12: main_2(x0) x2 -> main_3(x0, x2) map() 13: cond_mult_n_m(0(), x1, x3) -> 0() 14: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 15: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 16: mult_1(x1) x2 -> mult_n(x1, x2) 17: mult(x1) x2 -> mult_1(x1) x2 18: main_1(x0) x1 -> main_2(x0) mult(x1) 19: cond_plus_n_m(0(), x1) -> x1 20: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 21: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 22: plus_1() x1 -> plus_n(x1) 23: plus() x0 -> plus_1() x0 24: 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 :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: ((nat -> nat) -> nat list -> nat list) -> nat list -> (nat -> nat) -> nat list main_1 :: nat list -> (nat -> nat -> nat) -> nat list map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat map_f_l_2 :: (nat -> nat) -> nat -> nat list -> nat list main_2 :: nat list -> (nat -> nat -> nat) -> nat list main_3 :: nat list -> (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list main_4 :: nat list -> (nat list -> nat list) -> nat list main_5 :: (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list -> nat list cond_map_f_l :: nat list -> (nat -> nat) -> nat list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^4)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_xs(x3, x4) x5 -> x3 x5 x4 3: f(x2) x5 -> x2 x5 (x2 x5 x5) 4: main_5(x5, x6) x8 -> x6 f(x5) x8 5: main_3(x0, x5) x7 -> main_5(x5, x7) x0 6: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 7: cond_map_f_l(Nil(), x3) -> Nil() 8: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 9: map_f(x3) x4 -> cond_map_f_l(x4, x3) 10: map_1() x3 -> map_f(x3) 11: map() x6 -> map_f(x6) 12: main_2(x0) x4 -> main_4(x0) main_5(x4, map()) 13: cond_mult_n_m(0(), x1, x3) -> 0() 14: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 15: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 16: mult_1(x1) x2 -> mult_n(x1, x2) 17: mult(x2) x4 -> mult_n(x2, x4) 18: main_1(x0) x3 -> main_3(x0, mult(x3)) map() 19: cond_plus_n_m(0(), x1) -> x1 20: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 21: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 22: plus_1() x1 -> plus_n(x1) 23: plus() x2 -> plus_n(x2) 24: main(x0) -> main_2(x0) 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 :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: ((nat -> nat) -> nat list -> nat list) -> nat list -> (nat -> nat) -> nat list main_1 :: nat list -> (nat -> nat -> nat) -> nat list map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat map_f_l_2 :: (nat -> nat) -> nat -> nat list -> nat list main_2 :: nat list -> (nat -> nat -> nat) -> nat list main_3 :: nat list -> (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list main_4 :: nat list -> (nat list -> nat list) -> nat list main_5 :: (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list -> nat list cond_map_f_l :: nat list -> (nat -> nat) -> nat list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^4)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_xs(x3, x4) x5 -> x3 x5 x4 3: f(x2) x5 -> x2 x5 (x2 x5 x5) 4: main_5(x5, x6) x8 -> x6 f(x5) x8 5: main_3(x16, x10) x12 -> x12 f(x10) x16 6: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 7: cond_map_f_l(Nil(), x3) -> Nil() 8: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 9: map_f(x3) x4 -> cond_map_f_l(x4, x3) 10: map_1() x3 -> map_f(x3) 11: map() x6 -> map_f(x6) 12: main_2(x0) x9 -> main_5(x9, map()) x0 13: cond_mult_n_m(0(), x1, x3) -> 0() 14: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 15: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 16: mult_1(x1) x2 -> mult_n(x1, x2) 17: mult(x2) x4 -> mult_n(x2, x4) 18: main_1(x0) x7 -> main_5(mult(x7), map()) x0 19: cond_plus_n_m(0(), x1) -> x1 20: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 21: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 22: plus_1() x1 -> plus_n(x1) 23: plus() x2 -> plus_n(x2) 24: main(x0) -> main_4(x0) main_5(mult(plus()), map()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: ((nat -> nat) -> nat list -> nat list) -> nat list -> (nat -> nat) -> nat list main_1 :: nat list -> (nat -> nat -> nat) -> nat list map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat map_f_l_2 :: (nat -> nat) -> nat -> nat list -> nat list main_2 :: nat list -> (nat -> nat -> nat) -> nat list main_3 :: nat list -> (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list main_4 :: nat list -> (nat list -> nat list) -> nat list main_5 :: (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list -> nat list cond_map_f_l :: nat list -> (nat -> nat) -> nat list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^4)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_xs(x3, x4) x5 -> x3 x5 x4 3: f(x2) x5 -> x2 x5 (x2 x5 x5) 4: main_5(x5, x6) x8 -> x6 f(x5) x8 5: main_3(x16, x10) x12 -> x12 f(x10) x16 6: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 7: cond_map_f_l(Nil(), x3) -> Nil() 8: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 9: map_f(x3) x4 -> cond_map_f_l(x4, x3) 10: map_1() x3 -> map_f(x3) 11: map() x6 -> map_f(x6) 12: main_2(x16) x10 -> map() f(x10) x16 13: cond_mult_n_m(0(), x1, x3) -> 0() 14: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 15: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 16: mult_1(x1) x2 -> mult_n(x1, x2) 17: mult(x2) x4 -> mult_n(x2, x4) 18: main_1(x16) x15 -> map() f(mult(x15)) x16 19: cond_plus_n_m(0(), x1) -> x1 20: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 21: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 22: plus_1() x1 -> plus_n(x1) 23: plus() x2 -> plus_n(x2) 24: main(x0) -> main_5(mult(plus()), map()) x0 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: ((nat -> nat) -> nat list -> nat list) -> nat list -> (nat -> nat) -> nat list main_1 :: nat list -> (nat -> nat -> nat) -> nat list map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat map_f_l_2 :: (nat -> nat) -> nat -> nat list -> nat list main_2 :: nat list -> (nat -> nat -> nat) -> nat list main_3 :: nat list -> (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list main_4 :: nat list -> (nat list -> nat list) -> nat list main_5 :: (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list -> nat list cond_map_f_l :: nat list -> (nat -> nat) -> nat list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^4)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_xs(x3, x4) x5 -> x3 x5 x4 3: f(x2) x5 -> x2 x5 (x2 x5 x5) 4: main_5(x5, x6) x8 -> x6 f(x5) x8 5: main_3(x16, x10) x12 -> x12 f(x10) x16 6: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 7: cond_map_f_l(Nil(), x3) -> Nil() 8: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 9: map_f(x3) x4 -> cond_map_f_l(x4, x3) 10: map_1() x3 -> map_f(x3) 11: map() x6 -> map_f(x6) 12: main_2(x16) x10 -> map() f(x10) x16 13: cond_mult_n_m(0(), x1, x3) -> 0() 14: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 15: mult_n(x1, x2) x3 -> cond_mult_n_m(x2, x1, x3) 16: mult_1(x1) x2 -> mult_n(x1, x2) 17: mult(x2) x4 -> mult_n(x2, x4) 18: main_1(x16) x15 -> map() f(mult(x15)) x16 19: cond_plus_n_m(0(), x1) -> x1 20: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 21: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 22: plus_1() x1 -> plus_n(x1) 23: plus() x2 -> plus_n(x2) 24: main(x16) -> map() f(mult(plus())) x16 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: ((nat -> nat) -> nat list -> nat list) -> nat list -> (nat -> nat) -> nat list main_1 :: nat list -> (nat -> nat -> nat) -> nat list map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat map_f_l_2 :: (nat -> nat) -> nat -> nat list -> nat list main_2 :: nat list -> (nat -> nat -> nat) -> nat list main_3 :: nat list -> (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list main_4 :: nat list -> (nat list -> nat list) -> nat list main_5 :: (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list -> nat list cond_map_f_l :: nat list -> (nat -> nat) -> nat list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^4)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_xs(x3, x4) x5 -> x3 x5 x4 3: f(x2) x5 -> x2 x5 (x2 x5 x5) 4: main_5(x5, x6) x8 -> x6 f(x5) x8 5: main_3(x16, x10) x12 -> x12 f(x10) x16 6: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 7: cond_map_f_l(Nil(), x3) -> Nil() 8: cond_map_f_l(Cons(x10, x13), x6) -> Cons(x6 x10, map() x6 x13) 9: map_f(x6) Nil() -> Nil() 10: map_f(x12) Cons(x20, x26) -> Cons(x12 x20, map() x12 x26) 11: map_1() x3 -> map_f(x3) 12: map() x6 -> map_f(x6) 13: main_2(x16) x10 -> map() f(x10) x16 14: cond_mult_n_m(0(), x1, x3) -> 0() 15: cond_mult_n_m(S(x4), x1, x3) -> S(x1 (mult(x1) x4 x3) x3) 16: mult_n(x2, 0()) x6 -> 0() 17: mult_n(x2, S(x8)) x6 -> S(x2 (mult(x2) x8 x6) x6) 18: mult_1(x1) x2 -> mult_n(x1, x2) 19: mult(x2) x4 -> mult_n(x2, x4) 20: main_1(x16) x15 -> map() f(mult(x15)) x16 21: cond_plus_n_m(0(), x1) -> x1 22: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 23: plus_n(x2) 0() -> x2 24: plus_n(x2) S(x6) -> S(plus() x2 x6) 25: plus_1() x1 -> plus_n(x1) 26: plus() x2 -> plus_n(x2) 27: main(x16) -> map() f(mult(plus())) x16 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: ((nat -> nat) -> nat list -> nat list) -> nat list -> (nat -> nat) -> nat list main_1 :: nat list -> (nat -> nat -> nat) -> nat list map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat map_f_l_2 :: (nat -> nat) -> nat -> nat list -> nat list main_2 :: nat list -> (nat -> nat -> nat) -> nat list main_3 :: nat list -> (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list main_4 :: nat list -> (nat list -> nat list) -> nat list main_5 :: (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list -> nat list cond_map_f_l :: nat list -> (nat -> nat) -> nat list cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^4)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_xs(x3, x4) x5 -> x3 x5 x4 3: f(x2) x5 -> x2 x5 (x2 x5 x5) 4: main_5(x5, x6) x8 -> x6 f(x5) x8 5: main_3(x16, x10) x12 -> x12 f(x10) x16 6: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 9: map_f(x6) Nil() -> Nil() 10: map_f(x12) Cons(x20, x26) -> Cons(x12 x20, map() x12 x26) 11: map_1() x3 -> map_f(x3) 12: map() x6 -> map_f(x6) 13: main_2(x16) x10 -> map() f(x10) x16 16: mult_n(x2, 0()) x6 -> 0() 17: mult_n(x2, S(x8)) x6 -> S(x2 (mult(x2) x8 x6) x6) 18: mult_1(x1) x2 -> mult_n(x1, x2) 19: mult(x2) x4 -> mult_n(x2, x4) 20: main_1(x16) x15 -> map() f(mult(x15)) x16 23: plus_n(x2) 0() -> x2 24: plus_n(x2) S(x6) -> S(plus() x2 x6) 25: plus_1() x1 -> plus_n(x1) 26: plus() x2 -> plus_n(x2) 27: main(x16) -> map() f(mult(plus())) x16 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: ((nat -> nat) -> nat list -> nat list) -> nat list -> (nat -> nat) -> nat list main_1 :: nat list -> (nat -> nat -> nat) -> nat list map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat map_f_l_2 :: (nat -> nat) -> nat -> nat list -> nat list main_2 :: nat list -> (nat -> nat -> nat) -> nat list main_3 :: nat list -> (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list main_4 :: nat list -> (nat list -> nat list) -> nat list main_5 :: (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^4)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_xs(x3, x4) x5 -> x3 x5 x4 3: f(x2) x5 -> x2 x5 (x2 x5 x5) 4: main_5(x5, x6) x8 -> x6 f(x5) x8 5: main_3(x16, x10) x12 -> x12 f(x10) x16 6: map_f_l_2(x3, x5) x7 -> Cons(x3 x5, x7) 7: map_f(x6) Nil() -> Nil() 8: map_f(x12) Cons(x20, x26) -> Cons(x12 x20, map() x12 x26) 9: map_1() x3 -> map_f(x3) 10: map() x6 -> map_f(x6) 11: main_2(x16) x10 -> map() f(x10) x16 12: mult_n(x2, 0()) x6 -> 0() 13: mult_n(x2, S(x8)) x6 -> S(x2 (mult(x2) x8 x6) x6) 14: mult_1(x1) x2 -> mult_n(x1, x2) 15: mult(x2) x4 -> mult_n(x2, x4) 16: main_1(x16) x15 -> map() f(mult(x15)) x16 17: plus_n(x2) 0() -> x2 18: plus_n(x2) S(x6) -> S(plus() x2 x6) 19: plus_1() x1 -> plus_n(x1) 20: plus() x2 -> plus_n(x2) 21: main(x16) -> map() f(mult(plus())) x16 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat main_xs :: ((nat -> nat) -> nat list -> nat list) -> nat list -> (nat -> nat) -> nat list main_1 :: nat list -> (nat -> nat -> nat) -> nat list map_1 :: (nat -> nat) -> nat list -> nat list mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat map_f_l_2 :: (nat -> nat) -> nat -> nat list -> nat list main_2 :: nat list -> (nat -> nat -> nat) -> nat list main_3 :: nat list -> (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list main_4 :: nat list -> (nat list -> nat list) -> nat list main_5 :: (nat -> nat -> nat) -> ((nat -> nat) -> nat list -> nat list) -> nat list -> nat list map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> S(X{*}) | S(X{*}) | 0() | S(X{*}) | S(X{*}) | 0() | 0() | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | Nil() | Cons(X{*},X{*}) ,V{x2_3} -> mult(plus()) ,V{x2_12} -> V{x2_15} ,V{x2_13} -> V{x2_15} ,V{x2_15} -> V{x2_13} | plus() ,V{x2_17} -> V{x2_20} ,V{x2_18} -> V{x2_20} ,V{x2_20} -> V{x2_18} | R{13} | R{12} ,V{x4_15} -> V{x8_13} | V{x5_3} ,V{x5_3} -> V{x20_8} ,V{x6_7} -> V{x6_10} ,V{x6_10} -> V{x12_8} | f(mult(plus())) ,V{x6_12} -> R{13} | V{x6_13} | R{12} | V{x5_3} ,V{x6_13} -> R{13} | V{x6_13} | R{12} | V{x5_3} ,V{x6_18} -> @(@(plus(),V{x2_18}),V{x6_18}) | @(R{20},V{x6_18}) | @(@(V{x2_13},@(@(mult(V{x2_13}),V{x8_13}),V{x6_13})),V{x6_13}) | @(@(V{x2_13},@(R{15},V{x6_13})),V{x6_13}) | @(@(V{x2_13},R{12}),V{x6_13}) | @(@(V{x2_13},R{13}),V{x6_13}) | @(R{20},V{x6_13}) | R{17} | R{18} | X{*} ,V{x8_13} -> X{*} ,V{x12_8} -> V{x6_10} ,V{x16_21} -> X{*} ,V{x20_8} -> X{*} ,V{x26_8} -> X{*} ,R{0} -> R{21} | main(X{*}) ,R{3} -> R{13} | R{12} | @(R{15},R{12}) | @(R{15},R{13}) | @(@(V{x2_3},V{x5_3}),R{13}) | @(@(V{x2_3},V{x5_3}),R{12}) | @(R{15},@(R{15},V{x5_3})) | @(@(V{x2_3},V{x5_3}),@(R{15},V{x5_3})) | @(R{15},@(@(V{x2_3},V{x5_3}),V{x5_3})) | @(@(V{x2_3},V{x5_3}),@(@(V{x2_3},V{x5_3}),V{x5_3})) ,R{7} -> Nil() ,R{8} -> Cons(R{3},R{7}) | Cons(R{3},R{8}) | Cons(@(V{x12_8},V{x20_8}),R{8}) | Cons(@(V{x12_8},V{x20_8}),R{7}) | Cons(R{3},@(R{10},V{x26_8})) | Cons(@(V{x12_8},V{x20_8}),@(R{10},V{x26_8})) | Cons(R{3},@(@(map(),V{x12_8}),V{x26_8})) | Cons(@(V{x12_8},V{x20_8}),@(@(map(),V{x12_8}),V{x26_8})) ,R{10} -> map_f(V{x6_10}) ,R{12} -> 0() ,R{13} -> S(R{18}) | S(R{17}) | S(@(R{20},V{x6_13})) | S(@(@(V{x2_13},R{13}),V{x6_13})) | S(@(@(V{x2_13},R{12}),V{x6_13})) | S(@(@(V{x2_13},@(R{15},V{x6_13})),V{x6_13})) | S(@(@(V{x2_13},@(@(mult(V{x2_13}),V{x8_13}),V{x6_13})),V{x6_13})) ,R{15} -> mult_n(V{x2_15},V{x4_15}) ,R{17} -> V{x2_17} ,R{18} -> S(R{18}) | S(R{17}) | S(@(R{20},V{x6_18})) | S(@(@(plus(),V{x2_18}),V{x6_18})) ,R{20} -> plus_n(V{x2_20}) ,R{21} -> R{8} | R{7} | @(R{10},V{x16_21}) | @(@(map(),f(mult(plus()))),V{x16_21})} * Step 11: UncurryATRS WORST_CASE(?,O(n^4)) + Considered Problem: 3: f(mult(plus())) x1 -> mult(plus()) x1 (mult(plus()) x1 x1) 7: map_f(f(mult(plus()))) Nil() -> Nil() 8: map_f(f(mult(plus()))) Cons(x2, x1) -> Cons(f(mult(plus())) x2, map() f(mult(plus())) x1) 10: map() f(mult(plus())) -> map_f(f(mult(plus()))) 12: mult_n(plus(), 0()) x1 -> 0() 13: mult_n(plus(), S(x2)) x1 -> S(plus() (mult(plus()) x2 x1) x1) 15: mult(plus()) x1 -> mult_n(plus(), x1) 17: plus_n(x2) 0() -> x2 18: plus_n(x2) S(x1) -> S(plus() x2 x1) 20: plus() x2 -> plus_n(x2) 21: main(x1) -> map() f(mult(plus())) x1 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat map_f :: (nat -> nat) -> nat list -> nat list mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat map :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: nat list -> nat list + Applied Processor: UncurryATRS + Details: none * Step 12: UsableRules WORST_CASE(?,O(n^4)) + Considered Problem: 1: f#1(mult(plus()), x1) -> mult#2(plus(), x1, mult#2(plus(), x1, x1)) 2: map_f#1(f(mult(plus())), Nil()) -> Nil() 3: map_f#1(f(mult(plus())), Cons(x2, x1)) -> Cons(f#1(mult(plus()), x2), map#2(f(mult(plus())), x1)) 4: map#1(f(mult(plus()))) -> map_f(f(mult(plus()))) 5: map#2(f(mult(plus())), x0) -> map_f#1(f(mult(plus())), x0) 6: mult_n#1(plus(), 0(), x1) -> 0() 7: mult_n#1(plus(), S(x2), x1) -> S(plus#2(mult#2(plus(), x2, x1), x1)) 8: mult#1(plus(), x1) -> mult_n(plus(), x1) 9: mult#2(plus(), x1, x2) -> mult_n#1(plus(), x1, x2) 10: plus_n#1(x2, 0()) -> x2 11: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 12: plus#1(x2) -> plus_n(x2) 13: plus#2(x2, x3) -> plus_n#1(x2, x3) 14: main(x1) -> map#2(f(mult(plus())), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat f#1 :: (nat -> nat -> nat) -> nat -> nat main :: nat list -> nat list map#1 :: (nat -> nat) -> nat list -> nat list map#2 :: (nat -> nat) -> nat list -> nat list map_f :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#1 :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat mult_n#1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#1 :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_n :: nat -> nat -> nat plus_n#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 13: Inline WORST_CASE(?,O(n^4)) + Considered Problem: 1: f#1(mult(plus()), x1) -> mult#2(plus(), x1, mult#2(plus(), x1, x1)) 2: map_f#1(f(mult(plus())), Nil()) -> Nil() 3: map_f#1(f(mult(plus())), Cons(x2, x1)) -> Cons(f#1(mult(plus()), x2), map#2(f(mult(plus())), x1)) 5: map#2(f(mult(plus())), x0) -> map_f#1(f(mult(plus())), x0) 6: mult_n#1(plus(), 0(), x1) -> 0() 7: mult_n#1(plus(), S(x2), x1) -> S(plus#2(mult#2(plus(), x2, x1), x1)) 9: mult#2(plus(), x1, x2) -> mult_n#1(plus(), x1, x2) 10: plus_n#1(x2, 0()) -> x2 11: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 13: plus#2(x2, x3) -> plus_n#1(x2, x3) 14: main(x1) -> map#2(f(mult(plus())), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat f#1 :: (nat -> nat -> nat) -> nat -> nat main :: nat list -> nat list map#2 :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_n#1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_n#1 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules WORST_CASE(?,O(n^4)) + Considered Problem: 1: f#1(mult(plus()), x1) -> mult#2(plus(), x1, mult#2(plus(), x1, x1)) 2: map_f#1(f(mult(plus())), Nil()) -> Nil() 3: map_f#1(f(mult(plus())), Cons(x2, x3)) -> Cons(mult#2(plus(), x2, mult#2(plus(), x2, x2)) , map#2(f(mult(plus())), x3)) 4: map#2(f(mult(plus())), Nil()) -> Nil() 5: map#2(f(mult(plus())), Cons(x4, x2)) -> Cons(f#1(mult(plus()), x4), map#2(f(mult(plus())), x2)) 6: mult_n#1(plus(), 0(), x1) -> 0() 7: mult_n#1(plus(), S(x2), x1) -> S(plus#2(mult#2(plus(), x2, x1), x1)) 8: mult#2(plus(), 0(), x2) -> 0() 9: mult#2(plus(), S(x4), x2) -> S(plus#2(mult#2(plus(), x4, x2), x2)) 10: plus_n#1(x2, 0()) -> x2 11: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 12: plus#2(x4, 0()) -> x4 13: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 14: main(x1) -> map#2(f(mult(plus())), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat f#1 :: (nat -> nat -> nat) -> nat -> nat main :: nat list -> nat list map#2 :: (nat -> nat) -> nat list -> nat list map_f#1 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_n#1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_n#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 15: Inline WORST_CASE(?,O(n^4)) + Considered Problem: 1: f#1(mult(plus()), x1) -> mult#2(plus(), x1, mult#2(plus(), x1, x1)) 4: map#2(f(mult(plus())), Nil()) -> Nil() 5: map#2(f(mult(plus())), Cons(x4, x2)) -> Cons(f#1(mult(plus()), x4), map#2(f(mult(plus())), x2)) 8: mult#2(plus(), 0(), x2) -> 0() 9: mult#2(plus(), S(x4), x2) -> S(plus#2(mult#2(plus(), x4, x2), x2)) 12: plus#2(x4, 0()) -> x4 13: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 14: main(x1) -> map#2(f(mult(plus())), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat f#1 :: (nat -> nat -> nat) -> nat -> nat main :: nat list -> nat list map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules WORST_CASE(?,O(n^4)) + Considered Problem: 1: f#1(mult(plus()), x1) -> mult#2(plus(), x1, mult#2(plus(), x1, x1)) 2: map#2(f(mult(plus())), Nil()) -> Nil() 3: map#2(f(mult(plus())), Cons(x2, x5)) -> Cons(mult#2(plus(), x2, mult#2(plus(), x2, x2)) , map#2(f(mult(plus())), x5)) 4: mult#2(plus(), 0(), x2) -> 0() 5: mult#2(plus(), S(x4), x2) -> S(plus#2(mult#2(plus(), x4, x2), x2)) 6: plus#2(x4, 0()) -> x4 7: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 8: main(x1) -> map#2(f(mult(plus())), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat f#1 :: (nat -> nat -> nat) -> nat -> nat main :: nat list -> nat list map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: Compression WORST_CASE(?,O(n^4)) + Considered Problem: 2: map#2(f(mult(plus())), Nil()) -> Nil() 3: map#2(f(mult(plus())), Cons(x2, x5)) -> Cons(mult#2(plus(), x2, mult#2(plus(), x2, x2)) , map#2(f(mult(plus())), x5)) 4: mult#2(plus(), 0(), x2) -> 0() 5: mult#2(plus(), S(x4), x2) -> S(plus#2(mult#2(plus(), x4, x2), x2)) 6: plus#2(x4, 0()) -> x4 7: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 8: main(x1) -> map#2(f(mult(plus())), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat f :: (nat -> nat -> nat) -> nat -> nat main :: nat list -> nat list map#2 :: (nat -> nat) -> nat list -> nat list mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Compression + Details: none * Step 18: ToTctProblem WORST_CASE(?,O(n^4)) + Considered Problem: 1: map#2(Nil()) -> Nil() 2: map#2(Cons(x2, x5)) -> Cons(mult#2(x2, mult#2(x2, x2)), map#2(x5)) 3: mult#2(0(), x2) -> 0() 4: mult#2(S(x4), x2) -> S(plus#2(mult#2(x4, x2), x2)) 5: plus#2(x4, 0()) -> x4 6: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 7: main(x1) -> map#2(x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat list -> nat list map#2 :: nat list -> nat list mult#2 :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: ToTctProblem + Details: none * Step 19: DependencyPairs WORST_CASE(?,O(n^4)) + Considered Problem: - Strict TRS: main(x1) -> map#2(x1) map#2(Cons(x2,x5)) -> Cons(mult#2(x2,mult#2(x2,x2)),map#2(x5)) map#2(Nil()) -> Nil() mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2} / {0/0,Cons/2,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) map#2#(Nil()) -> c_3() mult#2#(0(),x2) -> c_4() mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) plus#2#(x4,0()) -> c_6() plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) Weak DPs and mark the set of starting terms. * Step 20: UsableRules WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) map#2#(Nil()) -> c_3() mult#2#(0(),x2) -> c_4() mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) plus#2#(x4,0()) -> c_6() plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: main(x1) -> map#2(x1) map#2(Cons(x2,x5)) -> Cons(mult#2(x2,mult#2(x2,x2)),map#2(x5)) map#2(Nil()) -> Nil() mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) map#2#(Nil()) -> c_3() mult#2#(0(),x2) -> c_4() mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) plus#2#(x4,0()) -> c_6() plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) * Step 21: PredecessorEstimation WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) map#2#(Nil()) -> c_3() mult#2#(0(),x2) -> c_4() mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) plus#2#(x4,0()) -> c_6() plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,4,6} by application of Pre({3,4,6}) = {1,2,5,7}. Here rules are labelled as follows: 1: main#(x1) -> c_1(map#2#(x1)) 2: map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) 3: map#2#(Nil()) -> c_3() 4: mult#2#(0(),x2) -> c_4() 5: mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) 6: plus#2#(x4,0()) -> c_6() 7: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) * Step 22: RemoveWeakSuffixes WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: map#2#(Nil()) -> c_3() mult#2#(0(),x2) -> c_4() plus#2#(x4,0()) -> c_6() - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:main#(x1) -> c_1(map#2#(x1)) -->_1 map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)):2 -->_1 map#2#(Nil()) -> c_3():5 2:S:map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) -->_2 mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)):3 -->_1 mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)):3 -->_2 mult#2#(0(),x2) -> c_4():6 -->_1 mult#2#(0(),x2) -> c_4():6 -->_3 map#2#(Nil()) -> c_3():5 -->_3 map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)):2 3:S:mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):4 -->_1 plus#2#(x4,0()) -> c_6():7 -->_2 mult#2#(0(),x2) -> c_4():6 -->_2 mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)):3 4:S:plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) -->_1 plus#2#(x4,0()) -> c_6():7 -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):4 5:W:map#2#(Nil()) -> c_3() 6:W:mult#2#(0(),x2) -> c_4() 7:W:plus#2#(x4,0()) -> c_6() The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 5: map#2#(Nil()) -> c_3() 6: mult#2#(0(),x2) -> c_4() 7: plus#2#(x4,0()) -> c_6() * Step 23: DecomposeDG WORST_CASE(?,O(n^4)) + Considered Problem: - Strict DPs: main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) and a lower component mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) Further, following extension rules are added to the lower component. main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) ** Step 23.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: main#(x1) -> c_1(map#2#(x1)) 2: map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) The strictly oriented rules are moved into the weak component. *** Step 23.a:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_1) = {1}, uargs(c_2) = {1,3} Following symbols are considered usable: {mult#2,main#,map#2#} TcT has computed the following interpretation: p(0) = [12] p(Cons) = [1] x1 + [1] x2 + [3] p(Nil) = [0] p(S) = [2] p(main) = [2] x1 + [4] p(map#2) = [8] x1 + [1] p(mult#2) = [12] p(plus#2) = [1] x2 + [0] p(main#) = [8] x1 + [8] p(map#2#) = [8] x1 + [0] p(mult#2#) = [1] x2 + [2] p(plus#2#) = [2] x1 + [1] x2 + [0] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [4] x2 + [1] x3 + [0] p(c_3) = [8] p(c_4) = [0] p(c_5) = [8] x1 + [1] p(c_6) = [0] p(c_7) = [2] Following rules are strictly oriented: main#(x1) = [8] x1 + [8] > [8] x1 + [0] = c_1(map#2#(x1)) map#2#(Cons(x2,x5)) = [8] x2 + [8] x5 + [24] > [4] x2 + [8] x5 + [22] = c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) Following rules are (at-least) weakly oriented: mult#2(0(),x2) = [12] >= [12] = 0() mult#2(S(x4),x2) = [12] >= [2] = S(plus#2(mult#2(x4,x2),x2)) *** Step 23.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () *** Step 23.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: main#(x1) -> c_1(map#2#(x1)) map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:main#(x1) -> c_1(map#2#(x1)) -->_1 map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)):2 2:W:map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) -->_3 map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)):2 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: main#(x1) -> c_1(map#2#(x1)) 2: map#2#(Cons(x2,x5)) -> c_2(mult#2#(x2,mult#2(x2,x2)),mult#2#(x2,x2),map#2#(x5)) *** Step 23.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). ** Step 23.b:1: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Just someStrategy, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) and a lower component plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) Further, following extension rules are added to the lower component. main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) -> mult#2#(x4,x2) mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2) *** Step 23.b:1.a:1: PredecessorEstimationCP WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) Consider the set of all dependency pairs 1: mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) 2: main#(x1) -> map#2#(x1) 3: map#2#(Cons(x2,x5)) -> map#2#(x5) 4: map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) 5: map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) Processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^1)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,2} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 23.b:1.a:1.a:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(c_5) = {1,2} Following symbols are considered usable: {main#,map#2#,mult#2#} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [1] x1 + [1] x2 + [0] p(Nil) = [0] p(S) = [1] x1 + [8] p(main) = [1] x1 + [1] p(map#2) = [0] p(mult#2) = [12] x2 + [0] p(plus#2) = [0] p(main#) = [8] x1 + [11] p(map#2#) = [1] x1 + [10] p(mult#2#) = [1] x1 + [0] p(plus#2#) = [0] p(c_1) = [1] x1 + [1] p(c_2) = [1] x1 + [1] x3 + [1] p(c_3) = [0] p(c_4) = [1] p(c_5) = [1] x1 + [1] x2 + [7] p(c_6) = [0] p(c_7) = [0] Following rules are strictly oriented: mult#2#(S(x4),x2) = [1] x4 + [8] > [1] x4 + [7] = c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) Following rules are (at-least) weakly oriented: main#(x1) = [8] x1 + [11] >= [1] x1 + [10] = map#2#(x1) map#2#(Cons(x2,x5)) = [1] x2 + [1] x5 + [10] >= [1] x5 + [10] = map#2#(x5) map#2#(Cons(x2,x5)) = [1] x2 + [1] x5 + [10] >= [1] x2 + [0] = mult#2#(x2,x2) map#2#(Cons(x2,x5)) = [1] x2 + [1] x5 + [10] >= [1] x2 + [0] = mult#2#(x2,mult#2(x2,x2)) **** Step 23.b:1.a:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 23.b:1.a:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:main#(x1) -> map#2#(x1) -->_1 map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)):4 -->_1 map#2#(Cons(x2,x5)) -> mult#2#(x2,x2):3 -->_1 map#2#(Cons(x2,x5)) -> map#2#(x5):2 2:W:map#2#(Cons(x2,x5)) -> map#2#(x5) -->_1 map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)):4 -->_1 map#2#(Cons(x2,x5)) -> mult#2#(x2,x2):3 -->_1 map#2#(Cons(x2,x5)) -> map#2#(x5):2 3:W:map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) -->_1 mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)):5 4:W:map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) -->_1 mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)):5 5:W:mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) -->_2 mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)):5 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: main#(x1) -> map#2#(x1) 2: map#2#(Cons(x2,x5)) -> map#2#(x5) 3: map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) 4: map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) 5: mult#2#(S(x4),x2) -> c_5(plus#2#(mult#2(x4,x2),x2),mult#2#(x4,x2)) **** Step 23.b:1.a:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). *** Step 23.b:1.b:1: PredecessorEstimationCP WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) -> mult#2#(x4,x2) mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}} + Details: We first use the processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly: 1: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) Consider the set of all dependency pairs 1: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) 2: main#(x1) -> map#2#(x1) 3: map#2#(Cons(x2,x5)) -> map#2#(x5) 4: map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) 5: map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) 6: mult#2#(S(x4),x2) -> mult#2#(x4,x2) 7: mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2) Processor NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Nothing}induces the complexity certificateTIME (?,O(n^2)) SPACE(?,?)on application of the dependency pairs {1} These cover all (indirect) predecessors of dependency pairs {1,2} their number of applications is equally bounded. The dependency pairs are shifted into the weak component. **** Step 23.b:1.b:1.a:1: NaturalPI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) -> mult#2#(x4,x2) mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(mixed(2)): The following argument positions are considered usable: uargs(c_7) = {1} Following symbols are considered usable: {mult#2,plus#2,main#,map#2#,mult#2#,plus#2#} TcT has computed the following interpretation: p(0) = 0 p(Cons) = x1 + x2 p(Nil) = 1 p(S) = 1 + x1 p(main) = 4 + 4*x1 + x1^2 p(map#2) = 2 + x1 p(mult#2) = 2*x1 + x1*x2 + x1^2 p(plus#2) = 1 + x1 + x2 p(main#) = 5 + 6*x1 + 6*x1^2 p(map#2#) = 3 + 6*x1 + 5*x1^2 p(mult#2#) = 2*x1 + 2*x2 p(plus#2#) = 2 + 2*x2 p(c_1) = 4 + x1 p(c_2) = 0 p(c_3) = 1 p(c_4) = 1 p(c_5) = 2 + x1 + x2 p(c_6) = 4 p(c_7) = x1 Following rules are strictly oriented: plus#2#(x4,S(x2)) = 4 + 2*x2 > 2 + 2*x2 = c_7(plus#2#(x4,x2)) Following rules are (at-least) weakly oriented: main#(x1) = 5 + 6*x1 + 6*x1^2 >= 3 + 6*x1 + 5*x1^2 = map#2#(x1) map#2#(Cons(x2,x5)) = 3 + 6*x2 + 10*x2*x5 + 5*x2^2 + 6*x5 + 5*x5^2 >= 3 + 6*x5 + 5*x5^2 = map#2#(x5) map#2#(Cons(x2,x5)) = 3 + 6*x2 + 10*x2*x5 + 5*x2^2 + 6*x5 + 5*x5^2 >= 4*x2 = mult#2#(x2,x2) map#2#(Cons(x2,x5)) = 3 + 6*x2 + 10*x2*x5 + 5*x2^2 + 6*x5 + 5*x5^2 >= 6*x2 + 4*x2^2 = mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) = 2 + 2*x2 + 2*x4 >= 2*x2 + 2*x4 = mult#2#(x4,x2) mult#2#(S(x4),x2) = 2 + 2*x2 + 2*x4 >= 2 + 2*x2 = plus#2#(mult#2(x4,x2),x2) mult#2(0(),x2) = 0 >= 0 = 0() mult#2(S(x4),x2) = 3 + x2 + x2*x4 + 4*x4 + x4^2 >= 2 + x2 + x2*x4 + 2*x4 + x4^2 = S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) = 1 + x4 >= x4 = x4 plus#2(x4,S(x2)) = 2 + x2 + x4 >= 2 + x2 + x4 = S(plus#2(x4,x2)) **** Step 23.b:1.b:1.a:2: Assumption WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) -> mult#2#(x4,x2) mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown}} + Details: () **** Step 23.b:1.b:1.b:1: RemoveWeakSuffixes WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: main#(x1) -> map#2#(x1) map#2#(Cons(x2,x5)) -> map#2#(x5) map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) mult#2#(S(x4),x2) -> mult#2#(x4,x2) mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:W:main#(x1) -> map#2#(x1) -->_1 map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)):4 -->_1 map#2#(Cons(x2,x5)) -> mult#2#(x2,x2):3 -->_1 map#2#(Cons(x2,x5)) -> map#2#(x5):2 2:W:map#2#(Cons(x2,x5)) -> map#2#(x5) -->_1 map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)):4 -->_1 map#2#(Cons(x2,x5)) -> mult#2#(x2,x2):3 -->_1 map#2#(Cons(x2,x5)) -> map#2#(x5):2 3:W:map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) -->_1 mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2):6 -->_1 mult#2#(S(x4),x2) -> mult#2#(x4,x2):5 4:W:map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) -->_1 mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2):6 -->_1 mult#2#(S(x4),x2) -> mult#2#(x4,x2):5 5:W:mult#2#(S(x4),x2) -> mult#2#(x4,x2) -->_1 mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2):6 -->_1 mult#2#(S(x4),x2) -> mult#2#(x4,x2):5 6:W:mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2) -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):7 7:W:plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):7 The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed. 1: main#(x1) -> map#2#(x1) 2: map#2#(Cons(x2,x5)) -> map#2#(x5) 3: map#2#(Cons(x2,x5)) -> mult#2#(x2,x2) 4: map#2#(Cons(x2,x5)) -> mult#2#(x2,mult#2(x2,x2)) 5: mult#2#(S(x4),x2) -> mult#2#(x4,x2) 6: mult#2#(S(x4),x2) -> plus#2#(mult#2(x4,x2),x2) 7: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) **** Step 23.b:1.b:1.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {main/1,map#2/1,mult#2/2,plus#2/2,main#/1,map#2#/1,mult#2#/2,plus#2#/2} / {0/0,Cons/2,Nil/0,S/1,c_1/1,c_2/3 ,c_3/0,c_4/0,c_5/2,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Cons,Nil,S} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^4))