WORST_CASE(?,O(n^3)) * Step 1: Desugar WORST_CASE(?,O(n^3)) + 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 option = None | Some of 'a ;; 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: * examples/running.raml * * Author: * Jan Hoffmann (S(S(0))015) * * Description: * Running example in the S(S(0))015 TR. * *) ;; type Exception = Not_found | Inv_arg ;; let rec append l1 l2 = match l1 with | Nil()-> l2 | Cons(x,xs) -> Cons(x,(append xs l2)) ;; let rec partition f l = match l with | Nil()-> Pair(Nil,Nil) | Cons(x,xs) -> (match partition f xs with | Pair(cs,bs) -> ite (f x) Pair(cs,Cons(x,bs)) Pair(Cons(x,cs),bs)) ;; let rec quicksort gt xyz = match xyz with | Nil()-> Nil | Cons(x,xs) -> (match partition (gt x) xs with | Pair(ys, zs) -> append (quicksort gt ys) (Cons(x,(quicksort gt zs)))) ;; type ('a,'b) ablist = Acons of 'a * ('a,'b) ablist | Bcons of 'b * ('a,'b) ablist | Nil ;; let rec abmap f g abs = match abs with | Acons(a,abs') -> Acons(f a, abmap f g abs') | Bcons(b,abs') -> Bcons(g b, abmap f g abs') | Nil()-> Nil ;; let asort gt abs = abmap (quicksort gt) (fun x -> x) abs ;; let asort' gt abs = abmap (quicksort gt) (fun unused -> error Inv_arg) abs ;; let btick = abmap (fun a -> a) (fun b -> b) ;; let rec abfoldr f g acc abs = match abs with | Acons(a,abs') -> let acc' = abfoldr f g acc abs' in f a acc' | Bcons(b,abs') -> let acc' = abfoldr f g acc abs' in g b acc' | Nil()-> acc ;; let cons_all abs = let f x y = let fa = fun x acc -> error Not_found in let fb = fun b acc -> Bcons(plus b x,acc) in abfoldr fa fb Nil y in let g x y = Bcons (x,y) in abfoldr f g Nil abs ;; (* let abs = Acons ((Cons(S(0),Cons(S(S(0)),Nil))),Bcons (S(S(S(0))), Bcons (S(S(S(S(0)))), Nil))) * ;; *) (* let e1 () = asort (>) (Acons ((Cons(S(0),Cons(S(S(0)),Nil))),Bcons (0, Acons ((Cons(S(S(S(0))),Cons(S(S(S(S(0)))),Nil))), Nil)))) * let e2 () = asort' (>) (Acons ((Cons(S(0),Cons(S(S(0)),Nil))),Bcons (0, Acons ((Cons(S(S(S(0))),Cons(S(S(S(S(0)))),Nil))), Nil)))) * let e3 () = btick (Acons ((Cons(S(0),Cons(S(S(0)),Nil))),Bcons (0, Acons ((Cons(S(S(S(0))),Cons(S(S(S(S(0)))),Nil))), Nil)))) * * * ;; * let abs = Acons (S(0)00, Bcons (S(S(0)), Bcons (S(S(S(0))), Acons(S(S(S(S(0)))),Nil)))) *) let main abs = cons_all abs ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^3)) + Considered Problem: λabs : (nat,nat) ablist. (λplus : nat -> nat -> nat. (λabfoldr : (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist. (λcons_all : (nat,nat) ablist -> (nat,nat) ablist. (λmain : (nat,nat) ablist -> (nat,nat) ablist. main abs) (λabs : (nat,nat) ablist. cons_all abs)) (λabs : (nat,nat) ablist. (λf : nat -> (nat,nat) ablist -> (nat,nat) ablist. (λg : nat -> (nat,nat) ablist -> (nat,nat) ablist. abfoldr f g Nil abs) (λx : nat. λy : (nat,nat) ablist. Bcons(x,y))) (λx : nat. λy : (nat,nat) ablist. (λfa : nat -> (nat,nat) ablist -> (nat,nat) ablist. (λfb : nat -> (nat,nat) ablist -> (nat,nat) ablist. abfoldr fa fb Nil y) (λb : nat. λacc : (nat,nat) ablist. Bcons(plus b x,acc))) (λx : nat. λacc : (nat,nat) ablist. ⟘  Not_found)))) (μabfoldr : (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist. λf : nat -> (nat,nat) ablist -> (nat,nat) ablist. λg : nat -> (nat,nat) ablist -> (nat,nat) ablist. λacc : (nat,nat) ablist. λabs : (nat,nat) ablist. case abs of | Acons -> λa : nat. λabs' : (nat,nat) ablist. (λacc' : (nat,nat) ablist. f a acc') (abfoldr f g acc abs') | Bcons -> λb : nat. λabs' : (nat,nat) ablist. (λacc' : (nat,nat) ablist. g b acc') (abfoldr f g acc abs') | Nil -> acc)) (μplus : nat -> nat -> nat. λn : nat. λm : nat. case m of | 0 -> n | S -> λx : nat. S(plus n x)) : (nat ,nat) ablist -> (nat ,nat) ablist where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Cons :: 'a -> 'a list -> 'a list False :: bool Inv_arg :: Exception Nil :: ('a,'b) ablist None :: 'a option Not_found :: Exception Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Some :: 'a -> 'a option Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple True :: bool Unit :: Unit + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x0) x3 -> main_4(x0) main_5(x3) 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x2, x3) x4 -> cons_all_abs_1(x2, x3, x4) g() 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x1, x2, x4, x5) x6 -> f_x_y_1(x2, x5, x6) fb(x1, x4) 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x1, x2, x4) x5 -> f_x_y(x1, x2, x4, x5) fa() 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x1, x2) x3 -> cons_all_abs(x2, x3) f(x1, x2) 17: main_2(x0, x1) x2 -> main_3(x0) cons_all(x1, x2) 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 20: cond_abfoldr_f_g_acc_abs(Acons(x6, x7), x2, x3, x4) -> abfoldr_f_g_acc_abs_2(x2, x6) (abfoldr() x2 x3 x4 x7) 21: cond_abfoldr_f_g_acc_abs(Bcons(x6, x7), x2, x3, x4) -> abfoldr_f_g_acc_abs_5(x3, x6) (abfoldr() x2 x3 x4 x7) 22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4 23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4) 24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 26: abfoldr_1() x2 -> abfoldr_f(x2) 27: abfoldr() x0 -> abfoldr_1() x0 28: main_1(x0) x1 -> main_2(x0, x1) abfoldr() 29: cond_plus_n_m(0(), x1) -> x1 30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 32: plus_1() x1 -> plus_n(x1) 33: plus() x0 -> plus_1() x0 34: main(x0) -> main_1(x0) plus() where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist cond_plus_n_m :: nat -> nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x0) x7 -> main_5(x7) x0 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x2, x4, x8) x10 -> f_x_y_1(x4, x10, fa()) fb(x2, x8) 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x3, x4) x6 -> cons_all_abs_1(x4, x6, f(x3, x4)) g() 17: main_2(x0, x3) x5 -> main_4(x0) main_5(cons_all(x3, x5)) 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15) 21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15) 22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4 23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4) 24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 26: abfoldr_1() x2 -> abfoldr_f(x2) 27: abfoldr() x4 -> abfoldr_f(x4) 28: main_1(x0) x2 -> main_3(x0) cons_all(x2, abfoldr()) 29: cond_plus_n_m(0(), x1) -> x1 30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 32: plus_1() x1 -> plus_n(x1) 33: plus() x2 -> plus_n(x2) 34: main(x0) -> main_2(x0, plus()) abfoldr() where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist cond_plus_n_m :: nat -> nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x8) x6 -> x6 x8 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6 17: main_2(x0, x7) x11 -> main_5(cons_all(x7, x11)) x0 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15) 21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15) 22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4 23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4) 24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 26: abfoldr_1() x2 -> abfoldr_f(x2) 27: abfoldr() x4 -> abfoldr_f(x4) 28: main_1(x0) x5 -> main_5(cons_all(x5, abfoldr())) x0 29: cond_plus_n_m(0(), x1) -> x1 30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 32: plus_1() x1 -> plus_n(x1) 33: plus() x2 -> plus_n(x2) 34: main(x0) -> main_4(x0) main_5(cons_all(plus(), abfoldr())) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist cond_plus_n_m :: nat -> nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x8) x6 -> x6 x8 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6 17: main_2(x8, x15) x23 -> cons_all(x15, x23) x8 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15) 21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15) 22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4 23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4) 24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 26: abfoldr_1() x2 -> abfoldr_f(x2) 27: abfoldr() x4 -> abfoldr_f(x4) 28: main_1(x8) x11 -> cons_all(x11, abfoldr()) x8 29: cond_plus_n_m(0(), x1) -> x1 30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 32: plus_1() x1 -> plus_n(x1) 33: plus() x2 -> plus_n(x2) 34: main(x0) -> main_5(cons_all(plus(), abfoldr())) x0 where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist cond_plus_n_m :: nat -> nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x8) x6 -> x6 x8 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6 17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15) 21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15) 22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4 23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4) 24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 26: abfoldr_1() x2 -> abfoldr_f(x2) 27: abfoldr() x4 -> abfoldr_f(x4) 28: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12 29: cond_plus_n_m(0(), x1) -> x1 30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 32: plus_1() x1 -> plus_n(x1) 33: plus() x2 -> plus_n(x2) 34: main(x8) -> cons_all(plus(), abfoldr()) x8 where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist cond_plus_n_m :: nat -> nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 8: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x8) x6 -> x6 x8 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6 17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15) 21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15) 22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4 23: abfoldr_f_g_acc(x2, x3, x4) x5 -> cond_abfoldr_f_g_acc_abs(x5, x2, x3, x4) 24: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 25: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 26: abfoldr_1() x2 -> abfoldr_f(x2) 27: abfoldr() x4 -> abfoldr_f(x4) 28: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12 29: cond_plus_n_m(0(), x1) -> x1 30: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 31: plus_n(x1) x2 -> cond_plus_n_m(x2, x1) 32: plus_1() x1 -> plus_n(x1) 33: plus() x2 -> plus_n(x2) 34: main(x12) -> abfoldr() f(plus(), abfoldr()) g() Nil() x12 where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist cond_plus_n_m :: nat -> nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 9: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x8) x6 -> x6 x8 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6 17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 20: cond_abfoldr_f_g_acc_abs(Acons(x12, x15), x4, x7, x9) -> x4 x12 (abfoldr() x4 x7 x9 x15) 21: cond_abfoldr_f_g_acc_abs(Bcons(x12, x15), x5, x6, x9) -> x6 x12 (abfoldr() x5 x6 x9 x15) 22: cond_abfoldr_f_g_acc_abs(Nil(), x2, x3, x4) -> x4 23: abfoldr_f_g_acc(x8, x14, x18) Acons(x24, x30) -> x8 x24 (abfoldr() x8 x14 x18 x30) 24: abfoldr_f_g_acc(x10, x12, x18) Bcons(x24, x30) -> x12 x24 (abfoldr() x10 x12 x18 x30) 25: abfoldr_f_g_acc(x4, x6, x8) Nil() -> x8 26: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 27: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 28: abfoldr_1() x2 -> abfoldr_f(x2) 29: abfoldr() x4 -> abfoldr_f(x4) 30: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12 31: cond_plus_n_m(0(), x1) -> x1 32: cond_plus_n_m(S(x3), x1) -> S(plus() x1 x3) 33: plus_n(x2) 0() -> x2 34: plus_n(x2) S(x6) -> S(plus() x2 x6) 35: plus_1() x1 -> plus_n(x1) 36: plus() x2 -> plus_n(x2) 37: main(x12) -> abfoldr() f(plus(), abfoldr()) g() Nil() x12 where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist cond_abfoldr_f_g_acc_abs :: (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist cond_plus_n_m :: nat -> nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 10: NeededRules WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x8) x6 -> x6 x8 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6 17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 23: abfoldr_f_g_acc(x8, x14, x18) Acons(x24, x30) -> x8 x24 (abfoldr() x8 x14 x18 x30) 24: abfoldr_f_g_acc(x10, x12, x18) Bcons(x24, x30) -> x12 x24 (abfoldr() x10 x12 x18 x30) 25: abfoldr_f_g_acc(x4, x6, x8) Nil() -> x8 26: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 27: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 28: abfoldr_1() x2 -> abfoldr_f(x2) 29: abfoldr() x4 -> abfoldr_f(x4) 30: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12 33: plus_n(x2) 0() -> x2 34: plus_n(x2) S(x6) -> S(plus() x2 x6) 35: plus_1() x1 -> plus_n(x1) 36: plus() x2 -> plus_n(x2) 37: main(x12) -> abfoldr() f(plus(), abfoldr()) g() Nil() x12 where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: NeededRules + Details: none * Step 11: CFA WORST_CASE(?,O(n^3)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: main_5(x3) x4 -> x3 x4 3: main_3(x8) x6 -> x6 x8 4: cons_all_abs_1(x2, x3, x4) x5 -> x2 x4 x5 Nil() x3 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 7: cons_all_abs(x4, x6) x8 -> x4 x8 g() Nil() x6 8: f_x_y_1(x2, x5, x6) x7 -> x2 x6 x7 Nil() x5 9: fb_1(x1, x4, x7) x8 -> Bcons(x1 x7 x4, x8) 10: fb(x1, x4) x7 -> fb_1(x1, x4, x7) 11: f_x_y(x3, x4, x9, x10) x12 -> x4 x12 fb(x3, x9) Nil() x10 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(x5, x4, x17) x10 -> x4 fa() fb(x5, x17) Nil() x10 15: f(x1, x2) x4 -> f_x(x1, x2, x4) 16: cons_all(x7, x4) x6 -> x4 f(x7, x4) g() Nil() x6 17: main_2(x12, x14) x8 -> x8 f(x14, x8) g() Nil() x12 18: abfoldr_f_g_acc_abs_2(x2, x6) x8 -> x2 x6 x8 19: abfoldr_f_g_acc_abs_5(x3, x6) x8 -> x3 x6 x8 20: abfoldr_f_g_acc(x8, x14, x18) Acons(x24, x30) -> x8 x24 (abfoldr() x8 x14 x18 x30) 21: abfoldr_f_g_acc(x10, x12, x18) Bcons(x24, x30) -> x12 x24 (abfoldr() x10 x12 x18 x30) 22: abfoldr_f_g_acc(x4, x6, x8) Nil() -> x8 23: abfoldr_f_g(x2, x3) x4 -> abfoldr_f_g_acc(x2, x3, x4) 24: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 25: abfoldr_1() x2 -> abfoldr_f(x2) 26: abfoldr() x4 -> abfoldr_f(x4) 27: main_1(x12) x14 -> abfoldr() f(x14, abfoldr()) g() Nil() x12 28: plus_n(x2) 0() -> x2 29: plus_n(x2) S(x6) -> S(plus() x2 x6) 30: plus_1() x1 -> plus_n(x1) 31: plus() x2 -> plus_n(x2) 32: main(x12) -> abfoldr() f(plus(), abfoldr()) g() Nil() x12 where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat cons_all_abs :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist f_x_y :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist cons_all_abs_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_1 :: (nat,nat) ablist -> (nat -> nat -> nat) -> (nat,nat) ablist plus_1 :: nat -> nat -> nat f_x_y_1 :: ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_2 :: (nat,nat) ablist -> (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_3 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist main_4 :: (nat,nat) ablist -> ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist abfoldr_f_g_acc_abs_5 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist main_5 :: ((nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Nil() | S(X{*}) | S(X{*}) | 0() | Nil() | Nil() | Bcons(X{*},X{*}) | Acons(X{*},X{*}) | Nil() | Nil() | Nil() | Not_found() | Nil() | Bcons(X{*},X{*}) | Nil() | Nil() | Bcons(X{*},X{*}) | Nil() ,V{x1_9} -> V{x1_10} ,V{x1_10} -> V{x5_14} ,V{x1_15} -> plus() ,V{x2_15} -> abfoldr() ,V{x2_23} -> V{x2_24} ,V{x2_24} -> V{x4_26} ,V{x2_28} -> V{x2_31} ,V{x2_29} -> V{x2_31} ,V{x2_31} -> V{x2_29} | V{x7_9} ,V{x3_23} -> V{x3_24} ,V{x3_24} -> fb(V{x5_14},V{x17_14}) | V{x12_21} | V{x14_20} | g() ,V{x4_9} -> V{x4_10} ,V{x4_10} -> V{x17_14} ,V{x4_14} -> V{x2_15} ,V{x4_15} -> V{x24_20} ,V{x4_22} -> V{x2_23} ,V{x4_23} -> V{x18_21} | V{x18_20} | Nil() ,V{x4_26} -> fa() | V{x10_21} | V{x8_20} | f(plus(),abfoldr()) ,V{x5_5} -> V{x5_6} ,V{x5_6} -> V{x24_21} ,V{x5_14} -> V{x1_15} ,V{x6_5} -> R{22} | R{21} | R{20} ,V{x6_13} -> V{x24_20} ,V{x6_22} -> V{x3_23} ,V{x6_29} -> X{*} ,V{x7_9} -> V{x7_10} ,V{x7_10} -> V{x24_21} ,V{x7_12} -> R{22} | R{21} | R{20} ,V{x8_9} -> R{22} | R{21} | R{20} ,V{x8_20} -> V{x2_23} ,V{x8_22} -> V{x4_23} ,V{x10_14} -> R{21} | R{20} | R{22} ,V{x10_21} -> V{x2_23} ,V{x12_21} -> V{x3_23} ,V{x12_32} -> X{*} ,V{x14_20} -> V{x3_23} ,V{x17_14} -> V{x4_15} ,V{x18_20} -> V{x4_23} ,V{x18_21} -> V{x4_23} ,V{x24_20} -> X{*} ,V{x24_21} -> R{29} | R{28} | V{x5_5} | @(@(V{x1_9},V{x7_9}),V{x4_9}) | @(R{31},V{x4_9}) | X{*} ,V{x30_20} -> X{*} ,V{x30_21} -> V{x6_5} | V{x8_9} | X{*} ,R{0} -> R{32} | main(X{*}) ,R{5} -> Bcons(V{x5_5},V{x6_5}) ,R{6} -> g_x(V{x5_6}) ,R{9} -> Bcons(R{29},V{x8_9}) | Bcons(R{28},V{x8_9}) | Bcons(@(R{31},V{x4_9}),V{x8_9}) | Bcons(@(@(V{x1_9},V{x7_9}),V{x4_9}),V{x8_9}) ,R{10} -> fb_1(V{x1_10},V{x4_10},V{x7_10}) ,R{12} -> @(bot[0](),Not_found()) ,R{13} -> fa_1() ,R{14} -> R{22} | R{21} | @(R{23},V{x10_14}) | @(@(R{24},Nil()),V{x10_14}) | @(@(@(R{26},fb(V{x5_14},V{x17_14})),Nil()),V{x10_14}) | @(@(@(@(V{x4_14},fa()),fb(V{x5_14},V{x17_14})),Nil()),V{x10_14}) ,R{15} -> f_x(V{x1_15},V{x2_15},V{x4_15}) ,R{20} -> R{12} | @(R{13},@(@(@(@(abfoldr(),V{x8_20}),V{x14_20}),V{x18_20}),V{x30_20})) | @(R{13},@(@(@(R{26},V{x14_20}),V{x18_20}),V{x30_20})) | @(R{13},@(@(R{24},V{x18_20}),V{x30_20})) | @(R{13},@(R{23},V{x30_20})) | @(R{13},R{20}) | @(R{13},R{21}) | @(R{13},R{22}) | R{14} | @(R{15},R{20}) | @(R{15},R{21}) | @(R{15},R{22}) | @(@(V{x8_20},V{x24_20}),R{22}) | @(@(V{x8_20},V{x24_20}),R{21}) | @(@(V{x8_20},V{x24_20}),R{20}) | @(R{15},@(R{23},V{x30_20})) | @(@(V{x8_20},V{x24_20}),@(R{23},V{x30_20})) | @(R{15},@(@(R{24},V{x18_20}),V{x30_20})) | @(@(V{x8_20},V{x24_20}),@(@(R{24},V{x18_20}),V{x30_20})) | @(R{15},@(@(@(R{26},V{x14_20}),V{x18_20}),V{x30_20})) | @(@(V{x8_20},V{x24_20}),@(@(@(R{26},V{x14_20}),V{x18_20}),V{x30_20})) | @(R{15},@(@(@(@(abfoldr(),V{x8_20}),V{x14_20}),V{x18_20}),V{x30_20})) | @(@(V{x8_20},V{x24_20}),@(@(@(@(abfoldr(),V{x8_20}),V{x14_20}),V{x18_20}),V{x30_20})) ,R{21} -> R{9} | @(R{10},@(@(@(@(abfoldr(),V{x10_21}),V{x12_21}),V{x18_21}),V{x30_21})) | @(R{10},@(@(@(R{26},V{x12_21}),V{x18_21}),V{x30_21})) | @(R{10},@(@(R{24},V{x18_21}),V{x30_21})) | @(R{10},@(R{23},V{x30_21})) | @(R{10},R{20}) | @(R{10},R{21}) | @(R{10},R{22}) | R{5} | @(R{6},R{20}) | @(R{6},R{21}) | @(R{6},R{22}) | @(@(V{x12_21},V{x24_21}),R{22}) | @(@(V{x12_21},V{x24_21}),R{21}) | @(@(V{x12_21},V{x24_21}),R{20}) | @(R{6},@(R{23},V{x30_21})) | @(@(V{x12_21},V{x24_21}),@(R{23},V{x30_21})) | @(R{6},@(@(R{24},V{x18_21}),V{x30_21})) | @(@(V{x12_21},V{x24_21}),@(@(R{24},V{x18_21}),V{x30_21})) | @(R{6},@(@(@(R{26},V{x12_21}),V{x18_21}),V{x30_21})) | @(@(V{x12_21},V{x24_21}),@(@(@(R{26},V{x12_21}),V{x18_21}),V{x30_21})) | @(R{6},@(@(@(@(abfoldr(),V{x10_21}),V{x12_21}),V{x18_21}),V{x30_21})) | @(@(V{x12_21},V{x24_21}),@(@(@(@(abfoldr(),V{x10_21}),V{x12_21}),V{x18_21}),V{x30_21})) ,R{22} -> V{x8_22} ,R{23} -> abfoldr_f_g_acc(V{x2_23},V{x3_23},V{x4_23}) ,R{24} -> abfoldr_f_g(V{x2_24},V{x3_24}) ,R{26} -> abfoldr_f(V{x4_26}) ,R{28} -> V{x2_28} ,R{29} -> S(R{29}) | S(R{28}) | S(@(R{31},V{x6_29})) | S(@(@(plus(),V{x2_29}),V{x6_29})) ,R{31} -> plus_n(V{x2_31}) ,R{32} -> R{22} | R{21} | R{20} | @(R{23},V{x12_32}) | @(@(R{24},Nil()),V{x12_32}) | @(@(@(R{26},g()),Nil()),V{x12_32}) | @(@(@(@(abfoldr(),f(plus(),abfoldr())),g()),Nil()),V{x12_32})} * Step 12: UncurryATRS WORST_CASE(?,O(n^3)) + Considered Problem: 5: g_x(x5) x6 -> Bcons(x5, x6) 6: g() x5 -> g_x(x5) 9: fb_1(plus(), x3, x2) x1 -> Bcons(plus() x2 x3, x1) 10: fb(plus(), x2) x1 -> fb_1(plus(), x2, x1) 12: fa_1() x7 -> bot[0]() Not_found() 13: fa() x6 -> fa_1() 14: f_x(plus(), abfoldr(), x2) x1 -> abfoldr() fa() fb(plus(), x2) Nil() x1 15: f(plus(), abfoldr()) x1 -> f_x(plus(), abfoldr(), x1) 20: abfoldr_f_g_acc(fa(), x3, Nil()) Acons(x2, x1) -> fa() x2 (abfoldr() fa() x3 Nil() x1) 21: abfoldr_f_g_acc(f(plus(), abfoldr()), x3, Nil()) Acons(x2, x1) -> f(plus(), abfoldr()) x2 (abfoldr() f(plus(), abfoldr()) x3 Nil() x1) 22: abfoldr_f_g_acc(x5, fb(x3, x4), Nil()) Bcons(x2, x1) -> fb(x3, x4) x2 (abfoldr() x5 fb(x3, x4) Nil() x1) 23: abfoldr_f_g_acc(x3, g(), Nil()) Bcons(x2, x1) -> g() x2 (abfoldr() x3 g() Nil() x1) 24: abfoldr_f_g_acc(x2, x1, Nil()) Nil() -> Nil() 25: abfoldr_f_g(x2, x1) Nil() -> abfoldr_f_g_acc(x2, x1, Nil()) 26: abfoldr_f(x2) x3 -> abfoldr_f_g(x2, x3) 28: abfoldr() x4 -> abfoldr_f(x4) 30: plus_n(x2) 0() -> x2 31: plus_n(x2) S(x1) -> S(plus() x2 x1) 33: plus() x2 -> plus_n(x2) 34: main(x1) -> abfoldr() f(plus(), abfoldr()) g() Nil() x1 where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus_n :: nat -> nat -> nat f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist bot[0] :: Exception -> (nat,nat) ablist abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat main :: (nat,nat) ablist -> (nat,nat) ablist + Applied Processor: UncurryATRS + Details: none * Step 13: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: g_x#1(x5, x6) -> Bcons(x5, x6) 2: g#1(x5) -> g_x(x5) 3: g#2(x5, x6) -> g_x#1(x5, x6) 4: fb_1#1(plus(), x3, x2, x1) -> Bcons(plus#2(x2, x3), x1) 5: fb#1(plus(), x2, x1) -> fb_1(plus(), x2, x1) 6: fb#2(plus(), x2, x1, x3) -> fb_1#1(plus(), x2, x1, x3) 7: fa_1#1(x7) -> bot[0]#1(Not_found()) 8: fa#1(x6) -> fa_1() 9: fa#2(x6, x0) -> fa_1#1(x0) 10: f_x#1(plus(), abfoldr(), x2, x1) -> abfoldr#4(fa(), fb(plus(), x2), Nil(), x1) 11: f#1(plus(), abfoldr(), x1) -> f_x(plus(), abfoldr(), x1) 12: f#2(plus(), abfoldr(), x1, x2) -> f_x#1(plus(), abfoldr(), x1, x2) 13: abfoldr_f_g_acc#1(fa(), x3, Nil(), Acons(x2, x1)) -> fa#2(x2, abfoldr#4(fa(), x3, Nil(), x1)) 14: abfoldr_f_g_acc#1(f(plus(), abfoldr()), x3, Nil(), Acons(x2, x1)) -> f#2(plus(), abfoldr() , x2 , abfoldr#4(f(plus(), abfoldr()) , x3, Nil(), x1)) 15: abfoldr_f_g_acc#1(x5, fb(x3, x4), Nil(), Bcons(x2, x1)) -> fb#2(x3, x4 , x2 , abfoldr#4(x5, fb(x3, x4), Nil(), x1)) 16: abfoldr_f_g_acc#1(x3, g(), Nil(), Bcons(x2, x1)) -> g#2(x2, abfoldr#4(x3, g(), Nil(), x1)) 17: abfoldr_f_g_acc#1(x2, x1, Nil(), Nil()) -> Nil() 18: abfoldr_f_g#1(x2, x1, Nil()) -> abfoldr_f_g_acc(x2, x1, Nil()) 19: abfoldr_f_g#2(x2, x1, Nil(), x3) -> abfoldr_f_g_acc#1(x2, x1, Nil(), x3) 20: abfoldr_f#1(x2, x3) -> abfoldr_f_g(x2, x3) 21: abfoldr_f#2(x2, x3, x4) -> abfoldr_f_g#1(x2, x3, x4) 22: abfoldr_f#3(x2, x3, x4, x5) -> abfoldr_f_g#2(x2, x3, x4, x5) 23: abfoldr#1(x4) -> abfoldr_f(x4) 24: abfoldr#2(x4, x5) -> abfoldr_f#1(x4, x5) 25: abfoldr#3(x4, x5, x6) -> abfoldr_f#2(x4, x5, x6) 26: abfoldr#4(x4, x5, x6, x7) -> abfoldr_f#3(x4, x5, x6, x7) 27: plus_n#1(x2, 0()) -> x2 28: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 29: plus#1(x2) -> plus_n(x2) 30: plus#2(x2, x3) -> plus_n#1(x2, x3) 31: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#3 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f#3 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g_acc#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#1 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#2 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f_x#1 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa#1 :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#2 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb_1#1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#1 :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist g_x#1 :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist 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: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: 1: g_x#1(x5, x6) -> Bcons(x5, x6) 2: g#1(x5) -> g_x(x5) 3: g#2(x5, x6) -> g_x#1(x5, x6) 4: fb_1#1(plus(), x3, x2, x1) -> Bcons(plus#2(x2, x3), x1) 5: fb#1(plus(), x2, x1) -> fb_1(plus(), x2, x1) 6: fb#2(plus(), x2, x1, x3) -> fb_1#1(plus(), x2, x1, x3) 7: fa_1#1(x7) -> bot[0]#1(Not_found()) 8: fa#1(x6) -> fa_1() 9: fa#2(x6, x0) -> fa_1#1(x0) 10: f_x#1(plus(), abfoldr(), x2, x1) -> abfoldr#4(fa(), fb(plus(), x2), Nil(), x1) 11: f#1(plus(), abfoldr(), x1) -> f_x(plus(), abfoldr(), x1) 12: f#2(plus(), abfoldr(), x1, x2) -> f_x#1(plus(), abfoldr(), x1, x2) 13: abfoldr_f_g_acc#1(fa(), x7, Nil(), Acons(x12, x3)) -> fa_1#1(abfoldr#4(fa(), x7, Nil(), x3)) 14: abfoldr_f_g_acc#1(f(plus(), abfoldr()), x3, Nil(), Acons(x2, x1)) -> f#2(plus(), abfoldr() , x2 , abfoldr#4(f(plus(), abfoldr()) , x3, Nil(), x1)) 15: abfoldr_f_g_acc#1(x5, fb(x3, x4), Nil(), Bcons(x2, x1)) -> fb#2(x3, x4 , x2 , abfoldr#4(x5, fb(x3, x4), Nil(), x1)) 16: abfoldr_f_g_acc#1(x3, g(), Nil(), Bcons(x2, x1)) -> g#2(x2, abfoldr#4(x3, g(), Nil(), x1)) 17: abfoldr_f_g_acc#1(x2, x1, Nil(), Nil()) -> Nil() 18: abfoldr_f_g#1(x2, x1, Nil()) -> abfoldr_f_g_acc(x2, x1, Nil()) 19: abfoldr_f_g#2(x2, x1, Nil(), x3) -> abfoldr_f_g_acc#1(x2, x1, Nil(), x3) 20: abfoldr_f#1(x2, x3) -> abfoldr_f_g(x2, x3) 21: abfoldr_f#2(x2, x3, x4) -> abfoldr_f_g#1(x2, x3, x4) 22: abfoldr_f#3(x2, x3, x4, x5) -> abfoldr_f_g#2(x2, x3, x4, x5) 23: abfoldr#1(x4) -> abfoldr_f(x4) 24: abfoldr#2(x4, x5) -> abfoldr_f#1(x4, x5) 25: abfoldr#3(x4, x5, x6) -> abfoldr_f#2(x4, x5, x6) 26: abfoldr#4(x4, x5, x6, x7) -> abfoldr_f#3(x4, x5, x6, x7) 27: plus_n#1(x2, 0()) -> x2 28: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 29: plus#1(x2) -> plus_n(x2) 30: plus#2(x2, x3) -> plus_n#1(x2, x3) 31: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#3 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f#3 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g_acc :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g_acc#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#1 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#2 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f_x :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f_x#1 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa#1 :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1 :: (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#2 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb_1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb_1#1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#1 :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist g_x :: nat -> (nat,nat) ablist -> (nat,nat) ablist g_x#1 :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist 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 = Syntactic} + Details: none * Step 15: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: g_x#1(x5, x6) -> Bcons(x5, x6) 3: g#2(x5, x6) -> g_x#1(x5, x6) 4: fb_1#1(plus(), x3, x2, x1) -> Bcons(plus#2(x2, x3), x1) 6: fb#2(plus(), x2, x1, x3) -> fb_1#1(plus(), x2, x1, x3) 7: fa_1#1(x7) -> bot[0]#1(Not_found()) 10: f_x#1(plus(), abfoldr(), x2, x1) -> abfoldr#4(fa(), fb(plus(), x2), Nil(), x1) 12: f#2(plus(), abfoldr(), x1, x2) -> f_x#1(plus(), abfoldr(), x1, x2) 13: abfoldr_f_g_acc#1(fa(), x7, Nil(), Acons(x12, x3)) -> fa_1#1(abfoldr#4(fa(), x7, Nil(), x3)) 14: abfoldr_f_g_acc#1(f(plus(), abfoldr()), x3, Nil(), Acons(x2, x1)) -> f#2(plus(), abfoldr() , x2 , abfoldr#4(f(plus(), abfoldr()) , x3, Nil(), x1)) 15: abfoldr_f_g_acc#1(x5, fb(x3, x4), Nil(), Bcons(x2, x1)) -> fb#2(x3, x4 , x2 , abfoldr#4(x5, fb(x3, x4), Nil(), x1)) 16: abfoldr_f_g_acc#1(x3, g(), Nil(), Bcons(x2, x1)) -> g#2(x2, abfoldr#4(x3, g(), Nil(), x1)) 17: abfoldr_f_g_acc#1(x2, x1, Nil(), Nil()) -> Nil() 19: abfoldr_f_g#2(x2, x1, Nil(), x3) -> abfoldr_f_g_acc#1(x2, x1, Nil(), x3) 22: abfoldr_f#3(x2, x3, x4, x5) -> abfoldr_f_g#2(x2, x3, x4, x5) 26: abfoldr#4(x4, x5, x6, x7) -> abfoldr_f#3(x4, x5, x6, x7) 27: plus_n#1(x2, 0()) -> x2 28: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 30: plus#2(x2, x3) -> plus_n#1(x2, x3) 31: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f#3 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g_acc#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#2 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f_x#1 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#2 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb_1#1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist g_x#1 :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_n#1 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: 1: g_x#1(x5, x6) -> Bcons(x5, x6) 2: g#2(x10, x12) -> Bcons(x10, x12) 3: fb_1#1(plus(), x3, x2, x1) -> Bcons(plus#2(x2, x3), x1) 4: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2) 5: fa_1#1(x7) -> bot[0]#1(Not_found()) 6: f_x#1(plus(), abfoldr(), x2, x1) -> abfoldr#4(fa(), fb(plus(), x2), Nil(), x1) 7: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2) 8: abfoldr_f_g_acc#1(fa(), x7, Nil(), Acons(x12, x3)) -> fa_1#1(abfoldr#4(fa(), x7, Nil(), x3)) 9: abfoldr_f_g_acc#1(f(plus(), abfoldr()), x7, Nil(), Acons(x2, x3)) -> f_x#1(plus(), abfoldr() , x2 , abfoldr#4(f(plus(), abfoldr()) , x7, Nil(), x3)) 10: abfoldr_f_g_acc#1(x11, fb(plus(), x4), Nil(), Bcons(x2, x3)) -> fb_1#1(plus(), x4 , x2 , abfoldr#4(x11, fb(plus(), x4) , Nil() , x3)) 11: abfoldr_f_g_acc#1(x7, g(), Nil(), Bcons(x10, x3)) -> g_x#1(x10, abfoldr#4(x7, g(), Nil(), x3)) 12: abfoldr_f_g_acc#1(x2, x1, Nil(), Nil()) -> Nil() 13: abfoldr_f_g#2(fa(), x14, Nil(), Acons(x24, x6)) -> fa_1#1(abfoldr#4(fa(), x14, Nil(), x6)) 14: abfoldr_f_g#2(f(plus(), abfoldr()), x6, Nil(), Acons(x4, x2)) -> f#2(plus(), abfoldr() , x4 , abfoldr#4(f(plus(), abfoldr()), x6 , Nil() , x2)) 15: abfoldr_f_g#2(x10, fb(x6, x8), Nil(), Bcons(x4, x2)) -> fb#2(x6, x8 , x4 , abfoldr#4(x10, fb(x6, x8), Nil(), x2)) 16: abfoldr_f_g#2(x6, g(), Nil(), Bcons(x4, x2)) -> g#2(x4, abfoldr#4(x6, g(), Nil(), x2)) 17: abfoldr_f_g#2(x4, x2, Nil(), Nil()) -> Nil() 18: abfoldr_f#3(x4, x2, Nil(), x6) -> abfoldr_f_g_acc#1(x4, x2, Nil(), x6) 19: abfoldr#4(x4, x6, x8, x10) -> abfoldr_f_g#2(x4, x6, x8, x10) 20: plus_n#1(x2, 0()) -> x2 21: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 22: plus#2(x4, 0()) -> x4 23: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 24: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f#3 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g_acc#1 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#2 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f_x#1 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#2 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb_1#1 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist g_x#1 :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_n#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 2: g#2(x10, x12) -> Bcons(x10, x12) 4: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2) 5: fa_1#1(x7) -> bot[0]#1(Not_found()) 7: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2) 13: abfoldr_f_g#2(fa(), x14, Nil(), Acons(x24, x6)) -> fa_1#1(abfoldr#4(fa(), x14, Nil(), x6)) 14: abfoldr_f_g#2(f(plus(), abfoldr()), x6, Nil(), Acons(x4, x2)) -> f#2(plus(), abfoldr() , x4 , abfoldr#4(f(plus(), abfoldr()), x6 , Nil() , x2)) 15: abfoldr_f_g#2(x10, fb(x6, x8), Nil(), Bcons(x4, x2)) -> fb#2(x6, x8 , x4 , abfoldr#4(x10, fb(x6, x8), Nil(), x2)) 16: abfoldr_f_g#2(x6, g(), Nil(), Bcons(x4, x2)) -> g#2(x4, abfoldr#4(x6, g(), Nil(), x2)) 17: abfoldr_f_g#2(x4, x2, Nil(), Nil()) -> Nil() 19: abfoldr#4(x4, x6, x8, x10) -> abfoldr_f_g#2(x4, x6, x8, x10) 22: plus#2(x4, 0()) -> x4 23: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 24: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#2 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#2 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 18: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: 1: g#2(x10, x12) -> Bcons(x10, x12) 2: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2) 3: fa_1#1(x7) -> bot[0]#1(Not_found()) 4: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2) 5: abfoldr_f_g#2(fa(), x14, Nil(), Acons(x24, x6)) -> fa_1#1(abfoldr#4(fa(), x14, Nil(), x6)) 6: abfoldr_f_g#2(f(plus(), abfoldr()), x13, Nil(), Acons(x8, x5)) -> abfoldr#4(fa(), fb(plus(), x8) , Nil() , abfoldr#4(f(plus(), abfoldr()) , x13, Nil(), x5)) 7: abfoldr_f_g#2(x21, fb(plus(), x12), Nil(), Bcons(x8, x5)) -> Bcons(plus#2(x8, x12), abfoldr#4(x21 , fb(plus() , x12) , Nil() , x5)) 8: abfoldr_f_g#2(x13, g(), Nil(), Bcons(x20, x5)) -> Bcons(x20, abfoldr#4(x13, g(), Nil(), x5)) 9: abfoldr_f_g#2(x4, x2, Nil(), Nil()) -> Nil() 10: abfoldr#4(fa(), x28, Nil(), Acons(x48, x12)) -> fa_1#1(abfoldr#4(fa(), x28, Nil(), x12)) 11: abfoldr#4(f(plus(), abfoldr()), x12, Nil(), Acons(x8, x4)) -> f#2(plus(), abfoldr() , x8 , abfoldr#4(f(plus(), abfoldr()), x12 , Nil() , x4)) 12: abfoldr#4(x20, fb(x12, x16), Nil(), Bcons(x8, x4)) -> fb#2(x12, x16 , x8 , abfoldr#4(x20, fb(x12, x16), Nil(), x4)) 13: abfoldr#4(x12, g(), Nil(), Bcons(x8, x4)) -> g#2(x8, abfoldr#4(x12, g(), Nil(), x4)) 14: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil() 15: plus#2(x4, 0()) -> x4 16: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 17: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr_f_g#2 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#2 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#2 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 19: Inline WORST_CASE(?,O(n^3)) + Considered Problem: 1: g#2(x10, x12) -> Bcons(x10, x12) 2: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2) 3: fa_1#1(x7) -> bot[0]#1(Not_found()) 4: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2) 10: abfoldr#4(fa(), x28, Nil(), Acons(x48, x12)) -> fa_1#1(abfoldr#4(fa(), x28, Nil(), x12)) 11: abfoldr#4(f(plus(), abfoldr()), x12, Nil(), Acons(x8, x4)) -> f#2(plus(), abfoldr() , x8 , abfoldr#4(f(plus(), abfoldr()), x12 , Nil() , x4)) 12: abfoldr#4(x20, fb(x12, x16), Nil(), Bcons(x8, x4)) -> fb#2(x12, x16 , x8 , abfoldr#4(x20, fb(x12, x16), Nil(), x4)) 13: abfoldr#4(x12, g(), Nil(), Bcons(x8, x4)) -> g#2(x8, abfoldr#4(x12, g(), Nil(), x4)) 14: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil() 15: plus#2(x4, 0()) -> x4 16: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 17: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#2 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#2 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 20: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: 1: g#2(x10, x12) -> Bcons(x10, x12) 2: fb#2(plus(), x6, x4, x2) -> Bcons(plus#2(x4, x6), x2) 3: fa_1#1(x7) -> bot[0]#1(Not_found()) 4: f#2(plus(), abfoldr(), x4, x2) -> abfoldr#4(fa(), fb(plus(), x4), Nil(), x2) 5: abfoldr#4(fa(), x28, Nil(), Acons(x48, x12)) -> fa_1#1(abfoldr#4(fa(), x28, Nil(), x12)) 6: abfoldr#4(f(plus(), abfoldr()), x25, Nil(), Acons(x8, x9)) -> abfoldr#4(fa(), fb(plus(), x8) , Nil() , abfoldr#4(f(plus(), abfoldr()), x25 , Nil() , x9)) 7: abfoldr#4(x41, fb(plus(), x12), Nil(), Bcons(x8, x9)) -> Bcons(plus#2(x8, x12), abfoldr#4(x41, fb(plus() , x12) , Nil() , x9)) 8: abfoldr#4(x25, g(), Nil(), Bcons(x20, x9)) -> Bcons(x20, abfoldr#4(x25, g(), Nil(), x9)) 9: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil() 10: plus#2(x4, 0()) -> x4 11: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 12: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist f#2 :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist fb#2 :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist g#2 :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 21: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: 3: fa_1#1(x7) -> bot[0]#1(Not_found()) 5: abfoldr#4(fa(), x28, Nil(), Acons(x48, x12)) -> fa_1#1(abfoldr#4(fa(), x28, Nil(), x12)) 6: abfoldr#4(f(plus(), abfoldr()), x25, Nil(), Acons(x8, x9)) -> abfoldr#4(fa(), fb(plus(), x8) , Nil() , abfoldr#4(f(plus(), abfoldr()), x25 , Nil() , x9)) 7: abfoldr#4(x41, fb(plus(), x12), Nil(), Bcons(x8, x9)) -> Bcons(plus#2(x8, x12), abfoldr#4(x41, fb(plus() , x12) , Nil() , x9)) 8: abfoldr#4(x25, g(), Nil(), Bcons(x20, x9)) -> Bcons(x20, abfoldr#4(x25, g(), Nil(), x9)) 9: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil() 10: plus#2(x4, 0()) -> x4 11: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 12: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist Not_found :: Exception S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist bot[0]#1 :: Exception -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa_1#1 :: (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 22: Compression WORST_CASE(?,O(n^3)) + Considered Problem: 3: abfoldr#4(f(plus(), abfoldr()), x25, Nil(), Acons(x8, x9)) -> abfoldr#4(fa(), fb(plus(), x8) , Nil() , abfoldr#4(f(plus(), abfoldr()), x25 , Nil() , x9)) 4: abfoldr#4(x41, fb(plus(), x12), Nil(), Bcons(x8, x9)) -> Bcons(plus#2(x8, x12), abfoldr#4(x41, fb(plus() , x12) , Nil() , x9)) 5: abfoldr#4(x25, g(), Nil(), Bcons(x20, x9)) -> Bcons(x20, abfoldr#4(x25, g(), Nil(), x9)) 6: abfoldr#4(x8, x4, Nil(), Nil()) -> Nil() 7: plus#2(x4, 0()) -> x4 8: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 9: main(x1) -> abfoldr#4(f(plus(), abfoldr()), g(), Nil(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist S :: nat -> nat abfoldr :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist f :: (nat -> nat -> nat) -> ((nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist -> (nat,nat) ablist) -> nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: (nat -> nat -> nat) -> nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Compression + Details: none * Step 23: ToTctProblem WORST_CASE(?,O(n^3)) + Considered Problem: 1: abfoldr#4(f(), x25, Acons(x8, x9)) -> abfoldr#4(fa(), fb(x8), abfoldr#4(f(), x25, x9)) 2: abfoldr#4(x41, fb(x12), Bcons(x8, x9)) -> Bcons(plus#2(x8, x12), abfoldr#4(x41, fb(x12), x9)) 3: abfoldr#4(x25, g(), Bcons(x20, x9)) -> Bcons(x20, abfoldr#4(x25, g(), x9)) 4: abfoldr#4(x8, x4, Nil()) -> Nil() 5: plus#2(x4, 0()) -> x4 6: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 7: main(x1) -> abfoldr#4(f(), g(), x1) where 0 :: nat Acons :: 'a -> ('a,'b) ablist -> ('a,'b) ablist Bcons :: 'b -> ('a,'b) ablist -> ('a,'b) ablist Nil :: ('a,'b) ablist S :: nat -> nat abfoldr#4 :: (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat -> (nat,nat) ablist -> (nat,nat) ablist) -> (nat,nat) ablist -> (nat,nat) ablist f :: nat -> (nat,nat) ablist -> (nat,nat) ablist fa :: nat -> (nat,nat) ablist -> (nat,nat) ablist fb :: nat -> nat -> (nat,nat) ablist -> (nat,nat) ablist g :: nat -> (nat,nat) ablist -> (nat,nat) ablist main :: (nat,nat) ablist -> (nat,nat) ablist plus#2 :: nat -> nat -> nat + Applied Processor: ToTctProblem + Details: none * Step 24: DependencyPairs WORST_CASE(?,O(n^3)) + Considered Problem: - Strict TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1,g/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: DependencyPairs {dpKind_ = DT} + Details: We add the following dependency tuples: Strict DPs abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(x8,x4,Nil()) -> c_3() abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) 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 25: PredecessorEstimation WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(x8,x4,Nil()) -> c_3() abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,0()) -> c_6() plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: PredecessorEstimation {onSelection = all simple predecessor estimation selector} + Details: We estimate the number of application of {3,6} by application of Pre({3,6}) = {1,2,4,5,7}. Here rules are labelled as follows: 1: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) 2: abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) 3: abfoldr#4#(x8,x4,Nil()) -> c_3() 4: abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) 5: main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) 6: plus#2#(x4,0()) -> c_6() 7: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) * Step 26: RemoveWeakSuffixes WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: abfoldr#4#(x8,x4,Nil()) -> c_3() plus#2#(x4,0()) -> c_6() - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: RemoveWeakSuffixes + Details: Consider the dependency graph 1:S:abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) -->_1 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)):3 -->_1 abfoldr#4#(x8,x4,Nil()) -> c_3():6 -->_1 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1 2:S:abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) -->_1 plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)):5 -->_2 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)):3 -->_1 plus#2#(x4,0()) -> c_6():7 -->_2 abfoldr#4#(x8,x4,Nil()) -> c_3():6 -->_2 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2 3:S:abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) -->_2 abfoldr#4#(x8,x4,Nil()) -> c_3():6 -->_1 abfoldr#4#(x8,x4,Nil()) -> c_3():6 -->_2 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)):3 -->_2 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2 -->_1 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2 -->_2 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1 4:S:main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(x8,x4,Nil()) -> c_3():6 -->_1 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)):3 -->_1 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1 5: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)):5 6:W:abfoldr#4#(x8,x4,Nil()) -> c_3() 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. 7: plus#2#(x4,0()) -> c_6() 6: abfoldr#4#(x8,x4,Nil()) -> c_3() * Step 27: UsableRules WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) main(x1) -> abfoldr#4(f(),g(),x1) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: UsableRules + Details: We replace rewrite rules by usable rules: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) * Step 28: DecomposeDG WORST_CASE(?,O(n^3)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: DecomposeDG {onSelection = all below first cut in WDG, onUpper = Nothing, onLower = Nothing} + Details: We decompose the input problem according to the dependency graph into the upper component abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) 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. abfoldr#4#(x25,g(),Bcons(x20,x9)) -> abfoldr#4#(x25,g(),x9) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> abfoldr#4#(x41,fb(x12),x9) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> plus#2#(x8,x12) abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(f(),x25,x9) abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) main#(x1) -> abfoldr#4#(f(),g(),x1) ** Step 28.a:1: SimplifyRHS WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: SimplifyRHS + Details: Consider the dependency graph 1:S:abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) -->_1 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)):3 -->_1 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1 2:S:abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)) -->_2 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)):3 -->_2 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2 3:S:abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) -->_2 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)):3 -->_2 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2 -->_1 abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(plus#2#(x8,x12),abfoldr#4#(x41,fb(x12),x9)):2 -->_2 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1 4:S:main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) -->_1 abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)):3 -->_1 abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)):1 Due to missing edges in the depndency graph, the right-hand sides of following rules could be simplified: abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9)) ** Step 28.a:2: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,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(c_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1,2}, uargs(c_5) = {1} Following symbols are considered usable: {abfoldr#4#,main#} TcT has computed the following interpretation: p(0) = [0] p(Acons) = [1] x1 + [1] x2 + [0] p(Bcons) = [1] x1 + [1] x2 + [0] p(Nil) = [0] p(S) = [1] x1 + [0] p(abfoldr#4) = [0] p(f) = [0] p(fa) = [0] p(fb) = [0] p(g) = [0] p(main) = [0] p(plus#2) = [0] p(abfoldr#4#) = [0] p(main#) = [1] p(plus#2#) = [0] p(c_1) = [4] x1 + [0] p(c_2) = [4] x1 + [0] p(c_3) = [0] p(c_4) = [1] x1 + [4] x2 + [0] p(c_5) = [2] x1 + [0] p(c_6) = [0] p(c_7) = [0] Following rules are strictly oriented: main#(x1) = [1] > [0] = c_5(abfoldr#4#(f(),g(),x1)) Following rules are (at-least) weakly oriented: abfoldr#4#(x25,g(),Bcons(x20,x9)) = [0] >= [0] = c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) = [0] >= [0] = c_2(abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) = [0] >= [0] = c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)),abfoldr#4#(f(),x25,x9)) ** Step 28.a:3: NaturalMI WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) - Weak DPs: main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,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(c_1) = {1}, uargs(c_2) = {1}, uargs(c_4) = {1,2}, uargs(c_5) = {1} Following symbols are considered usable: {abfoldr#4,abfoldr#4#,main#} TcT has computed the following interpretation: p(0) = [2] p(Acons) = [1] x1 + [1] x2 + [1] p(Bcons) = [1] x2 + [0] p(Nil) = [0] p(S) = [4] p(abfoldr#4) = [0] p(f) = [0] p(fa) = [4] p(fb) = [1] x1 + [2] p(g) = [8] p(main) = [1] x1 + [2] p(plus#2) = [3] x2 + [8] p(abfoldr#4#) = [2] x3 + [0] p(main#) = [3] x1 + [5] p(plus#2#) = [1] x1 + [1] x2 + [2] p(c_1) = [1] x1 + [0] p(c_2) = [1] x1 + [0] p(c_3) = [1] p(c_4) = [1] x1 + [1] x2 + [0] p(c_5) = [1] x1 + [5] p(c_6) = [0] p(c_7) = [1] x1 + [0] Following rules are strictly oriented: abfoldr#4#(f(),x25,Acons(x8,x9)) = [2] x8 + [2] x9 + [2] > [2] x9 + [0] = c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)),abfoldr#4#(f(),x25,x9)) Following rules are (at-least) weakly oriented: abfoldr#4#(x25,g(),Bcons(x20,x9)) = [2] x9 + [0] >= [2] x9 + [0] = c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) = [2] x9 + [0] >= [2] x9 + [0] = c_2(abfoldr#4#(x41,fb(x12),x9)) main#(x1) = [3] x1 + [5] >= [2] x1 + [5] = c_5(abfoldr#4#(f(),g(),x1)) abfoldr#4(x25,g(),Bcons(x20,x9)) = [0] >= [0] = Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) = [0] >= [0] = Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) = [0] >= [0] = Nil() abfoldr#4(f(),x25,Acons(x8,x9)) = [0] >= [0] = abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ** Step 28.a:4: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9)) - Weak DPs: abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(0, 0) F (TrsFun "Acons") :: ["A"(2, 0) x "A"(2, 0)] -(0)-> "A"(2, 0) F (TrsFun "Acons") :: ["A"(2, 0) x "A"(4, 2)] -(0)-> "A"(2, 2) F (TrsFun "Bcons") :: ["A"(0, 0) x "A"(2, 2)] -(2)-> "A"(2, 2) F (TrsFun "Bcons") :: ["A"(0, 0) x "A"(2, 0)] -(2)-> "A"(2, 0) F (TrsFun "Bcons") :: ["A"(0, 0) x "A"(2, 4)] -(2)-> "A"(2, 4) F (TrsFun "Nil") :: [] -(0)-> "A"(2, 0) F (TrsFun "Nil") :: [] -(0)-> "A"(8, 8) F (TrsFun "S") :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (TrsFun "S") :: ["A"(0, 0)] -(0)-> "A"(12, 4) F (TrsFun "abfoldr#4") :: ["A"(0, 0) x "A"(0, 0) x "A"(2, 0)] -(0)-> "A"(2, 4) F (TrsFun "f") :: [] -(0)-> "A"(0, 0) F (TrsFun "f") :: [] -(0)-> "A"(9, 1) F (TrsFun "f") :: [] -(0)-> "A"(12, 12) F (TrsFun "f") :: [] -(0)-> "A"(12, 8) F (TrsFun "fa") :: [] -(0)-> "A"(12, 12) F (TrsFun "fb") :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (TrsFun "fb") :: ["A"(0, 0)] -(0)-> "A"(9, 8) F (TrsFun "fb") :: ["A"(0, 0)] -(0)-> "A"(5, 5) F (TrsFun "fb") :: ["A"(0, 0)] -(0)-> "A"(8, 8) F (TrsFun "fb") :: ["A"(0, 0)] -(0)-> "A"(7, 0) F (TrsFun "g") :: [] -(0)-> "A"(0, 0) F (TrsFun "g") :: [] -(0)-> "A"(12, 8) F (TrsFun "g") :: [] -(0)-> "A"(12, 12) F (TrsFun "g") :: [] -(0)-> "A"(14, 8) F (TrsFun "plus#2") :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 0) F (DpFun "abfoldr#4") :: ["A"(9, 1) x "A"(0, 0) x "A"(2, 2)] -(0)-> "A"(10, 0) F (DpFun "main") :: ["A"(14, 14)] -(14)-> "A"(0, 2) F (ComFun 1) :: ["A"(10, 0)] -(0)-> "A"(14, 10) F (ComFun 2) :: ["A"(0, 0)] -(0)-> "A"(13, 13) F (ComFun 4) :: ["A"(3, 0) x "A"(0, 0)] -(0)-> "A"(11, 3) F (ComFun 5) :: ["A"(8, 0)] -(2)-> "A"(2, 8) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 1)_A" :: ["A"(1, 0)] -(0)-> "A"(0, 1) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 4)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 4)_A" :: ["A"(1, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 5)_A" :: ["A"(0, 0)] -(1)-> "A"(1, 0) "F (ComFun 5)_A" :: ["A"(1, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"Acons\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Acons\")_A" :: ["A"(0, 0) x "A"(1, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Bcons\")_A" :: ["A"(0, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Bcons\")_A" :: ["A"(0, 0) x "A"(0, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"S\")_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"S\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"f\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"f\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"fa\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"fa\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"fb\")_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"fb\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"g\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"g\")_A" :: [] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9)) 2. Weak: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) ** Step 28.a:5: Ara WORST_CASE(?,O(n^2)) + Considered Problem: - Strict DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) - Weak DPs: abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> c_2(abfoldr#4#(x41,fb(x12),x9)) abfoldr#4#(f(),x25,Acons(x8,x9)) -> c_4(abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ,abfoldr#4#(f(),x25,x9)) main#(x1) -> c_5(abfoldr#4#(f(),g(),x1)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/1,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: Ara {minDegree = 1, maxDegree = 2, araTimeout = 8, araRuleShifting = Just 1} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(0, 0) F (TrsFun "Acons") :: ["A"(2, 0) x "A"(2, 0)] -(0)-> "A"(2, 0) F (TrsFun "Acons") :: ["A"(2, 0) x "A"(12, 10)] -(10)-> "A"(2, 10) F (TrsFun "Bcons") :: ["A"(2, 0) x "A"(2, 10)] -(2)-> "A"(2, 10) F (TrsFun "Bcons") :: ["A"(2, 0) x "A"(2, 0)] -(2)-> "A"(2, 0) F (TrsFun "Bcons") :: ["A"(2, 0) x "A"(2, 14)] -(2)-> "A"(2, 14) F (TrsFun "Nil") :: [] -(0)-> "A"(2, 0) F (TrsFun "Nil") :: [] -(0)-> "A"(12, 14) F (TrsFun "S") :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (TrsFun "S") :: ["A"(0, 0)] -(0)-> "A"(9, 1) F (TrsFun "abfoldr#4") :: ["A"(9, 1) x "A"(0, 0) x "A"(2, 0)] -(0)-> "A"(2, 14) F (TrsFun "f") :: [] -(0)-> "A"(9, 1) F (TrsFun "f") :: [] -(0)-> "A"(9, 8) F (TrsFun "f") :: [] -(0)-> "A"(12, 12) F (TrsFun "f") :: [] -(0)-> "A"(12, 8) F (TrsFun "fa") :: [] -(0)-> "A"(14, 12) F (TrsFun "fa") :: [] -(0)-> "A"(12, 12) F (TrsFun "fb") :: ["A"(0, 0)] -(0)-> "A"(0, 0) F (TrsFun "fb") :: ["A"(0, 0)] -(2)-> "A"(0, 2) F (TrsFun "fb") :: ["A"(0, 0)] -(0)-> "A"(8, 0) F (TrsFun "fb") :: ["A"(0, 0)] -(4)-> "A"(0, 4) F (TrsFun "g") :: [] -(0)-> "A"(0, 2) F (TrsFun "g") :: [] -(0)-> "A"(0, 0) F (TrsFun "g") :: [] -(0)-> "A"(12, 12) F (TrsFun "plus#2") :: ["A"(2, 0) x "A"(0, 0)] -(0)-> "A"(2, 0) F (DpFun "abfoldr#4") :: ["A"(9, 8) x "A"(0, 2) x "A"(2, 10)] -(1)-> "A"(0, 9) F (DpFun "main") :: ["A"(14, 14)] -(15)-> "A"(0, 0) F (ComFun 1) :: ["A"(0, 0)] -(0)-> "A"(4, 12) F (ComFun 2) :: ["A"(0, 0)] -(0)-> "A"(0, 14) F (ComFun 4) :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(4, 12) F (ComFun 5) :: ["A"(0, 0)] -(1)-> "A"(1, 15) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 1)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 2)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 4)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(1, 0) "F (ComFun 4)_A" :: ["A"(0, 0) x "A"(0, 0)] -(0)-> "A"(0, 1) "F (ComFun 5)_A" :: ["A"(0, 0)] -(1)-> "A"(1, 0) "F (ComFun 5)_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"0\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"Acons\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"Acons\")_A" :: ["A"(0, 0) x "A"(1, 1)] -(1)-> "A"(0, 1) "F (TrsFun \"Bcons\")_A" :: ["A"(1, 0) x "A"(1, 0)] -(1)-> "A"(1, 0) "F (TrsFun \"Bcons\")_A" :: ["A"(0, 0) x "A"(0, 1)] -(0)-> "A"(0, 1) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"Nil\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"S\")_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"S\")_A" :: ["A"(0, 0)] -(0)-> "A"(0, 1) "F (TrsFun \"f\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"f\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"fa\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"fa\")_A" :: [] -(0)-> "A"(0, 1) "F (TrsFun \"fb\")_A" :: ["A"(0, 0)] -(0)-> "A"(1, 0) "F (TrsFun \"fb\")_A" :: ["A"(0, 0)] -(1)-> "A"(0, 1) "F (TrsFun \"g\")_A" :: [] -(0)-> "A"(1, 0) "F (TrsFun \"g\")_A" :: [] -(0)-> "A"(0, 1) Following Still Strict Rules were Typed as: ------------------------------------------- 1. Strict: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> c_1(abfoldr#4#(x25,g(),x9)) 2. Weak: ** Step 28.b:1: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict DPs: plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> abfoldr#4#(x25,g(),x9) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> abfoldr#4#(x41,fb(x12),x9) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> plus#2#(x8,x12) abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(f(),x25,x9) abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) main#(x1) -> abfoldr#4#(f(),g(),x1) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,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(c_7) = {1} Following symbols are considered usable: {abfoldr#4,abfoldr#4#,main#,plus#2#} TcT has computed the following interpretation: p(0) = [0] p(Acons) = [1] x1 + [1] x2 + [0] p(Bcons) = [1] x2 + [0] p(Nil) = [0] p(S) = [1] x1 + [8] p(abfoldr#4) = [0] p(f) = [2] p(fa) = [1] p(fb) = [2] x1 + [2] p(g) = [1] p(main) = [1] x1 + [2] p(plus#2) = [0] p(abfoldr#4#) = [2] x1 + [1] x2 + [2] x3 + [7] p(main#) = [2] x1 + [14] p(plus#2#) = [1] x2 + [0] p(c_1) = [0] p(c_2) = [0] p(c_3) = [0] p(c_4) = [0] p(c_5) = [0] p(c_6) = [0] p(c_7) = [1] x1 + [7] Following rules are strictly oriented: plus#2#(x4,S(x2)) = [1] x2 + [8] > [1] x2 + [7] = c_7(plus#2#(x4,x2)) Following rules are (at-least) weakly oriented: abfoldr#4#(x25,g(),Bcons(x20,x9)) = [2] x25 + [2] x9 + [8] >= [2] x25 + [2] x9 + [8] = abfoldr#4#(x25,g(),x9) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) = [2] x12 + [2] x41 + [2] x9 + [9] >= [2] x12 + [2] x41 + [2] x9 + [9] = abfoldr#4#(x41,fb(x12),x9) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) = [2] x12 + [2] x41 + [2] x9 + [9] >= [1] x12 + [0] = plus#2#(x8,x12) abfoldr#4#(f(),x25,Acons(x8,x9)) = [1] x25 + [2] x8 + [2] x9 + [11] >= [1] x25 + [2] x9 + [11] = abfoldr#4#(f(),x25,x9) abfoldr#4#(f(),x25,Acons(x8,x9)) = [1] x25 + [2] x8 + [2] x9 + [11] >= [2] x8 + [11] = abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) main#(x1) = [2] x1 + [14] >= [2] x1 + [12] = abfoldr#4#(f(),g(),x1) abfoldr#4(x25,g(),Bcons(x20,x9)) = [0] >= [0] = Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) = [0] >= [0] = Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) = [0] >= [0] = Nil() abfoldr#4(f(),x25,Acons(x8,x9)) = [0] >= [0] = abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) ** Step 28.b:2: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak DPs: abfoldr#4#(x25,g(),Bcons(x20,x9)) -> abfoldr#4#(x25,g(),x9) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> abfoldr#4#(x41,fb(x12),x9) abfoldr#4#(x41,fb(x12),Bcons(x8,x9)) -> plus#2#(x8,x12) abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(f(),x25,x9) abfoldr#4#(f(),x25,Acons(x8,x9)) -> abfoldr#4#(fa(),fb(x8),abfoldr#4(f(),x25,x9)) main#(x1) -> abfoldr#4#(f(),g(),x1) plus#2#(x4,S(x2)) -> c_7(plus#2#(x4,x2)) - Weak TRS: abfoldr#4(x25,g(),Bcons(x20,x9)) -> Bcons(x20,abfoldr#4(x25,g(),x9)) abfoldr#4(x41,fb(x12),Bcons(x8,x9)) -> Bcons(plus#2(x8,x12),abfoldr#4(x41,fb(x12),x9)) abfoldr#4(x8,x4,Nil()) -> Nil() abfoldr#4(f(),x25,Acons(x8,x9)) -> abfoldr#4(fa(),fb(x8),abfoldr#4(f(),x25,x9)) plus#2(x4,0()) -> x4 plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) - Signature: {abfoldr#4/3,main/1,plus#2/2,abfoldr#4#/3,main#/1,plus#2#/2} / {0/0,Acons/2,Bcons/2,Nil/0,S/1,f/0,fa/0,fb/1 ,g/0,c_1/1,c_2/2,c_3/0,c_4/2,c_5/1,c_6/0,c_7/1} - Obligation: innermost runtime complexity wrt. defined symbols {main#} and constructors {0,Acons,Bcons,Nil,S} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^3))