WORST_CASE(?,O(n^2))
* Step 1: Desugar WORST_CASE(?,O(n^2))
+ Considered Problem:
type nat = 0 | S of nat
;;
type 'a list = Nil | Cons of 'a * 'a list
;;
(*
map f [] = [];
map f (x:xs) = (f x) : (map f xs);
append [] ys = ys;
append (x:xs) ys = x : (append xs ys);
prependAll xs ys = map (append xs) ys;
*)
let rec map f xs =
match xs with
| Nil -> Nil
| Cons(x,xs') -> Cons(f x, map f xs')
;;
let rec append xs ys =
match xs with
| Nil -> ys
| Cons(x,xs') -> Cons(x, append xs' ys)
;;
let prependAll xs ys = map (append xs) ys
;;
+ Applied Processor:
Desugar {analysedFunction = Nothing}
+ Details:
none
* Step 2: Defunctionalization WORST_CASE(?,O(n^2))
+ Considered Problem:
[1mλxs[0m : 'a2 list.
[1mλys[0m : 'a2 list list.
([1mλmap[0m : ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list.
([1mλappend[0m : 'a2 list -> 'a2 list -> 'a2 list.
([1mλprependAll[0m : 'a2 list -> 'a2 list list -> 'a2 list list. [4mprependAll[0m [4mxs[0m [4mys[0m)
([1mλxs[0m : 'a2 list. [1mλys[0m : 'a2 list list. [4mmap[0m ([4mappend[0m [4mxs[0m) [4mys[0m))
([1mμappend[0m : 'a2 list -> 'a2 list -> 'a2 list.
[1mλxs[0m : 'a2 list.
[1mλys[0m : 'a2 list.
[1mcase[0m [4mxs[0m [1mof[0m | Nil -> [4mys[0m | Cons -> [1mλx[0m : 'a2. [1mλxs'[0m : 'a2 list. Cons([4mx[0m,[4mappend[0m [4mxs'[0m [4mys[0m)))
([1mμmap[0m : ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list.
[1mλf[0m : 'a2 list -> 'a2 list.
[1mλxs[0m : 'a2 list list.
[1mcase[0m [4mxs[0m [1mof[0m
| Nil -> Nil
| Cons -> [1mλx[0m : 'a2 list.
[1mλxs'[0m : 'a2 list list. Cons([4mf[0m [4mx[0m,[4mmap[0m [4mf[0m [4mxs'[0m)) : 'a2 list
-> 'a2 list list
-> 'a2 list list
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
S :: nat -> nat
+ Applied Processor:
Defunctionalization
+ Details:
none
* Step 3: Inline WORST_CASE(?,O(n^2))
+ Considered Problem:
1: main_4(x0, x1) x4 -> x4 x0 x1
2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5
3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4)
4: main_3(x0, x1, x2) x3 -> main_4(x0, x1) prependAll(x2, x3)
5: cond_append_xs_ys(Nil(), x4) -> x4
6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4)
7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4)
8: append_1() x3 -> append_xs(x3)
9: append() x0 -> append_1() x0
10: main_2(x0, x1) x2 -> main_3(x0, x1, x2) append()
11: cond_map_f_xs(Nil(), x2) -> Nil()
12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5)
13: map_f(x2) x3 -> cond_map_f_xs(x3, x2)
14: map_1() x2 -> map_f(x2)
15: map() x0 -> map_1() x0
16: main(x0, x1) -> main_2(x0, x1) map()
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_1 :: 'a2 list -> 'a2 list -> 'a2 list
map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main_2 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
main_3 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list list
main_4 :: 'a2 list
-> 'a2 list list
-> ('a2 list -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list
cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 4: Inline WORST_CASE(?,O(n^2))
+ Considered Problem:
1: main_4(x0, x1) x4 -> x4 x0 x1
2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5
3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4)
4: main_3(x0, x2, x5) x7 -> prependAll(x5, x7) x0 x2
5: cond_append_xs_ys(Nil(), x4) -> x4
6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4)
7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4)
8: append_1() x3 -> append_xs(x3)
9: append() x6 -> append_xs(x6)
10: main_2(x0, x2) x4 -> main_4(x0, x2) prependAll(x4, append())
11: cond_map_f_xs(Nil(), x2) -> Nil()
12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5)
13: map_f(x2) x3 -> cond_map_f_xs(x3, x2)
14: map_1() x2 -> map_f(x2)
15: map() x4 -> map_f(x4)
16: main(x0, x2) -> main_3(x0, x2, map()) append()
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_1 :: 'a2 list -> 'a2 list -> 'a2 list
map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main_2 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
main_3 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list list
main_4 :: 'a2 list
-> 'a2 list list
-> ('a2 list -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list
cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 5: Inline WORST_CASE(?,O(n^2))
+ Considered Problem:
1: main_4(x0, x1) x4 -> x4 x0 x1
2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5
3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4)
4: main_3(x8, x5, x4) x6 -> prependAll_xs(x4, x6, x8) x5
5: cond_append_xs_ys(Nil(), x4) -> x4
6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4)
7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4)
8: append_1() x3 -> append_xs(x3)
9: append() x6 -> append_xs(x6)
10: main_2(x0, x2) x9 -> prependAll(x9, append()) x0 x2
11: cond_map_f_xs(Nil(), x2) -> Nil()
12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5)
13: map_f(x2) x3 -> cond_map_f_xs(x3, x2)
14: map_1() x2 -> map_f(x2)
15: map() x4 -> map_f(x4)
16: main(x0, x4) -> prependAll(map(), append()) x0 x4
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_1 :: 'a2 list -> 'a2 list -> 'a2 list
map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main_2 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
main_3 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list list
main_4 :: 'a2 list
-> 'a2 list list
-> ('a2 list -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list
cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 6: Inline WORST_CASE(?,O(n^2))
+ Considered Problem:
1: main_4(x0, x1) x4 -> x4 x0 x1
2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5
3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4)
4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10
5: cond_append_xs_ys(Nil(), x4) -> x4
6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4)
7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4)
8: append_1() x3 -> append_xs(x3)
9: append() x6 -> append_xs(x6)
10: main_2(x8, x5) x4 -> prependAll_xs(x4, append(), x8) x5
11: cond_map_f_xs(Nil(), x2) -> Nil()
12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5)
13: map_f(x2) x3 -> cond_map_f_xs(x3, x2)
14: map_1() x2 -> map_f(x2)
15: map() x4 -> map_f(x4)
16: main(x8, x9) -> prependAll_xs(map(), append(), x8) x9
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_1 :: 'a2 list -> 'a2 list -> 'a2 list
map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main_2 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
main_3 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list list
main_4 :: 'a2 list
-> 'a2 list list
-> ('a2 list -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list
cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 7: Inline WORST_CASE(?,O(n^2))
+ Considered Problem:
1: main_4(x0, x1) x4 -> x4 x0 x1
2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5
3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4)
4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10
5: cond_append_xs_ys(Nil(), x4) -> x4
6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4)
7: append_xs(x3) x4 -> cond_append_xs_ys(x3, x4)
8: append_1() x3 -> append_xs(x3)
9: append() x6 -> append_xs(x6)
10: main_2(x8, x10) x4 -> x4 (append() x8) x10
11: cond_map_f_xs(Nil(), x2) -> Nil()
12: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5)
13: map_f(x2) x3 -> cond_map_f_xs(x3, x2)
14: map_1() x2 -> map_f(x2)
15: map() x4 -> map_f(x4)
16: main(x8, x10) -> map() (append() x8) x10
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_1 :: 'a2 list -> 'a2 list -> 'a2 list
map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main_2 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
main_3 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list list
main_4 :: 'a2 list
-> 'a2 list list
-> ('a2 list -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list
cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
+ Details:
none
* Step 8: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
1: main_4(x0, x1) x4 -> x4 x0 x1
2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5
3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4)
4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10
5: cond_append_xs_ys(Nil(), x4) -> x4
6: cond_append_xs_ys(Cons(x5, x6), x4) -> Cons(x5, append() x6 x4)
7: append_xs(Nil()) x8 -> x8
8: append_xs(Cons(x10, x12)) x8 -> Cons(x10, append() x12 x8)
9: append_1() x3 -> append_xs(x3)
10: append() x6 -> append_xs(x6)
11: main_2(x8, x10) x4 -> x4 (append() x8) x10
12: cond_map_f_xs(Nil(), x2) -> Nil()
13: cond_map_f_xs(Cons(x4, x5), x2) -> Cons(x2 x4, map() x2 x5)
14: map_f(x4) Nil() -> Nil()
15: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10)
16: map_1() x2 -> map_f(x2)
17: map() x4 -> map_f(x4)
18: main(x8, x10) -> map() (append() x8) x10
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_1 :: 'a2 list -> 'a2 list -> 'a2 list
map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main_2 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
main_3 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list list
main_4 :: 'a2 list
-> 'a2 list list
-> ('a2 list -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
cond_map_f_xs :: 'a2 list list -> ('a2 list -> 'a2 list) -> 'a2 list list
cond_append_xs_ys :: 'a2 list -> 'a2 list -> 'a2 list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 9: NeededRules WORST_CASE(?,O(n^2))
+ Considered Problem:
1: main_4(x0, x1) x4 -> x4 x0 x1
2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5
3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4)
4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10
7: append_xs(Nil()) x8 -> x8
8: append_xs(Cons(x10, x12)) x8 -> Cons(x10, append() x12 x8)
9: append_1() x3 -> append_xs(x3)
10: append() x6 -> append_xs(x6)
11: main_2(x8, x10) x4 -> x4 (append() x8) x10
14: map_f(x4) Nil() -> Nil()
15: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10)
16: map_1() x2 -> map_f(x2)
17: map() x4 -> map_f(x4)
18: main(x8, x10) -> map() (append() x8) x10
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_1 :: 'a2 list -> 'a2 list -> 'a2 list
map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main_2 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
main_3 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list list
main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
NeededRules
+ Details:
none
* Step 10: CFA WORST_CASE(?,O(n^2))
+ Considered Problem:
1: main_4(x0, x1) x4 -> x4 x0 x1
2: prependAll_xs(x2, x3, x4) x5 -> x2 (x3 x4) x5
3: prependAll(x2, x3) x4 -> prependAll_xs(x2, x3, x4)
4: main_3(x8, x10, x4) x6 -> x4 (x6 x8) x10
5: append_xs(Nil()) x8 -> x8
6: append_xs(Cons(x10, x12)) x8 -> Cons(x10, append() x12 x8)
7: append_1() x3 -> append_xs(x3)
8: append() x6 -> append_xs(x6)
9: main_2(x8, x10) x4 -> x4 (append() x8) x10
10: map_f(x4) Nil() -> Nil()
11: map_f(x4) Cons(x8, x10) -> Cons(x4 x8, map() x4 x10)
12: map_1() x2 -> map_f(x2)
13: map() x4 -> map_f(x4)
14: main(x8, x10) -> map() (append() x8) x10
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
prependAll :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
prependAll_xs :: (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list
-> 'a2 list list
-> 'a2 list list
append_1 :: 'a2 list -> 'a2 list -> 'a2 list
map_1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main_2 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> 'a2 list list
main_3 :: 'a2 list
-> 'a2 list list
-> (('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list)
-> ('a2 list -> 'a2 list -> 'a2 list)
-> 'a2 list list
main_4 :: 'a2 list -> 'a2 list list -> ('a2 list -> 'a2 list list -> 'a2 list list) -> 'a2 list list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
CFA {cfaRefinement = <control flow analysis>}
+ Details:
{X{*} -> Cons(X{*},X{*})
| Cons(X{*},X{*})
| Nil()
| Nil()
| Cons(X{*},X{*})
| Cons(X{*},X{*})
| Nil()
,V{x4_10} -> V{x4_13}
,V{x4_11} -> V{x4_13}
,V{x4_13} -> V{x4_11}
| R{8}
,V{x6_8} -> V{x12_6}
| V{x8_14}
,V{x8_5} -> V{x8_6}
| V{x8_11}
,V{x8_6} -> V{x8_6}
| V{x8_11}
,V{x8_11} -> X{*}
,V{x8_14} -> X{*}
,V{x10_6} -> X{*}
,V{x10_11} -> X{*}
,V{x10_14} -> X{*}
,V{x12_6} -> X{*}
,R{0} -> R{14}
| main(X{*},X{*})
,R{5} -> V{x8_5}
,R{6} -> Cons(V{x10_6},R{6})
| Cons(V{x10_6},R{5})
| Cons(V{x10_6},@(R{8},V{x8_6}))
| Cons(V{x10_6},@(@(append(),V{x12_6}),V{x8_6}))
,R{8} -> append_xs(V{x6_8})
,R{10} -> Nil()
,R{11} -> Cons(R{6},R{10})
| Cons(R{5},R{10})
| Cons(R{6},R{11})
| Cons(R{5},R{11})
| Cons(@(V{x4_11},V{x8_11}),R{11})
| Cons(@(V{x4_11},V{x8_11}),R{10})
| Cons(R{6},@(R{13},V{x10_11}))
| Cons(R{5},@(R{13},V{x10_11}))
| Cons(@(V{x4_11},V{x8_11}),@(R{13},V{x10_11}))
| Cons(R{6},@(@(map(),V{x4_11}),V{x10_11}))
| Cons(R{5},@(@(map(),V{x4_11}),V{x10_11}))
| Cons(@(V{x4_11},V{x8_11}),@(@(map(),V{x4_11}),V{x10_11}))
,R{13} -> map_f(V{x4_13})
,R{14} -> R{11}
| R{10}
| @(R{13},V{x10_14})
| @(@(map(),R{8}),V{x10_14})
| @(@(map(),@(append(),V{x8_14})),V{x10_14})}
* Step 11: UncurryATRS WORST_CASE(?,O(n^2))
+ Considered Problem:
5: append_xs(Nil()) x8 -> x8
6: append_xs(Cons(x3, x2)) x1 -> Cons(x3, append() x2 x1)
8: append() x6 -> append_xs(x6)
10: map_f(append_xs(x1)) Nil() -> Nil()
11: map_f(append_xs(x3)) Cons(x2, x1) -> Cons(append_xs(x3) x2, map() append_xs(x3) x1)
13: map() append_xs(x1) -> map_f(append_xs(x1))
14: main(x2, x1) -> map() (append() x2) x1
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
append :: 'a2 list -> 'a2 list -> 'a2 list
map :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
+ Applied Processor:
UncurryATRS
+ Details:
none
* Step 12: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
1: append_xs#1(Nil(), x8) -> x8
2: append_xs#1(Cons(x3, x2), x1) -> Cons(x3, append#2(x2, x1))
3: append#1(x6) -> append_xs(x6)
4: append#2(x6, x7) -> append_xs#1(x6, x7)
5: map_f#1(append_xs(x1), Nil()) -> Nil()
6: map_f#1(append_xs(x3), Cons(x2, x1)) -> Cons(append_xs#1(x3, x2), map#2(append_xs(x3), x1))
7: map#1(append_xs(x1)) -> map_f(append_xs(x1))
8: map#2(append_xs(x1), x2) -> map_f#1(append_xs(x1), x2)
9: main(x2, x1) -> map#2(append#1(x2), x1)
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
append#1 :: 'a2 list -> 'a2 list -> 'a2 list
append#2 :: 'a2 list -> 'a2 list -> 'a2 list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
map#1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
map_f :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
map_f#1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
+ Applied Processor:
UsableRules {urType = DFA}
+ Details:
none
* Step 13: Inline WORST_CASE(?,O(n^2))
+ Considered Problem:
1: append_xs#1(Nil(), x8) -> x8
2: append_xs#1(Cons(x3, x2), x1) -> Cons(x3, append#2(x2, x1))
3: append#1(x6) -> append_xs(x6)
4: append#2(x6, x7) -> append_xs#1(x6, x7)
5: map_f#1(append_xs(x1), Nil()) -> Nil()
6: map_f#1(append_xs(x3), Cons(x2, x1)) -> Cons(append_xs#1(x3, x2), map#2(append_xs(x3), x1))
8: map#2(append_xs(x1), x2) -> map_f#1(append_xs(x1), x2)
9: main(x2, x1) -> map#2(append#1(x2), x1)
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
append#1 :: 'a2 list -> 'a2 list -> 'a2 list
append#2 :: 'a2 list -> 'a2 list -> 'a2 list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
map_f#1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
+ Details:
none
* Step 14: UsableRules WORST_CASE(?,O(n^2))
+ Considered Problem:
1: append_xs#1(Nil(), x8) -> x8
2: append_xs#1(Cons(x7, x12), x14) -> Cons(x7, append_xs#1(x12, x14))
3: append#1(x6) -> append_xs(x6)
4: append#2(x6, x7) -> append_xs#1(x6, x7)
5: map_f#1(append_xs(x1), Nil()) -> Nil()
6: map_f#1(append_xs(x3), Cons(x2, x1)) -> Cons(append_xs#1(x3, x2), map#2(append_xs(x3), x1))
7: map#2(append_xs(x2), Nil()) -> Nil()
8: map#2(append_xs(x6), Cons(x4, x2)) -> Cons(append_xs#1(x6, x4), map#2(append_xs(x6), x2))
9: main(x12, x3) -> map#2(append_xs(x12), x3)
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
append#1 :: 'a2 list -> 'a2 list -> 'a2 list
append#2 :: 'a2 list -> 'a2 list -> 'a2 list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
map_f#1 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 15: Compression WORST_CASE(?,O(n^2))
+ Considered Problem:
1: append_xs#1(Nil(), x8) -> x8
2: append_xs#1(Cons(x7, x12), x14) -> Cons(x7, append_xs#1(x12, x14))
7: map#2(append_xs(x2), Nil()) -> Nil()
8: map#2(append_xs(x6), Cons(x4, x2)) -> Cons(append_xs#1(x6, x4), map#2(append_xs(x6), x2))
9: main(x12, x3) -> map#2(append_xs(x12), x3)
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
+ Applied Processor:
Compression
+ Details:
none
* Step 16: ToTctProblem WORST_CASE(?,O(n^2))
+ Considered Problem:
1: append_xs#1(Nil(), x8) -> x8
2: append_xs#1(Cons(x7, x12), x14) -> Cons(x7, append_xs#1(x12, x14))
3: map#2(append_xs(x2), Nil()) -> Nil()
4: map#2(append_xs(x6), Cons(x4, x2)) -> Cons(append_xs#1(x6, x4), map#2(append_xs(x6), x2))
5: main(x12, x3) -> map#2(append_xs(x12), x3)
where
Cons :: 'a -> 'a list -> 'a list
Nil :: 'a list
append_xs :: 'a2 list -> 'a2 list -> 'a2 list
append_xs#1 :: 'a2 list -> 'a2 list -> 'a2 list
main :: 'a2 list -> 'a2 list list -> 'a2 list list
map#2 :: ('a2 list -> 'a2 list) -> 'a2 list list -> 'a2 list list
+ Applied Processor:
ToTctProblem
+ Details:
none
* Step 17: NaturalPI WORST_CASE(?,O(n^2))
+ Considered Problem:
- Strict TRS:
append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14))
append_xs#1(Nil(),x8) -> x8
main(x12,x3) -> map#2(append_xs(x12),x3)
map#2(append_xs(x2),Nil()) -> Nil()
map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2))
- Signature:
{append_xs#1/2,main/2,map#2/2} / {Cons/2,Nil/0,append_xs/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil}
+ Applied Processor:
NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
+ Details:
We apply a polynomial interpretation of kind constructor-based(mixed(2)):
The following argument positions are considered usable:
uargs(Cons) = {1,2}
Following symbols are considered usable:
{append_xs#1,main,map#2}
TcT has computed the following interpretation:
p(Cons) = 2 + x1 + x2
p(Nil) = 1
p(append_xs) = x1
p(append_xs#1) = 1 + 2*x1 + x1*x2 + 5*x2 + x2^2
p(main) = 7 + 4*x1*x2 + 6*x1^2 + 7*x2 + x2^2
p(map#2) = 3 + 4*x1*x2 + 3*x1^2 + 3*x2 + x2^2
Following rules are strictly oriented:
append_xs#1(Cons(x7,x12),x14) = 5 + 2*x12 + x12*x14 + 7*x14 + x14*x7 + x14^2 + 2*x7
> 3 + 2*x12 + x12*x14 + 5*x14 + x14^2 + x7
= Cons(x7,append_xs#1(x12,x14))
append_xs#1(Nil(),x8) = 3 + 6*x8 + x8^2
> x8
= x8
main(x12,x3) = 7 + 4*x12*x3 + 6*x12^2 + 7*x3 + x3^2
> 3 + 4*x12*x3 + 3*x12^2 + 3*x3 + x3^2
= map#2(append_xs(x12),x3)
map#2(append_xs(x2),Nil()) = 7 + 4*x2 + 3*x2^2
> 1
= Nil()
map#2(append_xs(x6),Cons(x4,x2)) = 13 + 7*x2 + 2*x2*x4 + 4*x2*x6 + x2^2 + 7*x4 + 4*x4*x6 + x4^2 + 8*x6 + 3*x6^2
> 6 + 3*x2 + 4*x2*x6 + x2^2 + 5*x4 + x4*x6 + x4^2 + 2*x6 + 3*x6^2
= Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2))
Following rules are (at-least) weakly oriented:
* Step 18: EmptyProcessor WORST_CASE(?,O(1))
+ Considered Problem:
- Weak TRS:
append_xs#1(Cons(x7,x12),x14) -> Cons(x7,append_xs#1(x12,x14))
append_xs#1(Nil(),x8) -> x8
main(x12,x3) -> map#2(append_xs(x12),x3)
map#2(append_xs(x2),Nil()) -> Nil()
map#2(append_xs(x6),Cons(x4,x2)) -> Cons(append_xs#1(x6,x4),map#2(append_xs(x6),x2))
- Signature:
{append_xs#1/2,main/2,map#2/2} / {Cons/2,Nil/0,append_xs/1}
- Obligation:
innermost runtime complexity wrt. defined symbols {main} and constructors {Cons,Nil}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is already closed. The intended complexity is O(1).
WORST_CASE(?,O(n^2))