WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: (* flatten example from 'Static Determination of Quantitative Resource Usage for Higher-Order Programs' by Jost et. al. *) type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree ;; type 'a list = Nil | Cons of 'a * 'a list ;; let cons x xs = Cons(x,xs) ;; let rec dfsAcc g t acc = match t with | Leaf(x) -> g x acc | Node(t1,t2) -> dfsAcc g t2 (dfsAcc g t1 acc) ;; let rec revApp l acc = match l with | Nil -> acc | Cons(y,ys) -> revApp ys Cons(y,acc) ;; let flatten t = revApp (dfsAcc cons t Nil) Nil ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λt : 'a48 tree. (λcons : 'a48 -> 'a48 list -> 'a48 list. (λdfsAcc : ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list. (λrevApp : 'a48 list -> 'a48 list -> 'a48 list. (λflatten : 'a48 tree -> 'a48 list. flatten t) (λt : 'a48 tree. revApp (dfsAcc cons t Nil) Nil)) (μrevApp : 'a48 list -> 'a48 list -> 'a48 list. λl : 'a48 list. λacc : 'a48 list. case l of | Nil -> acc | Cons -> λy : 'a48. λys : 'a48 list. revApp ys Cons(y,acc))) (μdfsAcc : ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list. λg : 'a48 -> 'a48 list -> 'a48 list. λt : 'a48 tree. λacc : 'a48 list. case t of | Leaf -> λx : 'a48. g x acc | Node -> λt1 : 'a48 tree. λt2 : 'a48 tree. dfsAcc g t2 (dfsAcc g t1 acc))) (λx : 'a48. λxs : 'a48 list. Cons(x,xs)) : 'a48 tree -> 'a48 list where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x1, x2, x3) x4 -> x3 (x2 x1 x4 Nil()) Nil() 3: main_3(x0, x1, x2) x3 -> main_4(x0) flatten(x1, x2, x3) 4: cond_revApp_l_acc(Nil(), x4) -> x4 5: cond_revApp_l_acc(Cons(x5, x6), x4) -> revApp() x6 Cons(x5, x4) 6: revApp_l(x3) x4 -> cond_revApp_l_acc(x3, x4) 7: revApp_1() x3 -> revApp_l(x3) 8: revApp() x0 -> revApp_1() x0 9: main_2(x0, x1) x2 -> main_3(x0, x1, x2) revApp() 10: cond_dfsAcc_g_t_acc(Leaf(x5), x2, x4) -> x2 x5 x4 11: cond_dfsAcc_g_t_acc(Node(x5, x6), x2, x4) -> dfsAcc() x2 x6 (dfsAcc() x2 x5 x4) 12: dfsAcc_g_t(x2, x3) x4 -> cond_dfsAcc_g_t_acc(x3, x2, x4) 13: dfsAcc_g(x2) x3 -> dfsAcc_g_t(x2, x3) 14: dfsAcc_1() x2 -> dfsAcc_g(x2) 15: dfsAcc() x0 -> dfsAcc_1() x0 16: main_1(x0) x1 -> main_2(x0, x1) dfsAcc() 17: cons_x(x1) x2 -> Cons(x1, x2) 18: cons() x1 -> cons_x(x1) 19: main(x0) -> main_1(x0) cons() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list flatten :: ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main_1 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list revApp_1 :: 'a48 list -> 'a48 list -> 'a48 list main_2 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> 'a48 list main_3 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 list main_4 :: 'a48 tree -> ('a48 tree -> 'a48 list) -> 'a48 list cond_revApp_l_acc :: 'a48 list -> 'a48 list -> 'a48 list cond_dfsAcc_g_t_acc :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x1, x2, x3) x4 -> x3 (x2 x1 x4 Nil()) Nil() 3: main_3(x0, x3, x5) x7 -> flatten(x3, x5, x7) x0 4: cond_revApp_l_acc(Nil(), x4) -> x4 5: cond_revApp_l_acc(Cons(x5, x6), x4) -> revApp() x6 Cons(x5, x4) 6: revApp_l(x3) x4 -> cond_revApp_l_acc(x3, x4) 7: revApp_1() x3 -> revApp_l(x3) 8: revApp() x6 -> revApp_l(x6) 9: main_2(x0, x2) x4 -> main_4(x0) flatten(x2, x4, revApp()) 10: cond_dfsAcc_g_t_acc(Leaf(x5), x2, x4) -> x2 x5 x4 11: cond_dfsAcc_g_t_acc(Node(x5, x6), x2, x4) -> dfsAcc() x2 x6 (dfsAcc() x2 x5 x4) 12: dfsAcc_g_t(x2, x3) x4 -> cond_dfsAcc_g_t_acc(x3, x2, x4) 13: dfsAcc_g(x2) x3 -> dfsAcc_g_t(x2, x3) 14: dfsAcc_1() x2 -> dfsAcc_g(x2) 15: dfsAcc() x4 -> dfsAcc_g(x4) 16: main_1(x0) x2 -> main_3(x0, x2, dfsAcc()) revApp() 17: cons_x(x1) x2 -> Cons(x1, x2) 18: cons() x1 -> cons_x(x1) 19: main(x0) -> main_2(x0, cons()) dfsAcc() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list flatten :: ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main_1 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list revApp_1 :: 'a48 list -> 'a48 list -> 'a48 list main_2 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> 'a48 list main_3 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 list main_4 :: 'a48 tree -> ('a48 tree -> 'a48 list) -> 'a48 list cond_revApp_l_acc :: 'a48 list -> 'a48 list -> 'a48 list cond_dfsAcc_g_t_acc :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x1, x2, x3) x4 -> x3 (x2 x1 x4 Nil()) Nil() 3: main_3(x8, x2, x4) x6 -> x6 (x4 x2 x8 Nil()) Nil() 4: cond_revApp_l_acc(Nil(), x4) -> x4 5: cond_revApp_l_acc(Cons(x5, x6), x4) -> revApp() x6 Cons(x5, x4) 6: revApp_l(x3) x4 -> cond_revApp_l_acc(x3, x4) 7: revApp_1() x3 -> revApp_l(x3) 8: revApp() x6 -> revApp_l(x6) 9: main_2(x0, x5) x9 -> flatten(x5, x9, revApp()) x0 10: cond_dfsAcc_g_t_acc(Leaf(x5), x2, x4) -> x2 x5 x4 11: cond_dfsAcc_g_t_acc(Node(x5, x6), x2, x4) -> dfsAcc() x2 x6 (dfsAcc() x2 x5 x4) 12: dfsAcc_g_t(x2, x3) x4 -> cond_dfsAcc_g_t_acc(x3, x2, x4) 13: dfsAcc_g(x2) x3 -> dfsAcc_g_t(x2, x3) 14: dfsAcc_1() x2 -> dfsAcc_g(x2) 15: dfsAcc() x4 -> dfsAcc_g(x4) 16: main_1(x0) x6 -> flatten(x6, dfsAcc(), revApp()) x0 17: cons_x(x1) x2 -> Cons(x1, x2) 18: cons() x1 -> cons_x(x1) 19: main(x0) -> main_4(x0) flatten(cons(), dfsAcc(), revApp()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list flatten :: ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main_1 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list revApp_1 :: 'a48 list -> 'a48 list -> 'a48 list main_2 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> 'a48 list main_3 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 list main_4 :: 'a48 tree -> ('a48 tree -> 'a48 list) -> 'a48 list cond_revApp_l_acc :: 'a48 list -> 'a48 list -> 'a48 list cond_dfsAcc_g_t_acc :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x1, x2, x3) x4 -> x3 (x2 x1 x4 Nil()) Nil() 3: main_3(x8, x2, x4) x6 -> x6 (x4 x2 x8 Nil()) Nil() 4: cond_revApp_l_acc(Nil(), x4) -> x4 5: cond_revApp_l_acc(Cons(x5, x6), x4) -> revApp() x6 Cons(x5, x4) 6: revApp_l(x3) x4 -> cond_revApp_l_acc(x3, x4) 7: revApp_1() x3 -> revApp_l(x3) 8: revApp() x6 -> revApp_l(x6) 9: main_2(x8, x2) x4 -> revApp() (x4 x2 x8 Nil()) Nil() 10: cond_dfsAcc_g_t_acc(Leaf(x5), x2, x4) -> x2 x5 x4 11: cond_dfsAcc_g_t_acc(Node(x5, x6), x2, x4) -> dfsAcc() x2 x6 (dfsAcc() x2 x5 x4) 12: dfsAcc_g_t(x2, x3) x4 -> cond_dfsAcc_g_t_acc(x3, x2, x4) 13: dfsAcc_g(x2) x3 -> dfsAcc_g_t(x2, x3) 14: dfsAcc_1() x2 -> dfsAcc_g(x2) 15: dfsAcc() x4 -> dfsAcc_g(x4) 16: main_1(x8) x2 -> revApp() (dfsAcc() x2 x8 Nil()) Nil() 17: cons_x(x1) x2 -> Cons(x1, x2) 18: cons() x1 -> cons_x(x1) 19: main(x0) -> flatten(cons(), dfsAcc(), revApp()) x0 where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list flatten :: ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main_1 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list revApp_1 :: 'a48 list -> 'a48 list -> 'a48 list main_2 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> 'a48 list main_3 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 list main_4 :: 'a48 tree -> ('a48 tree -> 'a48 list) -> 'a48 list cond_revApp_l_acc :: 'a48 list -> 'a48 list -> 'a48 list cond_dfsAcc_g_t_acc :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x1, x2, x3) x4 -> x3 (x2 x1 x4 Nil()) Nil() 3: main_3(x8, x2, x4) x6 -> x6 (x4 x2 x8 Nil()) Nil() 4: cond_revApp_l_acc(Nil(), x4) -> x4 5: cond_revApp_l_acc(Cons(x5, x6), x4) -> revApp() x6 Cons(x5, x4) 6: revApp_l(x3) x4 -> cond_revApp_l_acc(x3, x4) 7: revApp_1() x3 -> revApp_l(x3) 8: revApp() x6 -> revApp_l(x6) 9: main_2(x8, x2) x4 -> revApp() (x4 x2 x8 Nil()) Nil() 10: cond_dfsAcc_g_t_acc(Leaf(x5), x2, x4) -> x2 x5 x4 11: cond_dfsAcc_g_t_acc(Node(x5, x6), x2, x4) -> dfsAcc() x2 x6 (dfsAcc() x2 x5 x4) 12: dfsAcc_g_t(x2, x3) x4 -> cond_dfsAcc_g_t_acc(x3, x2, x4) 13: dfsAcc_g(x2) x3 -> dfsAcc_g_t(x2, x3) 14: dfsAcc_1() x2 -> dfsAcc_g(x2) 15: dfsAcc() x4 -> dfsAcc_g(x4) 16: main_1(x8) x2 -> revApp() (dfsAcc() x2 x8 Nil()) Nil() 17: cons_x(x1) x2 -> Cons(x1, x2) 18: cons() x1 -> cons_x(x1) 19: main(x8) -> revApp() (dfsAcc() cons() x8 Nil()) Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list flatten :: ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main_1 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list revApp_1 :: 'a48 list -> 'a48 list -> 'a48 list main_2 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> 'a48 list main_3 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 list main_4 :: 'a48 tree -> ('a48 tree -> 'a48 list) -> 'a48 list cond_revApp_l_acc :: 'a48 list -> 'a48 list -> 'a48 list cond_dfsAcc_g_t_acc :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x1, x2, x3) x4 -> x3 (x2 x1 x4 Nil()) Nil() 3: main_3(x8, x2, x4) x6 -> x6 (x4 x2 x8 Nil()) Nil() 4: cond_revApp_l_acc(Nil(), x4) -> x4 5: cond_revApp_l_acc(Cons(x5, x6), x4) -> revApp() x6 Cons(x5, x4) 6: revApp_l(Nil()) x8 -> x8 7: revApp_l(Cons(x10, x12)) x8 -> revApp() x12 Cons(x10, x8) 8: revApp_1() x3 -> revApp_l(x3) 9: revApp() x6 -> revApp_l(x6) 10: main_2(x8, x2) x4 -> revApp() (x4 x2 x8 Nil()) Nil() 11: cond_dfsAcc_g_t_acc(Leaf(x5), x2, x4) -> x2 x5 x4 12: cond_dfsAcc_g_t_acc(Node(x5, x6), x2, x4) -> dfsAcc() x2 x6 (dfsAcc() x2 x5 x4) 13: dfsAcc_g_t(x4, Leaf(x10)) x8 -> x4 x10 x8 14: dfsAcc_g_t(x4, Node(x10, x12)) x8 -> dfsAcc() x4 x12 (dfsAcc() x4 x10 x8) 15: dfsAcc_g(x2) x3 -> dfsAcc_g_t(x2, x3) 16: dfsAcc_1() x2 -> dfsAcc_g(x2) 17: dfsAcc() x4 -> dfsAcc_g(x4) 18: main_1(x8) x2 -> revApp() (dfsAcc() x2 x8 Nil()) Nil() 19: cons_x(x1) x2 -> Cons(x1, x2) 20: cons() x1 -> cons_x(x1) 21: main(x8) -> revApp() (dfsAcc() cons() x8 Nil()) Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list flatten :: ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main_1 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list revApp_1 :: 'a48 list -> 'a48 list -> 'a48 list main_2 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> 'a48 list main_3 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 list main_4 :: 'a48 tree -> ('a48 tree -> 'a48 list) -> 'a48 list cond_revApp_l_acc :: 'a48 list -> 'a48 list -> 'a48 list cond_dfsAcc_g_t_acc :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x1, x2, x3) x4 -> x3 (x2 x1 x4 Nil()) Nil() 3: main_3(x8, x2, x4) x6 -> x6 (x4 x2 x8 Nil()) Nil() 6: revApp_l(Nil()) x8 -> x8 7: revApp_l(Cons(x10, x12)) x8 -> revApp() x12 Cons(x10, x8) 8: revApp_1() x3 -> revApp_l(x3) 9: revApp() x6 -> revApp_l(x6) 10: main_2(x8, x2) x4 -> revApp() (x4 x2 x8 Nil()) Nil() 13: dfsAcc_g_t(x4, Leaf(x10)) x8 -> x4 x10 x8 14: dfsAcc_g_t(x4, Node(x10, x12)) x8 -> dfsAcc() x4 x12 (dfsAcc() x4 x10 x8) 15: dfsAcc_g(x2) x3 -> dfsAcc_g_t(x2, x3) 16: dfsAcc_1() x2 -> dfsAcc_g(x2) 17: dfsAcc() x4 -> dfsAcc_g(x4) 18: main_1(x8) x2 -> revApp() (dfsAcc() x2 x8 Nil()) Nil() 19: cons_x(x1) x2 -> Cons(x1, x2) 20: cons() x1 -> cons_x(x1) 21: main(x8) -> revApp() (dfsAcc() cons() x8 Nil()) Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list flatten :: ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main_1 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list revApp_1 :: 'a48 list -> 'a48 list -> 'a48 list main_2 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> 'a48 list main_3 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 list main_4 :: 'a48 tree -> ('a48 tree -> 'a48 list) -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_4(x0) x4 -> x4 x0 2: flatten(x1, x2, x3) x4 -> x3 (x2 x1 x4 Nil()) Nil() 3: main_3(x8, x2, x4) x6 -> x6 (x4 x2 x8 Nil()) Nil() 4: revApp_l(Nil()) x8 -> x8 5: revApp_l(Cons(x10, x12)) x8 -> revApp() x12 Cons(x10, x8) 6: revApp_1() x3 -> revApp_l(x3) 7: revApp() x6 -> revApp_l(x6) 8: main_2(x8, x2) x4 -> revApp() (x4 x2 x8 Nil()) Nil() 9: dfsAcc_g_t(x4, Leaf(x10)) x8 -> x4 x10 x8 10: dfsAcc_g_t(x4, Node(x10, x12)) x8 -> dfsAcc() x4 x12 (dfsAcc() x4 x10 x8) 11: dfsAcc_g(x2) x3 -> dfsAcc_g_t(x2, x3) 12: dfsAcc_1() x2 -> dfsAcc_g(x2) 13: dfsAcc() x4 -> dfsAcc_g(x4) 14: main_1(x8) x2 -> revApp() (dfsAcc() x2 x8 Nil()) Nil() 15: cons_x(x1) x2 -> Cons(x1, x2) 16: cons() x1 -> cons_x(x1) 17: main(x8) -> revApp() (dfsAcc() cons() x8 Nil()) Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list flatten :: ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main_1 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> 'a48 list revApp_1 :: 'a48 list -> 'a48 list -> 'a48 list main_2 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> 'a48 list main_3 :: 'a48 tree -> ('a48 -> 'a48 list -> 'a48 list) -> (('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list) -> ('a48 list -> 'a48 list -> 'a48 list) -> 'a48 list main_4 :: 'a48 tree -> ('a48 tree -> 'a48 list) -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Nil() | Nil() | Cons(X{*},X{*}) | Nil() | Nil() | Node(X{*},X{*}) | Leaf(X{*}) | Nil() | Nil() | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | Nil() | Nil() | Nil() | Nil() ,V{x1_15} -> V{x1_16} ,V{x1_16} -> V{x10_9} ,V{x2_11} -> V{x4_13} ,V{x2_15} -> V{x8_9} ,V{x3_11} -> V{x12_10} | V{x10_10} | V{x8_17} ,V{x4_9} -> V{x2_11} ,V{x4_10} -> V{x2_11} ,V{x4_13} -> V{x4_10} | cons() ,V{x6_7} -> R{10} | V{x12_5} | R{9} ,V{x8_4} -> Cons(V{x10_5},V{x8_5}) | Nil() ,V{x8_5} -> Cons(V{x10_5},V{x8_5}) | Nil() ,V{x8_9} -> R{10} | R{9} | V{x8_10} | Nil() ,V{x8_10} -> R{10} | R{9} | V{x8_10} | Nil() ,V{x8_17} -> X{*} ,V{x10_5} -> V{x1_15} ,V{x10_9} -> X{*} ,V{x10_10} -> X{*} ,V{x12_5} -> V{x2_15} ,V{x12_10} -> X{*} ,R{0} -> R{17} | main(X{*}) ,R{4} -> V{x8_4} ,R{5} -> R{5} | R{4} | @(R{7},Cons(V{x10_5},V{x8_5})) | @(@(revApp(),V{x12_5}),Cons(V{x10_5},V{x8_5})) ,R{7} -> revApp_l(V{x6_7}) ,R{9} -> R{15} | @(R{16},V{x8_9}) | @(@(V{x4_9},V{x10_9}),V{x8_9}) ,R{10} -> R{10} | R{9} | @(R{11},R{10}) | @(R{11},R{9}) | @(R{11},@(R{11},V{x8_10})) | @(@(R{13},V{x12_10}),R{9}) | @(@(R{13},V{x12_10}),R{10}) | @(@(@(dfsAcc(),V{x4_10}),V{x12_10}),R{10}) | @(@(@(dfsAcc(),V{x4_10}),V{x12_10}),R{9}) | @(@(R{13},V{x12_10}),@(R{11},V{x8_10})) | @(R{11},@(@(R{13},V{x10_10}),V{x8_10})) | @(R{11},@(@(@(dfsAcc(),V{x4_10}),V{x10_10}),V{x8_10})) | @(@(@(dfsAcc(),V{x4_10}),V{x12_10}),@(R{11},V{x8_10})) | @(@(R{13},V{x12_10}),@(@(R{13},V{x10_10}),V{x8_10})) | @(@(@(dfsAcc(),V{x4_10}),V{x12_10}),@(@(R{13},V{x10_10}),V{x8_10})) | @(@(R{13},V{x12_10}),@(@(@(dfsAcc(),V{x4_10}),V{x10_10}),V{x8_10})) | @(@(@(dfsAcc(),V{x4_10}),V{x12_10}),@(@(@(dfsAcc(),V{x4_10}),V{x10_10}),V{x8_10})) ,R{11} -> dfsAcc_g_t(V{x2_11},V{x3_11}) ,R{13} -> dfsAcc_g(V{x4_13}) ,R{15} -> Cons(V{x1_15},V{x2_15}) ,R{16} -> cons_x(V{x1_16}) ,R{17} -> R{4} | R{5} | @(R{7},Nil()) | @(@(revApp(),R{10}),Nil()) | @(@(revApp(),R{9}),Nil()) | @(@(revApp(),@(R{11},Nil())),Nil()) | @(@(revApp(),@(@(R{13},V{x8_17}),Nil())),Nil()) | @(@(revApp(),@(@(@(dfsAcc(),cons()),V{x8_17}),Nil())),Nil())} * Step 11: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 4: revApp_l(Nil()) x8 -> x8 5: revApp_l(Cons(x3, x2)) x1 -> revApp() x2 Cons(x3, x1) 7: revApp() x6 -> revApp_l(x6) 9: dfsAcc_g_t(cons(), Leaf(x2)) x1 -> cons() x2 x1 10: dfsAcc_g_t(cons(), Node(x3, x2)) x1 -> dfsAcc() cons() x2 (dfsAcc() cons() x3 x1) 11: dfsAcc_g(cons()) x1 -> dfsAcc_g_t(cons(), x1) 13: dfsAcc() cons() -> dfsAcc_g(cons()) 15: cons_x(x1) x2 -> Cons(x1, x2) 16: cons() x1 -> cons_x(x1) 17: main(x1) -> revApp() (dfsAcc() cons() x1 Nil()) Nil() where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list dfsAcc :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list revApp :: 'a48 list -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list + Applied Processor: UncurryATRS + Details: none * Step 12: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp_l#1(Nil(), x8) -> x8 2: revApp_l#1(Cons(x3, x2), x1) -> revApp#2(x2, Cons(x3, x1)) 3: revApp#1(x6) -> revApp_l(x6) 4: revApp#2(x6, x7) -> revApp_l#1(x6, x7) 5: dfsAcc_g_t#1(cons(), Leaf(x2), x1) -> cons#2(x2, x1) 6: dfsAcc_g_t#1(cons(), Node(x3, x2), x1) -> dfsAcc#3(cons(), x2, dfsAcc#3(cons(), x3, x1)) 7: dfsAcc_g#1(cons(), x1) -> dfsAcc_g_t(cons(), x1) 8: dfsAcc_g#2(cons(), x1, x2) -> dfsAcc_g_t#1(cons(), x1, x2) 9: dfsAcc#1(cons()) -> dfsAcc_g(cons()) 10: dfsAcc#2(cons(), x0) -> dfsAcc_g#1(cons(), x0) 11: dfsAcc#3(cons(), x0, x1) -> dfsAcc_g#2(cons(), x0, x1) 12: cons_x#1(x1, x2) -> Cons(x1, x2) 13: cons#1(x1) -> cons_x(x1) 14: cons#2(x1, x2) -> cons_x#1(x1, x2) 15: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list cons#1 :: 'a48 -> 'a48 list -> 'a48 list cons#2 :: 'a48 -> 'a48 list -> 'a48 list cons_x :: 'a48 -> 'a48 list -> 'a48 list cons_x#1 :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc#2 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g#1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g#2 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g_t :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g_t#1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#1 :: 'a48 list -> 'a48 list -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list revApp_l :: 'a48 list -> 'a48 list -> 'a48 list revApp_l#1 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 13: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp_l#1(Nil(), x8) -> x8 2: revApp_l#1(Cons(x3, x2), x1) -> revApp#2(x2, Cons(x3, x1)) 4: revApp#2(x6, x7) -> revApp_l#1(x6, x7) 5: dfsAcc_g_t#1(cons(), Leaf(x2), x1) -> cons#2(x2, x1) 6: dfsAcc_g_t#1(cons(), Node(x3, x2), x1) -> dfsAcc#3(cons(), x2, dfsAcc#3(cons(), x3, x1)) 8: dfsAcc_g#2(cons(), x1, x2) -> dfsAcc_g_t#1(cons(), x1, x2) 11: dfsAcc#3(cons(), x0, x1) -> dfsAcc_g#2(cons(), x0, x1) 12: cons_x#1(x1, x2) -> Cons(x1, x2) 14: cons#2(x1, x2) -> cons_x#1(x1, x2) 15: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list cons#2 :: 'a48 -> 'a48 list -> 'a48 list cons_x#1 :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g#2 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g_t#1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list revApp_l#1 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 14: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp_l#1(Nil(), x8) -> x8 2: revApp_l#1(Cons(x3, x2), x1) -> revApp#2(x2, Cons(x3, x1)) 3: revApp#2(Nil(), x16) -> x16 4: revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2)) 5: dfsAcc_g_t#1(cons(), Leaf(x2), x4) -> cons_x#1(x2, x4) 6: dfsAcc_g_t#1(cons(), Node(x3, x2), x1) -> dfsAcc#3(cons(), x2, dfsAcc#3(cons(), x3, x1)) 7: dfsAcc_g#2(cons(), Leaf(x4), x2) -> cons#2(x4, x2) 8: dfsAcc_g#2(cons(), Node(x6, x4), x2) -> dfsAcc#3(cons(), x4, dfsAcc#3(cons(), x6, x2)) 9: dfsAcc#3(cons(), x2, x4) -> dfsAcc_g_t#1(cons(), x2, x4) 10: cons_x#1(x1, x2) -> Cons(x1, x2) 11: cons#2(x2, x4) -> Cons(x2, x4) 12: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list cons#2 :: 'a48 -> 'a48 list -> 'a48 list cons_x#1 :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g#2 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g_t#1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list revApp_l#1 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 15: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 3: revApp#2(Nil(), x16) -> x16 4: revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2)) 5: dfsAcc_g_t#1(cons(), Leaf(x2), x4) -> cons_x#1(x2, x4) 6: dfsAcc_g_t#1(cons(), Node(x3, x2), x1) -> dfsAcc#3(cons(), x2, dfsAcc#3(cons(), x3, x1)) 9: dfsAcc#3(cons(), x2, x4) -> dfsAcc_g_t#1(cons(), x2, x4) 10: cons_x#1(x1, x2) -> Cons(x1, x2) 12: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list cons_x#1 :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g_t#1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp#2(Nil(), x16) -> x16 2: revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2)) 3: dfsAcc_g_t#1(cons(), Leaf(x2), x4) -> Cons(x2, x4) 4: dfsAcc_g_t#1(cons(), Node(x3, x2), x1) -> dfsAcc#3(cons(), x2, dfsAcc#3(cons(), x3, x1)) 5: dfsAcc#3(cons(), Leaf(x4), x8) -> cons_x#1(x4, x8) 6: dfsAcc#3(cons(), Node(x6, x4), x2) -> dfsAcc#3(cons(), x4, dfsAcc#3(cons(), x6, x2)) 7: cons_x#1(x1, x2) -> Cons(x1, x2) 8: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list cons_x#1 :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list dfsAcc_g_t#1 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp#2(Nil(), x16) -> x16 2: revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2)) 5: dfsAcc#3(cons(), Leaf(x4), x8) -> cons_x#1(x4, x8) 6: dfsAcc#3(cons(), Node(x6, x4), x2) -> dfsAcc#3(cons(), x4, dfsAcc#3(cons(), x6, x2)) 7: cons_x#1(x1, x2) -> Cons(x1, x2) 8: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list cons_x#1 :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 18: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp#2(Nil(), x16) -> x16 2: revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2)) 3: dfsAcc#3(cons(), Leaf(x2), x4) -> Cons(x2, x4) 4: dfsAcc#3(cons(), Node(x6, x4), x2) -> dfsAcc#3(cons(), x4, dfsAcc#3(cons(), x6, x2)) 5: cons_x#1(x1, x2) -> Cons(x1, x2) 6: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list cons_x#1 :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 19: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp#2(Nil(), x16) -> x16 2: revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2)) 3: dfsAcc#3(cons(), Leaf(x2), x4) -> Cons(x2, x4) 4: dfsAcc#3(cons(), Node(x6, x4), x2) -> dfsAcc#3(cons(), x4, dfsAcc#3(cons(), x6, x2)) 6: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 20: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp#2(Nil(), x16) -> x16 2: revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2)) 3: dfsAcc#3(cons(), Leaf(x2), x4) -> Cons(x2, x4) 4: dfsAcc#3(cons(), Node(x6, x4), x2) -> dfsAcc#3(cons(), x4, dfsAcc#3(cons(), x6, x2)) 5: main(x1) -> revApp#2(dfsAcc#3(cons(), x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree cons :: 'a48 -> 'a48 list -> 'a48 list dfsAcc#3 :: ('a48 -> 'a48 list -> 'a48 list) -> 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: Compression + Details: none * Step 21: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: revApp#2(Nil(), x16) -> x16 2: revApp#2(Cons(x6, x4), x2) -> revApp#2(x4, Cons(x6, x2)) 3: dfsAcc#3(Leaf(x2), x4) -> Cons(x2, x4) 4: dfsAcc#3(Node(x6, x4), x2) -> dfsAcc#3(x4, dfsAcc#3(x6, x2)) 5: main(x1) -> revApp#2(dfsAcc#3(x1, Nil()), Nil()) where Cons :: 'a -> 'a list -> 'a list Leaf :: 'a -> 'a tree Nil :: 'a list Node :: 'a tree -> 'a tree -> 'a tree dfsAcc#3 :: 'a48 tree -> 'a48 list -> 'a48 list main :: 'a48 tree -> 'a48 list revApp#2 :: 'a48 list -> 'a48 list -> 'a48 list + Applied Processor: ToTctProblem + Details: none * Step 22: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: dfsAcc#3(Leaf(x2),x4) -> Cons(x2,x4) dfsAcc#3(Node(x6,x4),x2) -> dfsAcc#3(x4,dfsAcc#3(x6,x2)) main(x1) -> revApp#2(dfsAcc#3(x1,Nil()),Nil()) revApp#2(Cons(x6,x4),x2) -> revApp#2(x4,Cons(x6,x2)) revApp#2(Nil(),x16) -> x16 - Signature: {dfsAcc#3/2,main/1,revApp#2/2} / {Cons/2,Leaf/1,Nil/0,Node/2} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Leaf,Nil,Node} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(dfsAcc#3) = {2}, uargs(revApp#2) = {1} Following symbols are considered usable: {dfsAcc#3,main,revApp#2} TcT has computed the following interpretation: p(Cons) = 4 + x1 + x2 p(Leaf) = 9 + x1 p(Nil) = 0 p(Node) = 12 + x1 + x2 p(dfsAcc#3) = 2*x1 + x2 p(main) = 9 + 14*x1 p(revApp#2) = 1 + 4*x1 + x2 Following rules are strictly oriented: dfsAcc#3(Leaf(x2),x4) = 18 + 2*x2 + x4 > 4 + x2 + x4 = Cons(x2,x4) dfsAcc#3(Node(x6,x4),x2) = 24 + x2 + 2*x4 + 2*x6 > x2 + 2*x4 + 2*x6 = dfsAcc#3(x4,dfsAcc#3(x6,x2)) main(x1) = 9 + 14*x1 > 1 + 8*x1 = revApp#2(dfsAcc#3(x1,Nil()),Nil()) revApp#2(Cons(x6,x4),x2) = 17 + x2 + 4*x4 + 4*x6 > 5 + x2 + 4*x4 + x6 = revApp#2(x4,Cons(x6,x2)) revApp#2(Nil(),x16) = 1 + x16 > x16 = x16 Following rules are (at-least) weakly oriented: * Step 23: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: dfsAcc#3(Leaf(x2),x4) -> Cons(x2,x4) dfsAcc#3(Node(x6,x4),x2) -> dfsAcc#3(x4,dfsAcc#3(x6,x2)) main(x1) -> revApp#2(dfsAcc#3(x1,Nil()),Nil()) revApp#2(Cons(x6,x4),x2) -> revApp#2(x4,Cons(x6,x2)) revApp#2(Nil(),x16) -> x16 - Signature: {dfsAcc#3/2,main/1,revApp#2/2} / {Cons/2,Leaf/1,Nil/0,Node/2} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Leaf,Nil,Node} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))