WORST_CASE(?,O(n^1))
* Step 1: Desugar WORST_CASE(?,O(n^1))
+ Considered Problem:
type 'a list = Nil | Cons of 'a * 'a list;;
type 'a tree = Leaf of 'a | Node of 'a tree * 'a tree;;
let cons x xs = Cons(x,xs) ;;
let comp f g x = f (g x) ;;
let rec walk t =
match t with
| Leaf(x) -> cons x
| Node(t1,t2) -> comp (walk t1) (walk t2)
;;
let flatten t = walk t Nil
;;
+ Applied Processor:
Desugar {analysedFunction = Nothing}
+ Details:
none
* Step 2: Defunctionalization WORST_CASE(?,O(n^1))
+ Considered Problem:
[1mλt[0m : 'a24 tree.
([1mλcons[0m : 'a24 -> 'a24 list -> 'a24 list.
([1mλcomp[0m : ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list.
([1mλwalk[0m : 'a24 tree -> 'a24 list -> 'a24 list.
([1mλflatten[0m : 'a24 tree -> 'a24 list. [4mflatten[0m [4mt[0m) ([1mλt[0m : 'a24 tree. [4mwalk[0m [4mt[0m Nil))
([1mμwalk[0m : 'a24 tree -> 'a24 list -> 'a24 list.
[1mλt[0m : 'a24 tree.
[1mcase[0m [4mt[0m [1mof[0m
| Leaf -> [1mλx[0m : 'a24.
[4mcons[0m [4mx[0m
| Node -> [1mλt1[0m : 'a24 tree.
[1mλt2[0m : 'a24 tree. [4mcomp[0m ([4mwalk[0m [4mt1[0m) ([4mwalk[0m [4mt2[0m)))
([1mλf[0m : 'a24 list -> 'a24 list. [1mλg[0m : 'a24 list -> 'a24 list. [1mλx[0m : 'a24 list. [4mf[0m ([4mg[0m [4mx[0m)))
([1mλx[0m : 'a24. [1mλxs[0m : 'a24 list. Cons([4mx[0m,[4mxs[0m)) : 'a24 tree -> 'a24 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(x3) x4 -> x3 x4 Nil()
3: main_3(x0) x3 -> main_4(x0) flatten(x3)
4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4
5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5)
6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2)
7: walk(x1, x2) x3 -> walk_1(x1, x2) x3
8: main_2(x0, x1) x2 -> main_3(x0) walk(x1, x2)
9: comp_f_g(x2, x3) x4 -> x2 (x3 x4)
10: comp_f(x2) x3 -> comp_f_g(x2, x3)
11: comp() x2 -> comp_f(x2)
12: main_1(x0) x1 -> main_2(x0, x1) comp()
13: cons_x(x1) x2 -> Cons(x1, x2)
14: cons() x1 -> cons_x(x1)
15: 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
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list
walk_1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main_2 :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list
main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list
cond_walk_t :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
-> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 4: Inline WORST_CASE(?,O(n^1))
+ Considered Problem:
1: main_4(x0) x4 -> x4 x0
2: flatten(x3) x4 -> x3 x4 Nil()
3: main_3(x0) x7 -> flatten(x7) x0
4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4
5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5)
6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2)
7: walk(x2, x4) x6 -> cond_walk_t(x6, x2, x4)
8: main_2(x0, x3) x5 -> main_4(x0) flatten(walk(x3, x5))
9: comp_f_g(x2, x3) x4 -> x2 (x3 x4)
10: comp_f(x2) x3 -> comp_f_g(x2, x3)
11: comp() x2 -> comp_f(x2)
12: main_1(x0) x2 -> main_3(x0) walk(x2, comp())
13: cons_x(x1) x2 -> Cons(x1, x2)
14: cons() x1 -> cons_x(x1)
15: main(x0) -> main_2(x0, cons()) comp()
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list
walk_1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main_2 :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list
main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list
cond_walk_t :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
-> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 5: Inline WORST_CASE(?,O(n^1))
+ Considered Problem:
1: main_4(x0) x4 -> x4 x0
2: flatten(x3) x4 -> x3 x4 Nil()
3: main_3(x8) x6 -> x6 x8 Nil()
4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4
5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5)
6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2)
7: walk(x2, x4) x6 -> cond_walk_t(x6, x2, x4)
8: main_2(x0, x7) x11 -> flatten(walk(x7, x11)) x0
9: comp_f_g(x2, x3) x4 -> x2 (x3 x4)
10: comp_f(x2) x3 -> comp_f_g(x2, x3)
11: comp() x2 -> comp_f(x2)
12: main_1(x0) x5 -> flatten(walk(x5, comp())) x0
13: cons_x(x1) x2 -> Cons(x1, x2)
14: cons() x1 -> cons_x(x1)
15: main(x0) -> main_4(x0) flatten(walk(cons(), comp()))
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list
walk_1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main_2 :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list
main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list
cond_walk_t :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
-> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 6: Inline WORST_CASE(?,O(n^1))
+ Considered Problem:
1: main_4(x0) x4 -> x4 x0
2: flatten(x3) x4 -> x3 x4 Nil()
3: main_3(x8) x6 -> x6 x8 Nil()
4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4
5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5)
6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2)
7: walk(x2, x4) x6 -> cond_walk_t(x6, x2, x4)
8: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil()
9: comp_f_g(x2, x3) x4 -> x2 (x3 x4)
10: comp_f(x2) x3 -> comp_f_g(x2, x3)
11: comp() x2 -> comp_f(x2)
12: main_1(x8) x11 -> walk(x11, comp()) x8 Nil()
13: cons_x(x1) x2 -> Cons(x1, x2)
14: cons() x1 -> cons_x(x1)
15: main(x0) -> flatten(walk(cons(), comp())) x0
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list
walk_1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main_2 :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list
main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list
cond_walk_t :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
-> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 7: Inline WORST_CASE(?,O(n^1))
+ Considered Problem:
1: main_4(x0) x4 -> x4 x0
2: flatten(x3) x4 -> x3 x4 Nil()
3: main_3(x8) x6 -> x6 x8 Nil()
4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4
5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5)
6: walk_1(x1, x2) x3 -> cond_walk_t(x3, x1, x2)
7: walk(x2, x4) x6 -> cond_walk_t(x6, x2, x4)
8: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil()
9: comp_f_g(x2, x3) x4 -> x2 (x3 x4)
10: comp_f(x2) x3 -> comp_f_g(x2, x3)
11: comp() x2 -> comp_f(x2)
12: main_1(x8) x11 -> walk(x11, comp()) x8 Nil()
13: cons_x(x1) x2 -> Cons(x1, x2)
14: cons() x1 -> cons_x(x1)
15: main(x8) -> walk(cons(), comp()) x8 Nil()
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list
walk_1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main_2 :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list
main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list
cond_walk_t :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
-> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
+ Details:
none
* Step 8: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
1: main_4(x0) x4 -> x4 x0
2: flatten(x3) x4 -> x3 x4 Nil()
3: main_3(x8) x6 -> x6 x8 Nil()
4: cond_walk_t(Leaf(x4), x1, x2) -> x1 x4
5: cond_walk_t(Node(x4, x5), x1, x2) -> x2 (walk(x1, x2) x4) (walk(x1, x2) x5)
6: walk_1(x2, x4) Leaf(x8) -> x2 x8
7: walk_1(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10)
8: walk(x2, x4) Leaf(x8) -> x2 x8
9: walk(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10)
10: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil()
11: comp_f_g(x2, x3) x4 -> x2 (x3 x4)
12: comp_f(x2) x3 -> comp_f_g(x2, x3)
13: comp() x2 -> comp_f(x2)
14: main_1(x8) x11 -> walk(x11, comp()) x8 Nil()
15: cons_x(x1) x2 -> Cons(x1, x2)
16: cons() x1 -> cons_x(x1)
17: main(x8) -> walk(cons(), comp()) x8 Nil()
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list
walk_1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main_2 :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list
main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list
cond_walk_t :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
-> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 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(x3) x4 -> x3 x4 Nil()
3: main_3(x8) x6 -> x6 x8 Nil()
6: walk_1(x2, x4) Leaf(x8) -> x2 x8
7: walk_1(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10)
8: walk(x2, x4) Leaf(x8) -> x2 x8
9: walk(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10)
10: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil()
11: comp_f_g(x2, x3) x4 -> x2 (x3 x4)
12: comp_f(x2) x3 -> comp_f_g(x2, x3)
13: comp() x2 -> comp_f(x2)
14: main_1(x8) x11 -> walk(x11, comp()) x8 Nil()
15: cons_x(x1) x2 -> Cons(x1, x2)
16: cons() x1 -> cons_x(x1)
17: main(x8) -> walk(cons(), comp()) x8 Nil()
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list
walk_1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main_2 :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list
main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 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(x3) x4 -> x3 x4 Nil()
3: main_3(x8) x6 -> x6 x8 Nil()
4: walk_1(x2, x4) Leaf(x8) -> x2 x8
5: walk_1(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10)
6: walk(x2, x4) Leaf(x8) -> x2 x8
7: walk(x2, x4) Node(x8, x10) -> x4 (walk(x2, x4) x8) (walk(x2, x4) x10)
8: main_2(x8, x15) x23 -> walk(x15, x23) x8 Nil()
9: comp_f_g(x2, x3) x4 -> x2 (x3 x4)
10: comp_f(x2) x3 -> comp_f_g(x2, x3)
11: comp() x2 -> comp_f(x2)
12: main_1(x8) x11 -> walk(x11, comp()) x8 Nil()
13: cons_x(x1) x2 -> Cons(x1, x2)
14: cons() x1 -> cons_x(x1)
15: main(x8) -> walk(cons(), comp()) x8 Nil()
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
flatten :: ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 tree -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
main_1 :: 'a24 tree -> ('a24 -> 'a24 list -> 'a24 list) -> 'a24 list
walk_1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main_2 :: 'a24 tree
-> ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 list
main_3 :: 'a24 tree -> ('a24 tree -> 'a24 list -> 'a24 list) -> 'a24 list
main_4 :: 'a24 tree -> ('a24 tree -> 'a24 list) -> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 list
+ Applied Processor:
CFA {cfaRefinement = <control flow analysis>}
+ Details:
{X{*} -> Nil()
| Cons(X{*},X{*})
| Nil()
| Nil()
| Node(X{*},X{*})
| Leaf(X{*})
| Node(X{*},X{*})
| Leaf(X{*})
| Nil()
| Nil()
,V{x1_13} -> V{x1_14}
,V{x1_14} -> V{x8_6}
,V{x2_6} -> V{x2_7}
| cons()
,V{x2_7} -> V{x2_7}
| cons()
,V{x2_9} -> V{x2_10}
,V{x2_10} -> V{x2_11}
,V{x2_11} -> R{7}
| R{6}
,V{x2_13} -> R{9}
| R{13}
| V{x4_9}
| Nil()
,V{x3_9} -> V{x3_10}
,V{x3_10} -> R{7}
| R{6}
,V{x4_6} -> V{x4_7}
| comp()
,V{x4_7} -> V{x4_7}
| comp()
,V{x4_9} -> R{9}
| R{13}
| V{x4_9}
| Nil()
,V{x8_6} -> X{*}
,V{x8_7} -> X{*}
,V{x8_15} -> X{*}
,V{x10_7} -> X{*}
,R{0} -> R{15}
| main(X{*})
,R{6} -> R{14}
| @(V{x2_6},V{x8_6})
,R{7} -> R{10}
| @(R{11},R{7})
| @(R{11},R{6})
| @(R{11},@(walk(V{x2_7},V{x4_7}),V{x10_7}))
| @(@(V{x4_7},R{7}),R{6})
| @(@(V{x4_7},R{6}),R{6})
| @(@(V{x4_7},R{7}),R{7})
| @(@(V{x4_7},R{6}),R{7})
| @(@(V{x4_7},@(walk(V{x2_7},V{x4_7}),V{x8_7})),R{7})
| @(@(V{x4_7},@(walk(V{x2_7},V{x4_7}),V{x8_7})),R{6})
| @(@(V{x4_7},R{7}),@(walk(V{x2_7},V{x4_7}),V{x10_7}))
| @(@(V{x4_7},R{6}),@(walk(V{x2_7},V{x4_7}),V{x10_7}))
| @(@(V{x4_7},@(walk(V{x2_7},V{x4_7}),V{x8_7})),@(walk(V{x2_7},V{x4_7}),V{x10_7}))
,R{9} -> R{13}
| R{9}
| @(V{x2_9},R{13})
| @(V{x2_9},R{9})
| @(V{x2_9},@(V{x3_9},V{x4_9}))
,R{10} -> comp_f_g(V{x2_10},V{x3_10})
,R{11} -> comp_f(V{x2_11})
,R{13} -> Cons(V{x1_13},V{x2_13})
,R{14} -> cons_x(V{x1_14})
,R{15} -> R{9}
| R{13}
| @(R{7},Nil())
| @(R{6},Nil())
| @(@(walk(cons(),comp()),V{x8_15}),Nil())}
* Step 11: UncurryATRS WORST_CASE(?,O(n^1))
+ Considered Problem:
6: walk(cons(), comp()) Leaf(x1) -> cons() x1
7: walk(cons(), comp()) Node(x2, x1) -> comp() (walk(cons(), comp()) x2) (walk(cons(), comp()) x1)
9: comp_f_g(comp_f_g(x4, x5), comp_f_g(x2, x3)) x1 -> comp_f_g(x4, x5) (comp_f_g(x2, x3) x1)
10: comp_f_g(comp_f_g(x3, x4), cons_x(x2)) x1 -> comp_f_g(x3, x4) (cons_x(x2) x1)
11: comp_f_g(cons_x(x4), comp_f_g(x2, x3)) x1 -> cons_x(x4) (comp_f_g(x2, x3) x1)
12: comp_f_g(cons_x(x3), cons_x(x2)) x1 -> cons_x(x3) (cons_x(x2) x1)
13: comp_f(x2) x3 -> comp_f_g(x2, x3)
14: comp() x2 -> comp_f(x2)
16: cons_x(x1) x2 -> Cons(x1, x2)
17: cons() x1 -> cons_x(x1)
18: main(x1) -> walk(cons(), comp()) x1 Nil()
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
walk :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
main :: 'a24 tree -> 'a24 list
+ Applied Processor:
UncurryATRS
+ Details:
none
* Step 12: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
1: walk#1(cons(), comp(), Leaf(x1)) -> cons#1(x1)
2: walk#2(cons(), comp(), Leaf(x1), x2) -> cons#2(x1, x2)
3: walk#1(cons(), comp(), Node(x2, x1)) -> comp#2(walk#1(cons(), comp(), x2), walk#1(cons(), comp(), x1))
4: walk#2(cons(), comp(), Node(x2, x1), x3) -> comp#3(walk#1(cons(), comp(), x2), walk#1(cons(), comp(), x1)
, x3)
5: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1))
6: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1))
7: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1))
8: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1))
9: comp_f#1(x2, x3) -> comp_f_g(x2, x3)
10: comp_f#2(x2, x3, x4) -> comp_f_g#1(x2, x3, x4)
11: comp#1(x2) -> comp_f(x2)
12: comp#2(x2, x3) -> comp_f#1(x2, x3)
13: comp#3(x2, x3, x4) -> comp_f#2(x2, x3, x4)
14: cons_x#1(x1, x2) -> Cons(x1, x2)
15: cons#1(x1) -> cons_x(x1)
16: cons#2(x1, x2) -> cons_x#1(x1, x2)
17: main(x1) -> walk#2(cons(), comp(), x1, Nil())
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
cons#1 :: 'a24 -> 'a24 list -> 'a24 list
cons#2 :: 'a24 -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list
main :: 'a24 tree -> 'a24 list
walk#1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
walk#2 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
+ Applied Processor:
UsableRules {urType = DFA}
+ Details:
none
* Step 13: Inline WORST_CASE(?,O(n^1))
+ Considered Problem:
1: walk#1(cons(), comp(), Leaf(x1)) -> cons#1(x1)
2: walk#2(cons(), comp(), Leaf(x1), x2) -> cons#2(x1, x2)
3: walk#1(cons(), comp(), Node(x2, x1)) -> comp#2(walk#1(cons(), comp(), x2), walk#1(cons(), comp(), x1))
4: walk#2(cons(), comp(), Node(x2, x1), x3) -> comp#3(walk#1(cons(), comp(), x2), walk#1(cons(), comp(), x1)
, x3)
5: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1))
6: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1))
7: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1))
8: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1))
9: comp_f#1(x2, x3) -> comp_f_g(x2, x3)
10: comp_f#2(x2, x3, x4) -> comp_f_g#1(x2, x3, x4)
12: comp#2(x2, x3) -> comp_f#1(x2, x3)
13: comp#3(x2, x3, x4) -> comp_f#2(x2, x3, x4)
14: cons_x#1(x1, x2) -> Cons(x1, x2)
15: cons#1(x1) -> cons_x(x1)
16: cons#2(x1, x2) -> cons_x#1(x1, x2)
17: main(x1) -> walk#2(cons(), comp(), x1, Nil())
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
cons#1 :: 'a24 -> 'a24 list -> 'a24 list
cons#2 :: 'a24 -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list
main :: 'a24 tree -> 'a24 list
walk#1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
walk#2 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
+ Details:
none
* Step 14: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
1: walk#1(cons(), comp(), Leaf(x2)) -> cons_x(x2)
2: walk#2(cons(), comp(), Leaf(x2), x4) -> cons_x#1(x2, x4)
3: walk#1(cons(), comp(), Node(x5, x3)) -> comp_f#1(walk#1(cons(), comp(), x5), walk#1(cons(), comp(), x3))
4: walk#2(cons(), comp(), Node(x5, x3), x8) -> comp_f#2(walk#1(cons(), comp(), x5), walk#1(cons(), comp()
, x3)
, x8)
5: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1))
6: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1))
7: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1))
8: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1))
9: comp_f#1(x2, x3) -> comp_f_g(x2, x3)
10: comp_f#2(x2, x3, x4) -> comp_f_g#1(x2, x3, x4)
11: comp#2(x4, x6) -> comp_f_g(x4, x6)
12: comp#3(x4, x6, x8) -> comp_f_g#1(x4, x6, x8)
13: cons_x#1(x1, x2) -> Cons(x1, x2)
14: cons#1(x1) -> cons_x(x1)
15: cons#2(x1, x2) -> cons_x#1(x1, x2)
16: main(Leaf(x2)) -> cons#2(x2, Nil())
17: main(Node(x4, x2)) -> comp#3(walk#1(cons(), comp(), x4), walk#1(cons(), comp(), x2), Nil())
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f#2 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
cons#1 :: 'a24 -> 'a24 list -> 'a24 list
cons#2 :: 'a24 -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list
main :: 'a24 tree -> 'a24 list
walk#1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
walk#2 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 15: Inline WORST_CASE(?,O(n^1))
+ Considered Problem:
1: walk#1(cons(), comp(), Leaf(x2)) -> cons_x(x2)
3: walk#1(cons(), comp(), Node(x5, x3)) -> comp_f#1(walk#1(cons(), comp(), x5), walk#1(cons(), comp(), x3))
5: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1))
6: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1))
7: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1))
8: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1))
9: comp_f#1(x2, x3) -> comp_f_g(x2, x3)
12: comp#3(x4, x6, x8) -> comp_f_g#1(x4, x6, x8)
13: cons_x#1(x1, x2) -> Cons(x1, x2)
15: cons#2(x1, x2) -> cons_x#1(x1, x2)
16: main(Leaf(x2)) -> cons#2(x2, Nil())
17: main(Node(x4, x2)) -> comp#3(walk#1(cons(), comp(), x4), walk#1(cons(), comp(), x2), Nil())
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
cons#2 :: 'a24 -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list
main :: 'a24 tree -> 'a24 list
walk#1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
+ Details:
none
* Step 16: UsableRules WORST_CASE(?,O(n^1))
+ Considered Problem:
1: walk#1(cons(), comp(), Leaf(x2)) -> cons_x(x2)
2: walk#1(cons(), comp(), Node(x11, x7)) -> comp_f_g(walk#1(cons(), comp(), x11), walk#1(cons(), comp()
, x7))
3: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1))
4: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1))
5: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1))
6: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1))
7: comp_f#1(x2, x3) -> comp_f_g(x2, x3)
8: comp#3(x4, x6, x8) -> comp_f_g#1(x4, x6, x8)
9: cons_x#1(x1, x2) -> Cons(x1, x2)
10: cons#2(x1, x2) -> cons_x#1(x1, x2)
11: main(Leaf(x2)) -> cons_x#1(x2, Nil())
12: main(Node(x9, x5)) -> comp_f_g#1(walk#1(cons(), comp(), x9), walk#1(cons(), comp(), x5), Nil())
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp#3 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
cons#2 :: 'a24 -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list
main :: 'a24 tree -> 'a24 list
walk#1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 17: Compression WORST_CASE(?,O(n^1))
+ Considered Problem:
1: walk#1(cons(), comp(), Leaf(x2)) -> cons_x(x2)
2: walk#1(cons(), comp(), Node(x11, x7)) -> comp_f_g(walk#1(cons(), comp(), x11), walk#1(cons(), comp()
, x7))
3: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1))
4: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1))
5: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1))
6: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1))
9: cons_x#1(x1, x2) -> Cons(x1, x2)
11: main(Leaf(x2)) -> cons_x#1(x2, Nil())
12: main(Node(x9, x5)) -> comp_f_g#1(walk#1(cons(), comp(), x9), walk#1(cons(), comp(), x5), Nil())
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons :: 'a24 -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list
main :: 'a24 tree -> 'a24 list
walk#1 :: ('a24 -> 'a24 list -> 'a24 list)
-> (('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list)
-> 'a24 tree
-> 'a24 list
-> 'a24 list
+ Applied Processor:
Compression
+ Details:
none
* Step 18: ToTctProblem WORST_CASE(?,O(n^1))
+ Considered Problem:
1: walk#1(Leaf(x2)) -> cons_x(x2)
2: walk#1(Node(x11, x7)) -> comp_f_g(walk#1(x11), walk#1(x7))
3: comp_f_g#1(comp_f_g(x4, x5), comp_f_g(x2, x3), x1) -> comp_f_g#1(x4, x5, comp_f_g#1(x2, x3, x1))
4: comp_f_g#1(comp_f_g(x3, x4), cons_x(x2), x1) -> comp_f_g#1(x3, x4, cons_x#1(x2, x1))
5: comp_f_g#1(cons_x(x4), comp_f_g(x2, x3), x1) -> cons_x#1(x4, comp_f_g#1(x2, x3, x1))
6: comp_f_g#1(cons_x(x3), cons_x(x2), x1) -> cons_x#1(x3, cons_x#1(x2, x1))
7: cons_x#1(x1, x2) -> Cons(x1, x2)
8: main(Leaf(x2)) -> cons_x#1(x2, Nil())
9: main(Node(x9, x5)) -> comp_f_g#1(walk#1(x9), walk#1(x5), Nil())
where
Cons :: 'a -> 'a list -> 'a list
Leaf :: 'a -> 'a tree
Nil :: 'a list
Node :: 'a tree -> 'a tree -> 'a tree
comp_f_g :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
comp_f_g#1 :: ('a24 list -> 'a24 list) -> ('a24 list -> 'a24 list) -> 'a24 list -> 'a24 list
cons_x :: 'a24 -> 'a24 list -> 'a24 list
cons_x#1 :: 'a24 -> 'a24 list -> 'a24 list
main :: 'a24 tree -> 'a24 list
walk#1 :: 'a24 tree -> 'a24 list -> 'a24 list
+ Applied Processor:
ToTctProblem
+ Details:
none
* Step 19: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) -> comp_f_g#1(x3,x4,cons_x#1(x2,x1))
comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) -> comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1))
comp_f_g#1(cons_x(x3),cons_x(x2),x1) -> cons_x#1(x3,cons_x#1(x2,x1))
comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) -> cons_x#1(x4,comp_f_g#1(x2,x3,x1))
cons_x#1(x1,x2) -> Cons(x1,x2)
main(Leaf(x2)) -> cons_x#1(x2,Nil())
main(Node(x9,x5)) -> comp_f_g#1(walk#1(x9),walk#1(x5),Nil())
walk#1(Leaf(x2)) -> cons_x(x2)
walk#1(Node(x11,x7)) -> comp_f_g(walk#1(x11),walk#1(x7))
- Signature:
{comp_f_g#1/3,cons_x#1/2,main/1,walk#1/1} / {Cons/2,Leaf/1,Nil/0,Node/2,comp_f_g/2,cons_x/1}
- 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(comp_f_g) = {1,2},
uargs(comp_f_g#1) = {1,2,3},
uargs(cons_x#1) = {2}
Following symbols are considered usable:
{comp_f_g#1,cons_x#1,main,walk#1}
TcT has computed the following interpretation:
p(Cons) = 0
p(Leaf) = 2 + x1
p(Nil) = 2
p(Node) = 3 + x1 + x2
p(comp_f_g) = 3 + x1 + x2
p(comp_f_g#1) = 2 + 2*x1 + 2*x2 + x3
p(cons_x) = x1
p(cons_x#1) = x2
p(main) = 2 + 3*x1
p(walk#1) = x1
Following rules are strictly oriented:
comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) = 8 + x1 + 2*x2 + 2*x3 + 2*x4
> 2 + x1 + 2*x3 + 2*x4
= comp_f_g#1(x3,x4,cons_x#1(x2,x1))
comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) = 14 + x1 + 2*x2 + 2*x3 + 2*x4 + 2*x5
> 4 + x1 + 2*x2 + 2*x3 + 2*x4 + 2*x5
= comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1))
comp_f_g#1(cons_x(x3),cons_x(x2),x1) = 2 + x1 + 2*x2 + 2*x3
> x1
= cons_x#1(x3,cons_x#1(x2,x1))
comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) = 8 + x1 + 2*x2 + 2*x3 + 2*x4
> 2 + x1 + 2*x2 + 2*x3
= cons_x#1(x4,comp_f_g#1(x2,x3,x1))
main(Leaf(x2)) = 8 + 3*x2
> 2
= cons_x#1(x2,Nil())
main(Node(x9,x5)) = 11 + 3*x5 + 3*x9
> 4 + 2*x5 + 2*x9
= comp_f_g#1(walk#1(x9),walk#1(x5),Nil())
walk#1(Leaf(x2)) = 2 + x2
> x2
= cons_x(x2)
Following rules are (at-least) weakly oriented:
cons_x#1(x1,x2) = x2
>= 0
= Cons(x1,x2)
walk#1(Node(x11,x7)) = 3 + x11 + x7
>= 3 + x11 + x7
= comp_f_g(walk#1(x11),walk#1(x7))
* Step 20: NaturalPI WORST_CASE(?,O(n^1))
+ Considered Problem:
- Strict TRS:
cons_x#1(x1,x2) -> Cons(x1,x2)
walk#1(Node(x11,x7)) -> comp_f_g(walk#1(x11),walk#1(x7))
- Weak TRS:
comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) -> comp_f_g#1(x3,x4,cons_x#1(x2,x1))
comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) -> comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1))
comp_f_g#1(cons_x(x3),cons_x(x2),x1) -> cons_x#1(x3,cons_x#1(x2,x1))
comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) -> cons_x#1(x4,comp_f_g#1(x2,x3,x1))
main(Leaf(x2)) -> cons_x#1(x2,Nil())
main(Node(x9,x5)) -> comp_f_g#1(walk#1(x9),walk#1(x5),Nil())
walk#1(Leaf(x2)) -> cons_x(x2)
- Signature:
{comp_f_g#1/3,cons_x#1/2,main/1,walk#1/1} / {Cons/2,Leaf/1,Nil/0,Node/2,comp_f_g/2,cons_x/1}
- 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(comp_f_g) = {1,2},
uargs(comp_f_g#1) = {1,2,3},
uargs(cons_x#1) = {2}
Following symbols are considered usable:
{comp_f_g#1,cons_x#1,main,walk#1}
TcT has computed the following interpretation:
p(Cons) = 1
p(Leaf) = 4 + x1
p(Nil) = 6
p(Node) = 7 + x1 + x2
p(comp_f_g) = x1 + x2
p(comp_f_g#1) = 2*x1 + 2*x2 + x3
p(cons_x) = 2
p(cons_x#1) = 3 + x2
p(main) = 1 + 2*x1
p(walk#1) = 1 + x1
Following rules are strictly oriented:
cons_x#1(x1,x2) = 3 + x2
> 1
= Cons(x1,x2)
walk#1(Node(x11,x7)) = 8 + x11 + x7
> 2 + x11 + x7
= comp_f_g(walk#1(x11),walk#1(x7))
Following rules are (at-least) weakly oriented:
comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) = 4 + x1 + 2*x3 + 2*x4
>= 3 + x1 + 2*x3 + 2*x4
= comp_f_g#1(x3,x4,cons_x#1(x2,x1))
comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) = x1 + 2*x2 + 2*x3 + 2*x4 + 2*x5
>= x1 + 2*x2 + 2*x3 + 2*x4 + 2*x5
= comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1))
comp_f_g#1(cons_x(x3),cons_x(x2),x1) = 8 + x1
>= 6 + x1
= cons_x#1(x3,cons_x#1(x2,x1))
comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) = 4 + x1 + 2*x2 + 2*x3
>= 3 + x1 + 2*x2 + 2*x3
= cons_x#1(x4,comp_f_g#1(x2,x3,x1))
main(Leaf(x2)) = 9 + 2*x2
>= 9
= cons_x#1(x2,Nil())
main(Node(x9,x5)) = 15 + 2*x5 + 2*x9
>= 10 + 2*x5 + 2*x9
= comp_f_g#1(walk#1(x9),walk#1(x5),Nil())
walk#1(Leaf(x2)) = 5 + x2
>= 2
= cons_x(x2)
* Step 21: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
comp_f_g#1(comp_f_g(x3,x4),cons_x(x2),x1) -> comp_f_g#1(x3,x4,cons_x#1(x2,x1))
comp_f_g#1(comp_f_g(x4,x5),comp_f_g(x2,x3),x1) -> comp_f_g#1(x4,x5,comp_f_g#1(x2,x3,x1))
comp_f_g#1(cons_x(x3),cons_x(x2),x1) -> cons_x#1(x3,cons_x#1(x2,x1))
comp_f_g#1(cons_x(x4),comp_f_g(x2,x3),x1) -> cons_x#1(x4,comp_f_g#1(x2,x3,x1))
cons_x#1(x1,x2) -> Cons(x1,x2)
main(Leaf(x2)) -> cons_x#1(x2,Nil())
main(Node(x9,x5)) -> comp_f_g#1(walk#1(x9),walk#1(x5),Nil())
walk#1(Leaf(x2)) -> cons_x(x2)
walk#1(Node(x11,x7)) -> comp_f_g(walk#1(x11),walk#1(x7))
- Signature:
{comp_f_g#1/3,cons_x#1/2,main/1,walk#1/1} / {Cons/2,Leaf/1,Nil/0,Node/2,comp_f_g/2,cons_x/1}
- 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))