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 nat = 0 | S of nat ;; let rec fold f z xs = match xs with | Nil -> z | Cons(x,xs') -> f x (fold f z xs') ;; let rec plus x y = match x with | 0 -> y | S(x') -> S(plus x' y) ;; let sum l = fold plus 0 l ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λl : nat list. (λfold : (nat -> nat -> nat) -> nat -> nat list -> nat. (λplus : nat -> nat -> nat. (λsum : nat list -> nat. sum l) (λl : nat list. fold plus 0 l)) (μplus : nat -> nat -> nat. λx : nat. λy : nat. case x of | 0 -> y | S -> λx' : nat. S(plus x' y))) (μfold : (nat -> nat -> nat) -> nat -> nat list -> nat. λf : nat -> nat -> nat. λz : nat. λxs : nat list. case xs of | Nil -> z | Cons -> λx : nat. λxs' : nat list. f x (fold f z xs')) : nat list -> nat where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: sum(x1, x2) x3 -> x1 x2 0() x3 3: main_2(x0, x1) x2 -> main_3(x0) sum(x1, x2) 4: cond_plus_x_y(0(), x3) -> x3 5: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 6: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 7: plus_1() x2 -> plus_x(x2) 8: plus() x0 -> plus_1() x0 9: main_1(x0) x1 -> main_2(x0, x1) plus() 10: cond_fold_f_z_xs(Nil(), x1, x2) -> x2 11: cond_fold_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (fold() x1 x2 x5) 12: fold_f_z(x1, x2) x3 -> cond_fold_f_z_xs(x3, x1, x2) 13: fold_f(x1) x2 -> fold_f_z(x1, x2) 14: fold_1() x1 -> fold_f(x1) 15: fold() x0 -> fold_1() x0 16: main(x0) -> main_1(x0) fold() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat sum :: ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat list -> nat plus_x :: nat -> nat -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main_1 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> nat plus_1 :: nat -> nat -> nat main_2 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (nat list -> nat) -> nat cond_fold_f_z_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat fold :: (nat -> nat -> nat) -> nat -> nat list -> nat plus :: nat -> nat -> nat main :: nat list -> nat + 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: sum(x1, x2) x3 -> x1 x2 0() x3 3: main_2(x0, x3) x5 -> sum(x3, x5) x0 4: cond_plus_x_y(0(), x3) -> x3 5: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 6: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 7: plus_1() x2 -> plus_x(x2) 8: plus() x4 -> plus_x(x4) 9: main_1(x0) x2 -> main_3(x0) sum(x2, plus()) 10: cond_fold_f_z_xs(Nil(), x1, x2) -> x2 11: cond_fold_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (fold() x1 x2 x5) 12: fold_f_z(x1, x2) x3 -> cond_fold_f_z_xs(x3, x1, x2) 13: fold_f(x1) x2 -> fold_f_z(x1, x2) 14: fold_1() x1 -> fold_f(x1) 15: fold() x2 -> fold_f(x2) 16: main(x0) -> main_2(x0, fold()) plus() where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat sum :: ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat list -> nat plus_x :: nat -> nat -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main_1 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> nat plus_1 :: nat -> nat -> nat main_2 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (nat list -> nat) -> nat cond_fold_f_z_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat fold :: (nat -> nat -> nat) -> nat -> nat list -> nat plus :: nat -> nat -> nat main :: nat list -> nat + 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: sum(x1, x2) x3 -> x1 x2 0() x3 3: main_2(x6, x2) x4 -> x2 x4 0() x6 4: cond_plus_x_y(0(), x3) -> x3 5: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 6: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 7: plus_1() x2 -> plus_x(x2) 8: plus() x4 -> plus_x(x4) 9: main_1(x0) x5 -> sum(x5, plus()) x0 10: cond_fold_f_z_xs(Nil(), x1, x2) -> x2 11: cond_fold_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (fold() x1 x2 x5) 12: fold_f_z(x1, x2) x3 -> cond_fold_f_z_xs(x3, x1, x2) 13: fold_f(x1) x2 -> fold_f_z(x1, x2) 14: fold_1() x1 -> fold_f(x1) 15: fold() x2 -> fold_f(x2) 16: main(x0) -> sum(fold(), plus()) x0 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat sum :: ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat list -> nat plus_x :: nat -> nat -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main_1 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> nat plus_1 :: nat -> nat -> nat main_2 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (nat list -> nat) -> nat cond_fold_f_z_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat fold :: (nat -> nat -> nat) -> nat -> nat list -> nat plus :: nat -> nat -> nat main :: nat list -> nat + 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: sum(x1, x2) x3 -> x1 x2 0() x3 3: main_2(x6, x2) x4 -> x2 x4 0() x6 4: cond_plus_x_y(0(), x3) -> x3 5: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 6: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 7: plus_1() x2 -> plus_x(x2) 8: plus() x4 -> plus_x(x4) 9: main_1(x6) x2 -> x2 plus() 0() x6 10: cond_fold_f_z_xs(Nil(), x1, x2) -> x2 11: cond_fold_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (fold() x1 x2 x5) 12: fold_f_z(x1, x2) x3 -> cond_fold_f_z_xs(x3, x1, x2) 13: fold_f(x1) x2 -> fold_f_z(x1, x2) 14: fold_1() x1 -> fold_f(x1) 15: fold() x2 -> fold_f(x2) 16: main(x6) -> fold() plus() 0() x6 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat sum :: ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat list -> nat plus_x :: nat -> nat -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main_1 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> nat plus_1 :: nat -> nat -> nat main_2 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (nat list -> nat) -> nat cond_fold_f_z_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat fold :: (nat -> nat -> nat) -> nat -> nat list -> nat plus :: nat -> nat -> nat main :: nat list -> nat + 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: sum(x1, x2) x3 -> x1 x2 0() x3 3: main_2(x6, x2) x4 -> x2 x4 0() x6 4: cond_plus_x_y(0(), x3) -> x3 5: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 6: plus_x(0()) x6 -> x6 7: plus_x(S(x8)) x6 -> S(plus() x8 x6) 8: plus_1() x2 -> plus_x(x2) 9: plus() x4 -> plus_x(x4) 10: main_1(x6) x2 -> x2 plus() 0() x6 11: cond_fold_f_z_xs(Nil(), x1, x2) -> x2 12: cond_fold_f_z_xs(Cons(x4, x5), x1, x2) -> x1 x4 (fold() x1 x2 x5) 13: fold_f_z(x2, x4) Nil() -> x4 14: fold_f_z(x2, x4) Cons(x8, x10) -> x2 x8 (fold() x2 x4 x10) 15: fold_f(x1) x2 -> fold_f_z(x1, x2) 16: fold_1() x1 -> fold_f(x1) 17: fold() x2 -> fold_f(x2) 18: main(x6) -> fold() plus() 0() x6 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat sum :: ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat list -> nat plus_x :: nat -> nat -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main_1 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> nat plus_1 :: nat -> nat -> nat main_2 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (nat list -> nat) -> nat cond_fold_f_z_xs :: nat list -> (nat -> nat -> nat) -> nat -> nat cond_plus_x_y :: nat -> nat -> nat fold :: (nat -> nat -> nat) -> nat -> nat list -> nat plus :: nat -> nat -> nat main :: nat list -> nat + 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: sum(x1, x2) x3 -> x1 x2 0() x3 3: main_2(x6, x2) x4 -> x2 x4 0() x6 6: plus_x(0()) x6 -> x6 7: plus_x(S(x8)) x6 -> S(plus() x8 x6) 8: plus_1() x2 -> plus_x(x2) 9: plus() x4 -> plus_x(x4) 10: main_1(x6) x2 -> x2 plus() 0() x6 13: fold_f_z(x2, x4) Nil() -> x4 14: fold_f_z(x2, x4) Cons(x8, x10) -> x2 x8 (fold() x2 x4 x10) 15: fold_f(x1) x2 -> fold_f_z(x1, x2) 16: fold_1() x1 -> fold_f(x1) 17: fold() x2 -> fold_f(x2) 18: main(x6) -> fold() plus() 0() x6 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat sum :: ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat list -> nat plus_x :: nat -> nat -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main_1 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> nat plus_1 :: nat -> nat -> nat main_2 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (nat list -> nat) -> nat fold :: (nat -> nat -> nat) -> nat -> nat list -> nat plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: NeededRules + Details: none * Step 9: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: sum(x1, x2) x3 -> x1 x2 0() x3 3: main_2(x6, x2) x4 -> x2 x4 0() x6 4: plus_x(0()) x6 -> x6 5: plus_x(S(x8)) x6 -> S(plus() x8 x6) 6: plus_1() x2 -> plus_x(x2) 7: plus() x4 -> plus_x(x4) 8: main_1(x6) x2 -> x2 plus() 0() x6 9: fold_f_z(x2, x4) Nil() -> x4 10: fold_f_z(x2, x4) Cons(x8, x10) -> x2 x8 (fold() x2 x4 x10) 11: fold_f(x1) x2 -> fold_f_z(x1, x2) 12: fold_1() x1 -> fold_f(x1) 13: fold() x2 -> fold_f(x2) 14: main(x6) -> fold() plus() 0() x6 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat sum :: ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat list -> nat plus_x :: nat -> nat -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main_1 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> nat plus_1 :: nat -> nat -> nat main_2 :: nat list -> ((nat -> nat -> nat) -> nat -> nat list -> nat) -> (nat -> nat -> nat) -> nat main_3 :: nat list -> (nat list -> nat) -> nat fold :: (nat -> nat -> nat) -> nat -> nat list -> nat plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> 0() | Cons(X{*},X{*}) | Nil() | 0() | S(X{*}) | S(X{*}) | 0() | 0() | 0() ,V{x1_11} -> V{x2_13} ,V{x2_9} -> V{x1_11} ,V{x2_10} -> V{x1_11} ,V{x2_11} -> V{x4_10} | 0() ,V{x2_13} -> V{x2_10} | plus() ,V{x4_7} -> V{x8_5} | V{x8_10} ,V{x4_9} -> V{x2_11} ,V{x4_10} -> V{x2_11} ,V{x6_4} -> V{x6_5} | R{10} | R{9} ,V{x6_5} -> V{x6_5} | R{10} | R{9} ,V{x6_14} -> X{*} ,V{x8_5} -> X{*} ,V{x8_10} -> X{*} ,V{x10_10} -> X{*} ,R{0} -> R{14} | main(X{*}) ,R{4} -> V{x6_4} ,R{5} -> S(R{5}) | S(R{4}) | S(@(R{7},V{x6_5})) | S(@(@(plus(),V{x8_5}),V{x6_5})) ,R{7} -> plus_x(V{x4_7}) ,R{9} -> V{x4_9} ,R{10} -> R{5} | R{4} | @(R{7},R{9}) | @(R{7},R{10}) | @(@(V{x2_10},V{x8_10}),R{10}) | @(@(V{x2_10},V{x8_10}),R{9}) | @(R{7},@(R{11},V{x10_10})) | @(@(V{x2_10},V{x8_10}),@(R{11},V{x10_10})) | @(R{7},@(@(R{13},V{x4_10}),V{x10_10})) | @(@(V{x2_10},V{x8_10}),@(@(R{13},V{x4_10}),V{x10_10})) | @(R{7},@(@(@(fold(),V{x2_10}),V{x4_10}),V{x10_10})) | @(@(V{x2_10},V{x8_10}),@(@(@(fold(),V{x2_10}),V{x4_10}),V{x10_10})) ,R{11} -> fold_f_z(V{x1_11},V{x2_11}) ,R{13} -> fold_f(V{x2_13}) ,R{14} -> R{10} | R{9} | @(R{11},V{x6_14}) | @(@(R{13},0()),V{x6_14}) | @(@(@(fold(),plus()),0()),V{x6_14})} * Step 10: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 4: plus_x(0()) x6 -> x6 5: plus_x(S(x2)) x1 -> S(plus() x2 x1) 7: plus() x4 -> plus_x(x4) 9: fold_f_z(plus(), 0()) Nil() -> 0() 10: fold_f_z(plus(), 0()) Cons(x2, x1) -> plus() x2 (fold() plus() 0() x1) 11: fold_f(plus()) 0() -> fold_f_z(plus(), 0()) 13: fold() plus() -> fold_f(plus()) 14: main(x1) -> fold() plus() 0() x1 where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat plus_x :: nat -> nat -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold :: (nat -> nat -> nat) -> nat -> nat list -> nat plus :: nat -> nat -> nat main :: nat list -> nat + Applied Processor: UncurryATRS + Details: none * Step 11: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: plus_x#1(0(), x6) -> x6 2: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 3: plus#1(x4) -> plus_x(x4) 4: plus#2(x4, x5) -> plus_x#1(x4, x5) 5: fold_f_z#1(plus(), 0(), Nil()) -> 0() 6: fold_f_z#1(plus(), 0(), Cons(x2, x1)) -> plus#2(x2, fold#3(plus(), 0(), x1)) 7: fold_f#1(plus(), 0()) -> fold_f_z(plus(), 0()) 8: fold_f#2(plus(), 0(), x0) -> fold_f_z#1(plus(), 0(), x0) 9: fold#1(plus()) -> fold_f(plus()) 10: fold#2(plus(), x0) -> fold_f#1(plus(), x0) 11: fold#3(plus(), x0, x1) -> fold_f#2(plus(), x0, x1) 12: main(x1) -> fold#3(plus(), 0(), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold#1 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold#2 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold#3 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f#1 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f#2 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f_z :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f_z#1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main :: nat list -> nat plus :: nat -> nat -> nat plus#1 :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_x :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 12: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: plus_x#1(0(), x6) -> x6 2: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 4: plus#2(x4, x5) -> plus_x#1(x4, x5) 5: fold_f_z#1(plus(), 0(), Nil()) -> 0() 6: fold_f_z#1(plus(), 0(), Cons(x2, x1)) -> plus#2(x2, fold#3(plus(), 0(), x1)) 8: fold_f#2(plus(), 0(), x0) -> fold_f_z#1(plus(), 0(), x0) 11: fold#3(plus(), x0, x1) -> fold_f#2(plus(), x0, x1) 12: main(x1) -> fold#3(plus(), 0(), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold#3 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f#2 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f_z#1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main :: nat list -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 13: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: plus_x#1(0(), x6) -> x6 2: plus_x#1(S(x2), x1) -> S(plus#2(x2, x1)) 3: plus#2(0(), x12) -> x12 4: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 5: fold_f_z#1(plus(), 0(), Nil()) -> 0() 6: fold_f_z#1(plus(), 0(), Cons(x2, x1)) -> plus#2(x2, fold#3(plus(), 0(), x1)) 7: fold_f#2(plus(), 0(), Nil()) -> 0() 8: fold_f#2(plus(), 0(), Cons(x4, x2)) -> plus#2(x4, fold#3(plus(), 0(), x2)) 9: fold#3(plus(), 0(), x0) -> fold_f_z#1(plus(), 0(), x0) 10: main(x1) -> fold#3(plus(), 0(), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold#3 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f#2 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f_z#1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main :: nat list -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_x#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 14: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 3: plus#2(0(), x12) -> x12 4: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 5: fold_f_z#1(plus(), 0(), Nil()) -> 0() 6: fold_f_z#1(plus(), 0(), Cons(x2, x1)) -> plus#2(x2, fold#3(plus(), 0(), x1)) 9: fold#3(plus(), 0(), x0) -> fold_f_z#1(plus(), 0(), x0) 10: main(x1) -> fold#3(plus(), 0(), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold#3 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f_z#1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main :: nat list -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: plus#2(0(), x12) -> x12 2: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 3: fold_f_z#1(plus(), 0(), Nil()) -> 0() 4: fold_f_z#1(plus(), 0(), Cons(x2, x1)) -> plus#2(x2, fold#3(plus(), 0(), x1)) 5: fold#3(plus(), 0(), Nil()) -> 0() 6: fold#3(plus(), 0(), Cons(x4, x2)) -> plus#2(x4, fold#3(plus(), 0(), x2)) 7: main(x1) -> fold#3(plus(), 0(), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold#3 :: (nat -> nat -> nat) -> nat -> nat list -> nat fold_f_z#1 :: (nat -> nat -> nat) -> nat -> nat list -> nat main :: nat list -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 1: plus#2(0(), x12) -> x12 2: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 5: fold#3(plus(), 0(), Nil()) -> 0() 6: fold#3(plus(), 0(), Cons(x4, x2)) -> plus#2(x4, fold#3(plus(), 0(), x2)) 7: main(x1) -> fold#3(plus(), 0(), x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold#3 :: (nat -> nat -> nat) -> nat -> nat list -> nat main :: nat list -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Compression + Details: none * Step 17: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: plus#2(0(), x12) -> x12 2: plus#2(S(x4), x2) -> S(plus#2(x4, x2)) 3: fold#3(Nil()) -> 0() 4: fold#3(Cons(x4, x2)) -> plus#2(x4, fold#3(x2)) 5: main(x1) -> fold#3(x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list Nil :: 'a list S :: nat -> nat fold#3 :: nat list -> nat main :: nat list -> nat plus#2 :: nat -> nat -> nat + Applied Processor: ToTctProblem + Details: none * Step 18: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Signature: {fold#3/1,main/1,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: 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(S) = {1}, uargs(plus#2) = {2} Following symbols are considered usable: {fold#3,main,plus#2} TcT has computed the following interpretation: p(0) = [0] p(Cons) = [0] p(Nil) = [8] p(S) = [1] x1 + [0] p(fold#3) = [0] p(main) = [5] p(plus#2) = [1] x2 + [0] Following rules are strictly oriented: main(x1) = [5] > [0] = fold#3(x1) Following rules are (at-least) weakly oriented: fold#3(Cons(x4,x2)) = [0] >= [0] = plus#2(x4,fold#3(x2)) fold#3(Nil()) = [0] >= [0] = 0() plus#2(0(),x12) = [1] x12 + [0] >= [1] x12 + [0] = x12 plus#2(S(x4),x2) = [1] x2 + [0] >= [1] x2 + [0] = S(plus#2(x4,x2)) * Step 19: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Weak TRS: main(x1) -> fold#3(x1) - Signature: {fold#3/1,main/1,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: 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(S) = {1}, uargs(plus#2) = {2} Following symbols are considered usable: {fold#3,main,plus#2} TcT has computed the following interpretation: p(0) = 0 p(Cons) = 12 + x1 + x2 p(Nil) = 13 p(S) = x1 p(fold#3) = x1 p(main) = 8 + x1 p(plus#2) = x2 Following rules are strictly oriented: fold#3(Cons(x4,x2)) = 12 + x2 + x4 > x2 = plus#2(x4,fold#3(x2)) fold#3(Nil()) = 13 > 0 = 0() Following rules are (at-least) weakly oriented: main(x1) = 8 + x1 >= x1 = fold#3(x1) plus#2(0(),x12) = x12 >= x12 = x12 plus#2(S(x4),x2) = x2 >= x2 = S(plus#2(x4,x2)) * Step 20: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Weak TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) - Signature: {fold#3/1,main/1,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: 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(S) = {1}, uargs(plus#2) = {2} Following symbols are considered usable: {fold#3,main,plus#2} TcT has computed the following interpretation: p(0) = [2] p(Cons) = [1] x1 + [1] x2 + [1] p(Nil) = [0] p(S) = [1] x1 + [0] p(fold#3) = [8] x1 + [9] p(main) = [8] x1 + [9] p(plus#2) = [6] x1 + [1] x2 + [3] Following rules are strictly oriented: plus#2(0(),x12) = [1] x12 + [15] > [1] x12 + [0] = x12 Following rules are (at-least) weakly oriented: fold#3(Cons(x4,x2)) = [8] x2 + [8] x4 + [17] >= [8] x2 + [6] x4 + [12] = plus#2(x4,fold#3(x2)) fold#3(Nil()) = [9] >= [2] = 0() main(x1) = [8] x1 + [9] >= [8] x1 + [9] = fold#3(x1) plus#2(S(x4),x2) = [1] x2 + [6] x4 + [3] >= [1] x2 + [6] x4 + [3] = S(plus#2(x4,x2)) * Step 21: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Weak TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 - Signature: {fold#3/1,main/1,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: 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(S) = {1}, uargs(plus#2) = {2} Following symbols are considered usable: {fold#3,main,plus#2} TcT has computed the following interpretation: p(0) = 8 p(Cons) = x1 + x2 p(Nil) = 4 p(S) = 1 + x1 p(fold#3) = 2*x1 p(main) = 3 + 4*x1 p(plus#2) = 2*x1 + x2 Following rules are strictly oriented: plus#2(S(x4),x2) = 2 + x2 + 2*x4 > 1 + x2 + 2*x4 = S(plus#2(x4,x2)) Following rules are (at-least) weakly oriented: fold#3(Cons(x4,x2)) = 2*x2 + 2*x4 >= 2*x2 + 2*x4 = plus#2(x4,fold#3(x2)) fold#3(Nil()) = 8 >= 8 = 0() main(x1) = 3 + 4*x1 >= 2*x1 = fold#3(x1) plus#2(0(),x12) = 16 + x12 >= x12 = x12 * Step 22: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: fold#3(Cons(x4,x2)) -> plus#2(x4,fold#3(x2)) fold#3(Nil()) -> 0() main(x1) -> fold#3(x1) plus#2(0(),x12) -> x12 plus#2(S(x4),x2) -> S(plus#2(x4,x2)) - Signature: {fold#3/1,main/1,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: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))