WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: type 'a list = Nil | Cons of 'a * 'a list ;; type Unit = Unit ;; type 'a lazy_list = NilL | ConsL of 'a * (Unit -> 'a lazy_list) ;; type nat = 0 | S of nat ;; let rec take_l n xs = match force xs with | NilL -> Nil | ConsL(x,xs') -> match n with | 0 -> Nil | S(n') -> Cons(x,take_l n' xs') ;; let rec zeros = lazy ConsL(0, zeros) ;; let take_lazy n = take_l n zeros ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λn : nat. (λtake_l : nat -> (Unit -> nat lazy_list) -> nat list. (λzeros : Unit -> nat lazy_list. (λtake_lazy : nat -> nat list. take_lazy n) (λn : nat. take_l n zeros)) (μzeros : Unit -> nat lazy_list. λ0 : Unit. ConsL(0,zeros))) (μtake_l : nat -> (Unit -> nat lazy_list) -> nat list. λn : nat. λxs : Unit -> nat lazy_list. case xs ⟘  of | NilL -> Nil | ConsL -> λx : nat. λxs' : Unit -> nat lazy_list. case n of | 0 -> Nil | S -> λn' : nat. Cons(x,take_l n' xs')) : nat -> nat list where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list NilL :: 'a lazy_list S :: nat -> nat Unit :: Unit + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: take_lazy(x1, x2) x3 -> x1 x3 x2 3: main_2(x0, x1) x2 -> main_3(x0) take_lazy(x1, x2) 4: zeros_1() x2 -> ConsL(0(), zeros()) 5: zeros() x0 -> zeros_1() x0 6: main_1(x0) x1 -> main_2(x0, x1) zeros() 7: cond_take_l_n_xs_1(0(), x3, x4) -> Nil() 8: cond_take_l_n_xs_1(S(x5), x3, x4) -> Cons(x3, take_l() x5 x4) 9: cond_take_l_n_xs(NilL(), x1) -> Nil() 10: cond_take_l_n_xs(ConsL(x3, x4), x1) -> cond_take_l_n_xs_1(x1, x3, x4) 11: take_l_n(x1) x2 -> cond_take_l_n_xs(x2 bot[0](), x1) 12: take_l_1() x1 -> take_l_n(x1) 13: take_l() x0 -> take_l_1() x0 14: main(x0) -> main_1(x0) take_l() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list NilL :: 'a lazy_list S :: nat -> nat take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list take_lazy :: (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat -> nat list main_1 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> nat list take_l_1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros_1 :: Unit -> nat lazy_list main_2 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat list main_3 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat lazy_list) -> nat list take_l :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: take_lazy(x1, x2) x3 -> x1 x3 x2 3: main_2(x0, x3) x5 -> take_lazy(x3, x5) x0 4: zeros_1() x2 -> ConsL(0(), zeros()) 5: zeros() x4 -> ConsL(0(), zeros()) 6: main_1(x0) x2 -> main_3(x0) take_lazy(x2, zeros()) 7: cond_take_l_n_xs_1(0(), x3, x4) -> Nil() 8: cond_take_l_n_xs_1(S(x5), x3, x4) -> Cons(x3, take_l() x5 x4) 9: cond_take_l_n_xs(NilL(), x1) -> Nil() 10: cond_take_l_n_xs(ConsL(x3, x4), x1) -> cond_take_l_n_xs_1(x1, x3, x4) 11: take_l_n(x1) x2 -> cond_take_l_n_xs(x2 bot[0](), x1) 12: take_l_1() x1 -> take_l_n(x1) 13: take_l() x2 -> take_l_n(x2) 14: main(x0) -> main_2(x0, take_l()) zeros() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list NilL :: 'a lazy_list S :: nat -> nat take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list take_lazy :: (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat -> nat list main_1 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> nat list take_l_1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros_1 :: Unit -> nat lazy_list main_2 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat list main_3 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat lazy_list) -> nat list take_l :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: take_lazy(x1, x2) x3 -> x1 x3 x2 3: main_2(x6, x2) x4 -> x2 x6 x4 4: zeros_1() x2 -> ConsL(0(), zeros()) 5: zeros() x4 -> ConsL(0(), zeros()) 6: main_1(x0) x5 -> take_lazy(x5, zeros()) x0 7: cond_take_l_n_xs_1(0(), x3, x4) -> Nil() 8: cond_take_l_n_xs_1(S(x5), x3, x4) -> Cons(x3, take_l() x5 x4) 9: cond_take_l_n_xs(NilL(), x1) -> Nil() 10: cond_take_l_n_xs(ConsL(x3, x4), x1) -> cond_take_l_n_xs_1(x1, x3, x4) 11: take_l_n(x1) x2 -> cond_take_l_n_xs(x2 bot[0](), x1) 12: take_l_1() x1 -> take_l_n(x1) 13: take_l() x2 -> take_l_n(x2) 14: main(x0) -> take_lazy(take_l(), zeros()) x0 where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list NilL :: 'a lazy_list S :: nat -> nat take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list take_lazy :: (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat -> nat list main_1 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> nat list take_l_1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros_1 :: Unit -> nat lazy_list main_2 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat list main_3 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat lazy_list) -> nat list take_l :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: take_lazy(x1, x2) x3 -> x1 x3 x2 3: main_2(x6, x2) x4 -> x2 x6 x4 4: zeros_1() x2 -> ConsL(0(), zeros()) 5: zeros() x4 -> ConsL(0(), zeros()) 6: main_1(x6) x2 -> x2 x6 zeros() 7: cond_take_l_n_xs_1(0(), x3, x4) -> Nil() 8: cond_take_l_n_xs_1(S(x5), x3, x4) -> Cons(x3, take_l() x5 x4) 9: cond_take_l_n_xs(NilL(), x1) -> Nil() 10: cond_take_l_n_xs(ConsL(x3, x4), x1) -> cond_take_l_n_xs_1(x1, x3, x4) 11: take_l_n(x1) x2 -> cond_take_l_n_xs(x2 bot[0](), x1) 12: take_l_1() x1 -> take_l_n(x1) 13: take_l() x2 -> take_l_n(x2) 14: main(x6) -> take_l() x6 zeros() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list NilL :: 'a lazy_list S :: nat -> nat take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list take_lazy :: (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat -> nat list main_1 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> nat list take_l_1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros_1 :: Unit -> nat lazy_list main_2 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat list main_3 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat lazy_list) -> nat list take_l :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list main :: nat -> nat list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 7: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: take_lazy(x1, x2) x3 -> x1 x3 x2 3: main_2(x6, x2) x4 -> x2 x6 x4 4: zeros_1() x2 -> ConsL(0(), zeros()) 5: zeros() x4 -> ConsL(0(), zeros()) 6: main_1(x6) x2 -> x2 x6 zeros() 7: cond_take_l_n_xs_1(0(), x3, x4) -> Nil() 8: cond_take_l_n_xs_1(S(x5), x3, x4) -> Cons(x3, take_l() x5 x4) 9: cond_take_l_n_xs(NilL(), x1) -> Nil() 10: cond_take_l_n_xs(ConsL(x6, x8), 0()) -> Nil() 11: cond_take_l_n_xs(ConsL(x6, x8), S(x10)) -> Cons(x6, take_l() x10 x8) 12: take_l_n(x1) x2 -> cond_take_l_n_xs(x2 bot[0](), x1) 13: take_l_1() x1 -> take_l_n(x1) 14: take_l() x2 -> take_l_n(x2) 15: main(x6) -> take_l() x6 zeros() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list NilL :: 'a lazy_list S :: nat -> nat take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list take_lazy :: (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat -> nat list main_1 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> nat list take_l_1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros_1 :: Unit -> nat lazy_list main_2 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat list main_3 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list cond_take_l_n_xs_1 :: nat -> nat -> (Unit -> nat lazy_list) -> nat list take_l :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list main :: nat -> nat list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 8: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: take_lazy(x1, x2) x3 -> x1 x3 x2 3: main_2(x6, x2) x4 -> x2 x6 x4 4: zeros_1() x2 -> ConsL(0(), zeros()) 5: zeros() x4 -> ConsL(0(), zeros()) 6: main_1(x6) x2 -> x2 x6 zeros() 9: cond_take_l_n_xs(NilL(), x1) -> Nil() 10: cond_take_l_n_xs(ConsL(x6, x8), 0()) -> Nil() 11: cond_take_l_n_xs(ConsL(x6, x8), S(x10)) -> Cons(x6, take_l() x10 x8) 12: take_l_n(x1) x2 -> cond_take_l_n_xs(x2 bot[0](), x1) 13: take_l_1() x1 -> take_l_n(x1) 14: take_l() x2 -> take_l_n(x2) 15: main(x6) -> take_l() x6 zeros() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list NilL :: 'a lazy_list S :: nat -> nat take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list take_lazy :: (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat -> nat list main_1 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> nat list take_l_1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros_1 :: Unit -> nat lazy_list main_2 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat list main_3 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list take_l :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list main :: nat -> nat list + Applied Processor: NeededRules + Details: none * Step 9: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: take_lazy(x1, x2) x3 -> x1 x3 x2 3: main_2(x6, x2) x4 -> x2 x6 x4 4: zeros_1() x2 -> ConsL(0(), zeros()) 5: zeros() x4 -> ConsL(0(), zeros()) 6: main_1(x6) x2 -> x2 x6 zeros() 7: cond_take_l_n_xs(NilL(), x1) -> Nil() 8: cond_take_l_n_xs(ConsL(x6, x8), 0()) -> Nil() 9: cond_take_l_n_xs(ConsL(x6, x8), S(x10)) -> Cons(x6, take_l() x10 x8) 10: take_l_n(x1) x2 -> cond_take_l_n_xs(x2 bot[0](), x1) 11: take_l_1() x1 -> take_l_n(x1) 12: take_l() x2 -> take_l_n(x2) 13: main(x6) -> take_l() x6 zeros() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list NilL :: 'a lazy_list S :: nat -> nat take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list take_lazy :: (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat -> nat list main_1 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> nat list take_l_1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros_1 :: Unit -> nat lazy_list main_2 :: nat -> (nat -> (Unit -> nat lazy_list) -> nat list) -> (Unit -> nat lazy_list) -> nat list main_3 :: nat -> (nat -> nat list) -> nat list bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list take_l :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list main :: nat -> nat list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Cons(X{*},X{*}) | S(X{*}) | ConsL(X{*},X{*}) | Nil() | 0() | ConsL(X{*},X{*}) | Nil() | NilL() | 0() | ConsL(X{*},X{*}) | 0() | ConsL(X{*},X{*}) ,V{x1_10} -> V{x2_12} ,V{x2_10} -> V{x8_9} | zeros() ,V{x2_12} -> V{x10_9} | V{x6_13} ,V{x4_5} -> bot[0]() ,V{x6_8} -> 0() ,V{x6_9} -> 0() ,V{x6_13} -> X{*} ,V{x8_8} -> zeros() ,V{x8_9} -> zeros() ,V{x10_9} -> X{*} ,R{0} -> R{13} | main(X{*}) ,R{5} -> ConsL(0(),zeros()) ,R{8} -> Nil() ,R{9} -> Cons(V{x6_9},R{10}) | Cons(V{x6_9},@(R{12},V{x8_9})) | Cons(V{x6_9},@(@(take_l(),V{x10_9}),V{x8_9})) ,R{10} -> R{9} | R{8} | cond_take_l_n_xs(R{5},V{x1_10}) | cond_take_l_n_xs(@(V{x2_10},bot[0]()),V{x1_10}) ,R{12} -> take_l_n(V{x2_12}) ,R{13} -> R{10} | @(R{12},zeros()) | @(@(take_l(),V{x6_13}),zeros())} * Step 10: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 5: zeros() bot[0]() -> ConsL(0(), zeros()) 8: cond_take_l_n_xs(ConsL(0(), zeros()), 0()) -> Nil() 9: cond_take_l_n_xs(ConsL(0(), zeros()), S(x1)) -> Cons(0(), take_l() x1 zeros()) 10: take_l_n(x1) zeros() -> cond_take_l_n_xs(zeros() bot[0](), x1) 12: take_l() x2 -> take_l_n(x2) 13: main(x1) -> take_l() x1 zeros() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list S :: nat -> nat take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list take_l :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list main :: nat -> nat list + Applied Processor: UncurryATRS + Details: none * Step 11: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: zeros#1(bot[0]()) -> ConsL(0(), zeros()) 2: cond_take_l_n_xs(ConsL(0(), zeros()), 0()) -> Nil() 3: cond_take_l_n_xs(ConsL(0(), zeros()), S(x1)) -> Cons(0(), take_l#2(x1, zeros())) 4: take_l_n#1(x1, zeros()) -> cond_take_l_n_xs(zeros#1(bot[0]()), x1) 5: take_l#1(x2) -> take_l_n(x2) 6: take_l#2(x2, x3) -> take_l_n#1(x2, x3) 7: main(x1) -> take_l#2(x1, zeros()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list S :: nat -> nat bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list main :: nat -> nat list take_l#1 :: nat -> (Unit -> nat lazy_list) -> nat list take_l#2 :: nat -> (Unit -> nat lazy_list) -> nat list take_l_n :: nat -> (Unit -> nat lazy_list) -> nat list take_l_n#1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list zeros#1 :: Unit -> nat lazy_list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 12: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: zeros#1(bot[0]()) -> ConsL(0(), zeros()) 2: cond_take_l_n_xs(ConsL(0(), zeros()), 0()) -> Nil() 3: cond_take_l_n_xs(ConsL(0(), zeros()), S(x1)) -> Cons(0(), take_l#2(x1, zeros())) 4: take_l_n#1(x1, zeros()) -> cond_take_l_n_xs(zeros#1(bot[0]()), x1) 6: take_l#2(x2, x3) -> take_l_n#1(x2, x3) 7: main(x1) -> take_l#2(x1, zeros()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list S :: nat -> nat bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list main :: nat -> nat list take_l#2 :: nat -> (Unit -> nat lazy_list) -> nat list take_l_n#1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list zeros#1 :: Unit -> nat lazy_list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 13: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: zeros#1(bot[0]()) -> ConsL(0(), zeros()) 2: cond_take_l_n_xs(ConsL(0(), zeros()), 0()) -> Nil() 3: cond_take_l_n_xs(ConsL(0(), zeros()), S(x1)) -> Cons(0(), take_l#2(x1, zeros())) 4: take_l_n#1(x3, zeros()) -> cond_take_l_n_xs(ConsL(0(), zeros()), x3) 5: take_l#2(x2, zeros()) -> cond_take_l_n_xs(zeros#1(bot[0]()), x2) 6: main(x1) -> take_l#2(x1, zeros()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list S :: nat -> nat bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list main :: nat -> nat list take_l#2 :: nat -> (Unit -> nat lazy_list) -> nat list take_l_n#1 :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list zeros#1 :: Unit -> nat lazy_list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 14: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: zeros#1(bot[0]()) -> ConsL(0(), zeros()) 2: cond_take_l_n_xs(ConsL(0(), zeros()), 0()) -> Nil() 3: cond_take_l_n_xs(ConsL(0(), zeros()), S(x1)) -> Cons(0(), take_l#2(x1, zeros())) 5: take_l#2(x2, zeros()) -> cond_take_l_n_xs(zeros#1(bot[0]()), x2) 6: main(x1) -> take_l#2(x1, zeros()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list S :: nat -> nat bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list main :: nat -> nat list take_l#2 :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list zeros#1 :: Unit -> nat lazy_list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: zeros#1(bot[0]()) -> ConsL(0(), zeros()) 2: cond_take_l_n_xs(ConsL(0(), zeros()), 0()) -> Nil() 3: cond_take_l_n_xs(ConsL(0(), zeros()), S(x1)) -> Cons(0(), take_l#2(x1, zeros())) 4: take_l#2(x5, zeros()) -> cond_take_l_n_xs(ConsL(0(), zeros()), x5) 5: main(x1) -> take_l#2(x1, zeros()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list S :: nat -> nat bot[0] :: Unit cond_take_l_n_xs :: nat lazy_list -> nat -> nat list main :: nat -> nat list take_l#2 :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list zeros#1 :: Unit -> nat lazy_list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 2: cond_take_l_n_xs(ConsL(0(), zeros()), 0()) -> Nil() 3: cond_take_l_n_xs(ConsL(0(), zeros()), S(x1)) -> Cons(0(), take_l#2(x1, zeros())) 4: take_l#2(x5, zeros()) -> cond_take_l_n_xs(ConsL(0(), zeros()), x5) 5: main(x1) -> take_l#2(x1, zeros()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list S :: nat -> nat cond_take_l_n_xs :: nat lazy_list -> nat -> nat list main :: nat -> nat list take_l#2 :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 17: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: cond_take_l_n_xs(ConsL(0(), zeros()), 0()) -> Nil() 2: cond_take_l_n_xs(ConsL(0(), zeros()), S(x1)) -> Cons(0(), take_l#2(x1, zeros())) 3: take_l#2(0(), zeros()) -> Nil() 4: take_l#2(S(x2), zeros()) -> Cons(0(), take_l#2(x2, zeros())) 5: main(x1) -> take_l#2(x1, zeros()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsL :: 'a -> (Unit -> 'a lazy_list) -> 'a lazy_list Nil :: 'a list S :: nat -> nat cond_take_l_n_xs :: nat lazy_list -> nat -> nat list main :: nat -> nat list take_l#2 :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 18: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 3: take_l#2(0(), zeros()) -> Nil() 4: take_l#2(S(x2), zeros()) -> Cons(0(), take_l#2(x2, zeros())) 5: main(x1) -> take_l#2(x1, zeros()) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat -> nat list take_l#2 :: nat -> (Unit -> nat lazy_list) -> nat list zeros :: Unit -> nat lazy_list + Applied Processor: Compression + Details: none * Step 19: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: take_l#2(0()) -> Nil() 2: take_l#2(S(x2)) -> Cons(take_l#2(x2)) 3: main(x1) -> take_l#2(x1) where 0 :: nat Cons :: 'a list -> 'a list Nil :: 'a list S :: nat -> nat main :: nat -> nat list take_l#2 :: nat -> nat list + Applied Processor: ToTctProblem + Details: none * Step 20: Ara WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: main(x1) -> take_l#2(x1) take_l#2(0()) -> Nil() take_l#2(S(x2)) -> Cons(take_l#2(x2)) - Signature: {main/1,take_l#2/1} / {0/0,Cons/1,Nil/0,S/1} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,Nil,S} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 5, araRuleShifting = Nothing} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(1) F (TrsFun "Cons") :: ["A"(0)] -(0)-> "A"(0) F (TrsFun "Nil") :: [] -(0)-> "A"(0) F (TrsFun "S") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "main") :: ["A"(1)] -(2)-> "A"(0) F (TrsFun "take_l#2") :: ["A"(1)] -(1)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- WORST_CASE(?,O(n^1))