WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: type nat = 0 | S of nat ;; let rec iter f g x = match x with | 0 -> g | S(x') -> f (iter f g x') ;; let compS f z = f (S(z)) ;; let id y = y ;; let iterid n = iter compS id n 0 ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: Ī»n : nat. (Ī»iter : ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat. (Ī»compS : (nat -> nat) -> nat -> nat. (Ī»id : nat -> nat. (Ī»iterid : nat -> nat. iterid n) (Ī»n : nat. iter compS id n 0)) (Ī»y : nat. y)) (Ī»f : nat -> nat. Ī»z : nat. f S(z))) (Ī¼iter : ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat. Ī»f : (nat -> nat) -> nat -> nat. Ī»g : nat -> nat. Ī»x : nat. case x of | 0 -> g | S -> Ī»x' : nat. f (iter f g x')) : nat -> nat where 0 :: nat S :: nat -> nat + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: iterid(x1, x2, x3) x4 -> x1 x2 x3 x4 0() 3: main_3(x0, x1, x2) x3 -> main_4(x0) iterid(x1, x2, x3) 4: id() x3 -> x3 5: main_2(x0, x1) x2 -> main_3(x0, x1, x2) id() 6: compS_f(x2) x3 -> x2 S(x3) 7: compS() x2 -> compS_f(x2) 8: main_1(x0) x1 -> main_2(x0, x1) compS() 9: cond_iter_f_g_x(0(), x1, x2) -> x2 10: cond_iter_f_g_x(S(x4), x1, x2) -> x1 (iter() x1 x2 x4) 11: iter_f_g(x1, x2) x3 -> cond_iter_f_g_x(x3, x1, x2) 12: iter_f(x1) x2 -> iter_f_g(x1, x2) 13: iter_1() x1 -> iter_f(x1) 14: iter() x0 -> iter_1() x0 15: main(x0) -> main_1(x0) iter() where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iterid :: (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter_1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main_1 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> nat main_2 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> nat main_3 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat) -> nat cond_iter_f_g_x :: nat -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: iterid(x1, x2, x3) x4 -> x1 x2 x3 x4 0() 3: main_3(x0, x3, x5) x7 -> iterid(x3, x5, x7) x0 4: id() x3 -> x3 5: main_2(x0, x2) x4 -> main_4(x0) iterid(x2, x4, id()) 6: compS_f(x2) x3 -> x2 S(x3) 7: compS() x2 -> compS_f(x2) 8: main_1(x0) x2 -> main_3(x0, x2, compS()) id() 9: cond_iter_f_g_x(0(), x1, x2) -> x2 10: cond_iter_f_g_x(S(x4), x1, x2) -> x1 (iter() x1 x2 x4) 11: iter_f_g(x1, x2) x3 -> cond_iter_f_g_x(x3, x1, x2) 12: iter_f(x1) x2 -> iter_f_g(x1, x2) 13: iter_1() x1 -> iter_f(x1) 14: iter() x2 -> iter_f(x2) 15: main(x0) -> main_2(x0, iter()) compS() where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iterid :: (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter_1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main_1 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> nat main_2 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> nat main_3 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat) -> nat cond_iter_f_g_x :: nat -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: iterid(x1, x2, x3) x4 -> x1 x2 x3 x4 0() 3: main_3(x8, x2, x4) x6 -> x2 x4 x6 x8 0() 4: id() x3 -> x3 5: main_2(x0, x5) x9 -> iterid(x5, x9, id()) x0 6: compS_f(x2) x3 -> x2 S(x3) 7: compS() x2 -> compS_f(x2) 8: main_1(x0) x6 -> iterid(x6, compS(), id()) x0 9: cond_iter_f_g_x(0(), x1, x2) -> x2 10: cond_iter_f_g_x(S(x4), x1, x2) -> x1 (iter() x1 x2 x4) 11: iter_f_g(x1, x2) x3 -> cond_iter_f_g_x(x3, x1, x2) 12: iter_f(x1) x2 -> iter_f_g(x1, x2) 13: iter_1() x1 -> iter_f(x1) 14: iter() x2 -> iter_f(x2) 15: main(x0) -> main_4(x0) iterid(iter(), compS(), id()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iterid :: (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter_1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main_1 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> nat main_2 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> nat main_3 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat) -> nat cond_iter_f_g_x :: nat -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: iterid(x1, x2, x3) x4 -> x1 x2 x3 x4 0() 3: main_3(x8, x2, x4) x6 -> x2 x4 x6 x8 0() 4: id() x3 -> x3 5: main_2(x8, x2) x4 -> x2 x4 id() x8 0() 6: compS_f(x2) x3 -> x2 S(x3) 7: compS() x2 -> compS_f(x2) 8: main_1(x8) x2 -> x2 compS() id() x8 0() 9: cond_iter_f_g_x(0(), x1, x2) -> x2 10: cond_iter_f_g_x(S(x4), x1, x2) -> x1 (iter() x1 x2 x4) 11: iter_f_g(x1, x2) x3 -> cond_iter_f_g_x(x3, x1, x2) 12: iter_f(x1) x2 -> iter_f_g(x1, x2) 13: iter_1() x1 -> iter_f(x1) 14: iter() x2 -> iter_f(x2) 15: main(x0) -> iterid(iter(), compS(), id()) x0 where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iterid :: (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter_1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main_1 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> nat main_2 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> nat main_3 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat) -> nat cond_iter_f_g_x :: nat -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: iterid(x1, x2, x3) x4 -> x1 x2 x3 x4 0() 3: main_3(x8, x2, x4) x6 -> x2 x4 x6 x8 0() 4: id() x3 -> x3 5: main_2(x8, x2) x4 -> x2 x4 id() x8 0() 6: compS_f(x2) x3 -> x2 S(x3) 7: compS() x2 -> compS_f(x2) 8: main_1(x8) x2 -> x2 compS() id() x8 0() 9: cond_iter_f_g_x(0(), x1, x2) -> x2 10: cond_iter_f_g_x(S(x4), x1, x2) -> x1 (iter() x1 x2 x4) 11: iter_f_g(x1, x2) x3 -> cond_iter_f_g_x(x3, x1, x2) 12: iter_f(x1) x2 -> iter_f_g(x1, x2) 13: iter_1() x1 -> iter_f(x1) 14: iter() x2 -> iter_f(x2) 15: main(x8) -> iter() compS() id() x8 0() where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iterid :: (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter_1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main_1 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> nat main_2 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> nat main_3 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat) -> nat cond_iter_f_g_x :: nat -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: iterid(x1, x2, x3) x4 -> x1 x2 x3 x4 0() 3: main_3(x8, x2, x4) x6 -> x2 x4 x6 x8 0() 4: id() x3 -> x3 5: main_2(x8, x2) x4 -> x2 x4 id() x8 0() 6: compS_f(x2) x3 -> x2 S(x3) 7: compS() x2 -> compS_f(x2) 8: main_1(x8) x2 -> x2 compS() id() x8 0() 9: cond_iter_f_g_x(0(), x1, x2) -> x2 10: cond_iter_f_g_x(S(x4), x1, x2) -> x1 (iter() x1 x2 x4) 11: iter_f_g(x2, x4) 0() -> x4 12: iter_f_g(x2, x4) S(x8) -> x2 (iter() x2 x4 x8) 13: iter_f(x1) x2 -> iter_f_g(x1, x2) 14: iter_1() x1 -> iter_f(x1) 15: iter() x2 -> iter_f(x2) 16: main(x8) -> iter() compS() id() x8 0() where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iterid :: (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter_1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main_1 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> nat main_2 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> nat main_3 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat) -> nat cond_iter_f_g_x :: nat -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: iterid(x1, x2, x3) x4 -> x1 x2 x3 x4 0() 3: main_3(x8, x2, x4) x6 -> x2 x4 x6 x8 0() 4: id() x3 -> x3 5: main_2(x8, x2) x4 -> x2 x4 id() x8 0() 6: compS_f(x2) x3 -> x2 S(x3) 7: compS() x2 -> compS_f(x2) 8: main_1(x8) x2 -> x2 compS() id() x8 0() 11: iter_f_g(x2, x4) 0() -> x4 12: iter_f_g(x2, x4) S(x8) -> x2 (iter() x2 x4 x8) 13: iter_f(x1) x2 -> iter_f_g(x1, x2) 14: iter_1() x1 -> iter_f(x1) 15: iter() x2 -> iter_f(x2) 16: main(x8) -> iter() compS() id() x8 0() where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iterid :: (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter_1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main_1 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> nat main_2 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> nat main_3 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat) -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: iterid(x1, x2, x3) x4 -> x1 x2 x3 x4 0() 3: main_3(x8, x2, x4) x6 -> x2 x4 x6 x8 0() 4: id() x3 -> x3 5: main_2(x8, x2) x4 -> x2 x4 id() x8 0() 6: compS_f(x2) x3 -> x2 S(x3) 7: compS() x2 -> compS_f(x2) 8: main_1(x8) x2 -> x2 compS() id() x8 0() 9: iter_f_g(x2, x4) 0() -> x4 10: iter_f_g(x2, x4) S(x8) -> x2 (iter() x2 x4 x8) 11: iter_f(x1) x2 -> iter_f_g(x1, x2) 12: iter_1() x1 -> iter_f(x1) 13: iter() x2 -> iter_f(x2) 14: main(x8) -> iter() compS() id() x8 0() where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iterid :: (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat iter_1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main_1 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> nat main_2 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> nat main_3 :: nat -> (((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat) -> ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat main_4 :: nat -> (nat -> nat) -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> 0() | S(X{*}) | 0() | 0() | S(X{*}) | 0() | 0() | 0() ,V{x1_11} -> V{x2_13} ,V{x2_6} -> V{x2_7} ,V{x2_7} -> R{10} | R{9} ,V{x2_9} -> V{x1_11} ,V{x2_10} -> V{x1_11} ,V{x2_11} -> V{x4_10} | id() ,V{x2_13} -> V{x2_10} | compS() ,V{x3_4} -> S(V{x3_6}) | 0() ,V{x3_6} -> S(V{x3_6}) | 0() ,V{x4_9} -> V{x2_11} ,V{x4_10} -> V{x2_11} ,V{x8_10} -> X{*} ,V{x8_14} -> X{*} ,R{0} -> R{14} | main(X{*}) ,R{4} -> V{x3_4} ,R{6} -> R{6} | R{4} | @(V{x2_6},S(V{x3_6})) ,R{7} -> compS_f(V{x2_7}) ,R{9} -> V{x4_9} ,R{10} -> R{7} | @(V{x2_10},R{10}) | @(V{x2_10},R{9}) | @(V{x2_10},@(R{11},V{x8_10})) | @(V{x2_10},@(@(R{13},V{x4_10}),V{x8_10})) | @(V{x2_10},@(@(@(iter(),V{x2_10}),V{x4_10}),V{x8_10})) ,R{11} -> iter_f_g(V{x1_11},V{x2_11}) ,R{13} -> iter_f(V{x2_13}) ,R{14} -> R{6} | R{4} | @(R{10},0()) | @(R{9},0()) | @(@(R{11},V{x8_14}),0()) | @(@(@(R{13},id()),V{x8_14}),0()) | @(@(@(@(iter(),compS()),id()),V{x8_14}),0())} * Step 11: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 4: id() x3 -> x3 6: compS_f(compS_f(x2)) x1 -> compS_f(x2) S(x1) 7: compS_f(id()) x1 -> id() S(x1) 8: compS() x2 -> compS_f(x2) 10: iter_f_g(compS(), id()) 0() -> id() 11: iter_f_g(compS(), id()) S(x1) -> compS() (iter() compS() id() x1) 12: iter_f(compS()) id() -> iter_f_g(compS(), id()) 14: iter() compS() -> iter_f(compS()) 15: main(x1) -> iter() compS() id() x1 0() where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat id :: nat -> nat iter :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: UncurryATRS + Details: none * Step 12: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: id#1(x3) -> x3 2: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 3: compS_f#1(id(), x1) -> id#1(S(x1)) 4: compS#1(x2) -> compS_f(x2) 5: compS#2(x2, x3) -> compS_f#1(x2, x3) 6: iter_f_g#1(compS(), id(), 0()) -> id() 7: iter_f_g#2(compS(), id(), 0(), x0) -> id#1(x0) 8: iter_f_g#1(compS(), id(), S(x1)) -> compS#1(iter#3(compS(), id(), x1)) 9: iter_f_g#2(compS(), id(), S(x1), x2) -> compS#2(iter#3(compS(), id(), x1), x2) 10: iter_f#1(compS(), id()) -> iter_f_g(compS(), id()) 11: iter_f#2(compS(), id(), x0) -> iter_f_g#1(compS(), id(), x0) 12: iter_f#3(compS(), id(), x0, x1) -> iter_f_g#2(compS(), id(), x0, x1) 13: iter#1(compS()) -> iter_f(compS()) 14: iter#2(compS(), x0) -> iter_f#1(compS(), x0) 15: iter#3(compS(), x0, x1) -> iter_f#2(compS(), x0, x1) 16: iter#4(compS(), x0, x1, x2) -> iter_f#3(compS(), x0, x1, x2) 17: main(x1) -> iter#4(compS(), id(), x1, 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS#1 :: (nat -> nat) -> nat -> nat compS#2 :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat id#1 :: nat -> nat iter#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter#4 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 13: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: id#1(x3) -> x3 2: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 3: compS_f#1(id(), x3) -> S(x3) 4: compS#1(x2) -> compS_f(x2) 5: compS#2(x2, x3) -> compS_f#1(x2, x3) 6: iter_f_g#1(compS(), id(), 0()) -> id() 7: iter_f_g#2(compS(), id(), 0(), x6) -> x6 8: iter_f_g#1(compS(), id(), S(x1)) -> compS#1(iter#3(compS(), id(), x1)) 9: iter_f_g#2(compS(), id(), S(x1), x2) -> compS#2(iter#3(compS(), id(), x1), x2) 10: iter_f#1(compS(), id()) -> iter_f_g(compS(), id()) 11: iter_f#2(compS(), id(), x0) -> iter_f_g#1(compS(), id(), x0) 12: iter_f#3(compS(), id(), x0, x1) -> iter_f_g#2(compS(), id(), x0, x1) 13: iter#1(compS()) -> iter_f(compS()) 14: iter#2(compS(), x0) -> iter_f#1(compS(), x0) 15: iter#3(compS(), x0, x1) -> iter_f#2(compS(), x0, x1) 16: iter#4(compS(), x0, x1, x2) -> iter_f#3(compS(), x0, x1, x2) 17: main(x1) -> iter#4(compS(), id(), x1, 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS#1 :: (nat -> nat) -> nat -> nat compS#2 :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat id#1 :: nat -> nat iter#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter#4 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 14: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 2: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 3: compS_f#1(id(), x3) -> S(x3) 4: compS#1(x2) -> compS_f(x2) 5: compS#2(x2, x3) -> compS_f#1(x2, x3) 6: iter_f_g#1(compS(), id(), 0()) -> id() 7: iter_f_g#2(compS(), id(), 0(), x6) -> x6 8: iter_f_g#1(compS(), id(), S(x1)) -> compS#1(iter#3(compS(), id(), x1)) 9: iter_f_g#2(compS(), id(), S(x1), x2) -> compS#2(iter#3(compS(), id(), x1), x2) 11: iter_f#2(compS(), id(), x0) -> iter_f_g#1(compS(), id(), x0) 12: iter_f#3(compS(), id(), x0, x1) -> iter_f_g#2(compS(), id(), x0, x1) 15: iter#3(compS(), x0, x1) -> iter_f#2(compS(), x0, x1) 16: iter#4(compS(), x0, x1, x2) -> iter_f#3(compS(), x0, x1, x2) 17: main(x1) -> iter#4(compS(), id(), x1, 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS#1 :: (nat -> nat) -> nat -> nat compS#2 :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter#4 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 2: compS_f#1(id(), x3) -> S(x3) 3: compS#1(x2) -> compS_f(x2) 4: compS#2(x2, x3) -> compS_f#1(x2, x3) 5: iter_f_g#1(compS(), id(), 0()) -> id() 6: iter_f_g#2(compS(), id(), 0(), x6) -> x6 7: iter_f_g#1(compS(), id(), S(x3)) -> compS_f(iter#3(compS(), id(), x3)) 8: iter_f_g#2(compS(), id(), S(x3), x6) -> compS_f#1(iter#3(compS(), id(), x3), x6) 9: iter_f#2(compS(), id(), 0()) -> id() 10: iter_f#2(compS(), id(), S(x2)) -> compS#1(iter#3(compS(), id(), x2)) 11: iter_f#3(compS(), id(), 0(), x12) -> x12 12: iter_f#3(compS(), id(), S(x2), x4) -> compS#2(iter#3(compS(), id(), x2), x4) 13: iter#3(compS(), id(), x0) -> iter_f_g#1(compS(), id(), x0) 14: iter#4(compS(), id(), x0, x2) -> iter_f_g#2(compS(), id(), x0, x2) 15: main(x2) -> iter_f#3(compS(), id(), x2, 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS#1 :: (nat -> nat) -> nat -> nat compS#2 :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter#4 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#2 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 2: compS_f#1(id(), x3) -> S(x3) 4: compS#2(x2, x3) -> compS_f#1(x2, x3) 5: iter_f_g#1(compS(), id(), 0()) -> id() 7: iter_f_g#1(compS(), id(), S(x3)) -> compS_f(iter#3(compS(), id(), x3)) 11: iter_f#3(compS(), id(), 0(), x12) -> x12 12: iter_f#3(compS(), id(), S(x2), x4) -> compS#2(iter#3(compS(), id(), x2), x4) 13: iter#3(compS(), id(), x0) -> iter_f_g#1(compS(), id(), x0) 15: main(x2) -> iter_f#3(compS(), id(), x2, 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS#2 :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 17: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 2: compS_f#1(id(), x3) -> S(x3) 3: compS#2(x2, x3) -> compS_f#1(x2, x3) 4: iter_f_g#1(compS(), id(), 0()) -> id() 5: iter_f_g#1(compS(), id(), S(x3)) -> compS_f(iter#3(compS(), id(), x3)) 6: iter_f#3(compS(), id(), 0(), x12) -> x12 7: iter_f#3(compS(), id(), S(x5), x6) -> compS_f#1(iter#3(compS(), id(), x5), x6) 8: iter#3(compS(), id(), 0()) -> id() 9: iter#3(compS(), id(), S(x6)) -> compS_f(iter#3(compS(), id(), x6)) 10: main(0()) -> 0() 11: main(S(x4)) -> compS#2(iter#3(compS(), id(), x4), 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS#2 :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat iter_f_g#1 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 18: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 2: compS_f#1(id(), x3) -> S(x3) 3: compS#2(x2, x3) -> compS_f#1(x2, x3) 8: iter#3(compS(), id(), 0()) -> id() 9: iter#3(compS(), id(), S(x6)) -> compS_f(iter#3(compS(), id(), x6)) 10: main(0()) -> 0() 11: main(S(x4)) -> compS#2(iter#3(compS(), id(), x4), 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS#2 :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 19: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 2: compS_f#1(id(), x3) -> S(x3) 3: compS#2(x2, x3) -> compS_f#1(x2, x3) 4: iter#3(compS(), id(), 0()) -> id() 5: iter#3(compS(), id(), S(x6)) -> compS_f(iter#3(compS(), id(), x6)) 6: main(0()) -> 0() 7: main(S(x9)) -> compS_f#1(iter#3(compS(), id(), x9), 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS#2 :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 20: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 1: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 2: compS_f#1(id(), x3) -> S(x3) 4: iter#3(compS(), id(), 0()) -> id() 5: iter#3(compS(), id(), S(x6)) -> compS_f(iter#3(compS(), id(), x6)) 6: main(0()) -> 0() 7: main(S(x9)) -> compS_f#1(iter#3(compS(), id(), x9), 0()) where 0 :: nat S :: nat -> nat compS :: (nat -> nat) -> nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat iter#3 :: ((nat -> nat) -> nat -> nat) -> (nat -> nat) -> nat -> nat -> nat main :: nat -> nat + Applied Processor: Compression + Details: none * Step 21: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: compS_f#1(compS_f(x2), x1) -> compS_f#1(x2, S(x1)) 2: compS_f#1(id(), x3) -> S(x3) 3: iter#3(0()) -> id() 4: iter#3(S(x6)) -> compS_f(iter#3(x6)) 5: main(0()) -> 0() 6: main(S(x9)) -> compS_f#1(iter#3(x9), 0()) where 0 :: nat S :: nat -> nat compS_f :: (nat -> nat) -> nat -> nat compS_f#1 :: (nat -> nat) -> nat -> nat id :: nat -> nat iter#3 :: nat -> nat -> nat main :: nat -> nat + Applied Processor: ToTctProblem + Details: none * Step 22: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: compS_f#1(compS_f(x2),x1) -> compS_f#1(x2,S(x1)) compS_f#1(id(),x3) -> S(x3) iter#3(0()) -> id() iter#3(S(x6)) -> compS_f(iter#3(x6)) main(0()) -> 0() main(S(x9)) -> compS_f#1(iter#3(x9),0()) - Signature: {compS_f#1/2,iter#3/1,main/1} / {0/0,S/1,compS_f/1,id/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,S} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: uargs(compS_f) = {1}, uargs(compS_f#1) = {1} Following symbols are considered usable: {compS_f#1,iter#3,main} TcT has computed the following interpretation: p(0) = [1] p(S) = [1] x1 + [1] p(compS_f) = [1] x1 + [10] p(compS_f#1) = [1] x1 + [4] x2 + [10] p(id) = [0] p(iter#3) = [10] x1 + [0] p(main) = [15] x1 + [13] Following rules are strictly oriented: compS_f#1(compS_f(x2),x1) = [4] x1 + [1] x2 + [20] > [4] x1 + [1] x2 + [14] = compS_f#1(x2,S(x1)) compS_f#1(id(),x3) = [4] x3 + [10] > [1] x3 + [1] = S(x3) iter#3(0()) = [10] > [0] = id() main(0()) = [28] > [1] = 0() main(S(x9)) = [15] x9 + [28] > [10] x9 + [14] = compS_f#1(iter#3(x9),0()) Following rules are (at-least) weakly oriented: iter#3(S(x6)) = [10] x6 + [10] >= [10] x6 + [10] = compS_f(iter#3(x6)) * Step 23: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: iter#3(S(x6)) -> compS_f(iter#3(x6)) - Weak TRS: compS_f#1(compS_f(x2),x1) -> compS_f#1(x2,S(x1)) compS_f#1(id(),x3) -> S(x3) iter#3(0()) -> id() main(0()) -> 0() main(S(x9)) -> compS_f#1(iter#3(x9),0()) - Signature: {compS_f#1/2,iter#3/1,main/1} / {0/0,S/1,compS_f/1,id/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,S} + 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(compS_f) = {1}, uargs(compS_f#1) = {1} Following symbols are considered usable: {compS_f#1,iter#3,main} TcT has computed the following interpretation: p(0) = 0 p(S) = 3 + x1 p(compS_f) = 8 + x1 p(compS_f#1) = x1 + 2*x2 p(id) = 3 p(iter#3) = 6 + 6*x1 p(main) = 4 + 8*x1 Following rules are strictly oriented: iter#3(S(x6)) = 24 + 6*x6 > 14 + 6*x6 = compS_f(iter#3(x6)) Following rules are (at-least) weakly oriented: compS_f#1(compS_f(x2),x1) = 8 + 2*x1 + x2 >= 6 + 2*x1 + x2 = compS_f#1(x2,S(x1)) compS_f#1(id(),x3) = 3 + 2*x3 >= 3 + x3 = S(x3) iter#3(0()) = 6 >= 3 = id() main(0()) = 4 >= 0 = 0() main(S(x9)) = 28 + 8*x9 >= 6 + 6*x9 = compS_f#1(iter#3(x9),0()) * Step 24: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: compS_f#1(compS_f(x2),x1) -> compS_f#1(x2,S(x1)) compS_f#1(id(),x3) -> S(x3) iter#3(0()) -> id() iter#3(S(x6)) -> compS_f(iter#3(x6)) main(0()) -> 0() main(S(x9)) -> compS_f#1(iter#3(x9),0()) - Signature: {compS_f#1/2,iter#3/1,main/1} / {0/0,S/1,compS_f/1,id/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,S} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))