MAYBE
* Step 1: Desugar MAYBE
+ Considered Problem:
let rec leqNat y x =
match y with
| 0 -> True
| S(y') -> (match x with
| S(x') -> leqNat x' y'
| 0 -> False)
;;
let rec eqNat x y =
match y with
| 0 -> (match x with
| 0 -> True
| S(x') -> False)
| S(y') -> (match x with
| S(x') -> eqNat x' y'
| 0 -> False)
;;
let rec geqNat x y =
match y with
| 0 -> True
| S(y') -> (match x with
| 0 -> False
| S(x') -> geqNat x' y')
;;
let rec ltNat x y =
match y with
| 0 -> False
| S(y') -> (match x with
| 0 -> True
| S(x') -> ltNat x' y')
;;
let rec gtNat x y =
match x with
| 0 -> False
| S(x') -> (match y with
| 0 -> True
| S(y') -> gtNat x' y')
;;
let ifz n th el = match n with
| 0 -> th 0
| S(x) -> el x
;;
let ite cond thenPart elsePart = match cond with
| True -> thenPart
| False -> elsePart
;;
let ite2 cond thenPart elsePart = match cond with
| True -> thenPart
| False -> elsePart
;;
let minus n m =
let rec minus' m n = match m with
| 0 -> 0
| S(x) -> (match n with
| 0 -> m
| S(y) -> minus' x y)
in Pair(minus' n m,m)
;;
let rec plus n m = match m with
| 0 -> n
| S(x) -> S(plus n x)
;;
type ('a,'b,'c) triple = Triple of 'a * 'b * 'c
;;
let rec div_mod n m = match (minus n m) with
| Pair(res,m) -> (match res with
| 0 -> Triple (0,n,m)
| S(x) -> (match (div_mod res m) with
| Triple(a,rest,unusedM) -> Triple(plus S(0) a,rest,m)))
;;
let rec mult n m = match n with
| 0 -> 0
| S(x) -> S(plus (mult x m) m)
;;
type bool = True | False
;;
type 'a option = None | Some of 'a
;;
type 'a list = Nil | Cons of 'a * 'a list
;;
type nat = 0 | S of nat
;;
type Unit = Unit
;;
type ('a,'b) pair = Pair of 'a * 'b
;;
let rec compare_list l1 l2 =
match l1 with
| Nil()-> True
| Cons(x,xs) ->
(match l2 with
| Nil()-> False
| Cons(y,ys) -> ite2 (eqNat x y) (compare_list xs ys) (ltNat x y))
;;
let rec insert le x l =
match l with
| Nil()-> Cons(x,Nil)
| Cons(y,ys) -> ite (le y x) Cons(y,insert le x ys) Cons(x,Cons(y,ys))
;;
let rec isort le l =
match l with
| Nil()-> Nil
| Cons(x,xs) -> insert le x (isort le xs)
;;
let isort_list = isort compare_list
;;
let main xs = isort_list xs
;;
+ Applied Processor:
Desugar {analysedFunction = Nothing}
+ Details:
none
* Step 2: Defunctionalization MAYBE
+ Considered Problem:
[1mλxs[0m : nat list list.
([1mλeqNat[0m : nat -> nat -> bool.
([1mλltNat[0m : nat -> nat -> bool.
([1mλite[0m : bool -> nat list list -> nat list list -> nat list list.
([1mλite2[0m : bool -> bool -> bool -> bool.
([1mλcompare_list[0m : nat list -> nat list -> bool.
([1mλinsert[0m : (nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list.
([1mλisort[0m : (nat list -> nat list -> bool) -> nat list list -> nat list list.
([1mλisort_list[0m : nat list list -> nat list list.
([1mλmain[0m : nat list list -> nat list list. [4mmain[0m [4mxs[0m)
([1mλxs[0m : nat list list. [4misort_list[0m [4mxs[0m))
([4misort[0m [4mcompare_list[0m))
([1mμisort[0m : (nat list -> nat list -> bool) -> nat list list -> nat list list.
[1mλle[0m : nat list -> nat list -> bool.
[1mλl[0m : nat list list.
[1mcase[0m [4ml[0m [1mof[0m
| Nil -> Nil
| Cons -> [1mλx[0m : nat list.
[1mλxs[0m : nat list list. [4minsert[0m [4mle[0m [4mx[0m ([4misort[0m [4mle[0m [4mxs[0m)))
([1mμinsert[0m : (nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list.
[1mλle[0m : nat list -> nat list -> bool.
[1mλx[0m : nat list.
[1mλl[0m : nat list list.
[1mcase[0m [4ml[0m [1mof[0m
| Nil -> Cons([4mx[0m,Nil)
| Cons -> [1mλy[0m : nat list.
[1mλys[0m : nat list list.
[4mite[0m ([4mle[0m [4my[0m [4mx[0m) Cons([4my[0m,[4minsert[0m [4mle[0m [4mx[0m [4mys[0m) Cons([4mx[0m,Cons([4my[0m,[4mys[0m))))
([1mμcompare_list[0m : nat list -> nat list -> bool.
[1mλl1[0m : nat list.
[1mλl2[0m : nat list.
[1mcase[0m [4ml1[0m [1mof[0m
| Nil -> True
| Cons -> [1mλx[0m : nat.
[1mλxs[0m : nat list.
[1mcase[0m [4ml2[0m [1mof[0m
| Nil -> False
| Cons -> [1mλy[0m : nat.
[1mλys[0m : nat list.
[4mite2[0m ([4meqNat[0m [4mx[0m [4my[0m) ([4mcompare_list[0m [4mxs[0m [4mys[0m) ([4mltNat[0m [4mx[0m [4my[0m)))
([1mλcond[0m : bool.
[1mλthenPart[0m : bool. [1mλelsePart[0m : bool. [1mcase[0m [4mcond[0m [1mof[0m | True -> [4mthenPart[0m | False -> [4melsePart[0m))
([1mλcond[0m : bool.
[1mλthenPart[0m : nat list list.
[1mλelsePart[0m : nat list list. [1mcase[0m [4mcond[0m [1mof[0m | True -> [4mthenPart[0m | False -> [4melsePart[0m))
([1mμltNat[0m : nat -> nat -> bool.
[1mλx[0m : nat.
[1mλy[0m : nat.
[1mcase[0m [4my[0m [1mof[0m | 0 -> False | S -> [1mλy'[0m : nat. [1mcase[0m [4mx[0m [1mof[0m | 0 -> True | S -> [1mλx'[0m : nat. [4mltNat[0m [4mx'[0m [4my'[0m))
([1mμeqNat[0m : nat -> nat -> bool.
[1mλx[0m : nat.
[1mλy[0m : nat.
[1mcase[0m [4my[0m [1mof[0m
| 0 -> [1mcase[0m [4mx[0m [1mof[0m
| 0 -> True
| S -> [1mλx'[0m : nat.
False
| S -> [1mλy'[0m : nat.
[1mcase[0m [4mx[0m [1mof[0m | S -> [1mλx'[0m : nat. [4meqNat[0m [4mx'[0m [4my'[0m | 0 -> False) : nat list list -> nat list list
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
None :: 'a option
Pair :: 'a -> 'b -> ('a,'b) pair
S :: nat -> nat
Some :: 'a -> 'a option
Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple
True :: bool
Unit :: Unit
+ Applied Processor:
Defunctionalization
+ Details:
none
* Step 3: Inline MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x0) x8 -> main_9(x0) main_10(x8)
4: main_7(x0, x5) x7 -> main_8(x0) (x7 x5)
5: cond_isort_le_l(Nil(), x6, x7) -> Nil()
6: cond_isort_le_l(Cons(x9, x10), x6, x7) -> x6 x7 x9 (isort(x6) x7 x10)
7: isort_le(x6, x7) x8 -> cond_isort_le_l(x8, x6, x7)
8: isort_1(x6) x7 -> isort_le(x6, x7)
9: isort(x6) x7 -> isort_1(x6) x7
10: main_6(x0, x5) x6 -> main_7(x0, x5) isort(x6)
11: cond_insert_le_x_l(Nil(), x3, x6, x7) -> Cons(x7, Nil())
12: cond_insert_le_x_l(Cons(x9, x10), x3, x6, x7) -> x3 (x6 x9 x7) Cons(x9, insert(x3) x6 x7 x10) Cons(x7
, Cons(x9
, x10))
13: insert_le_x(x3, x6, x7) x8 -> cond_insert_le_x_l(x8, x3, x6, x7)
14: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
15: insert_1(x3) x6 -> insert_le(x3, x6)
16: insert(x3) x4 -> insert_1(x3) x4
17: main_5(x0, x3) x5 -> main_6(x0, x5) insert(x3)
18: cond_compare_list_l1_l2_1(Nil(), x1, x2, x4, x7, x8) -> False()
19: cond_compare_list_l1_l2_1(Cons(x9, x10), x1, x2, x4, x7, x8) -> x4 (x1 x7 x9) (compare_list(x1, x2, x4)
x8 x10) (x2 x7 x9)
20: cond_compare_list_l1_l2(Nil(), x1, x2, x4, x6) -> True()
21: cond_compare_list_l1_l2(Cons(x7, x8), x1, x2, x4, x6) -> cond_compare_list_l1_l2_1(x6, x1
, x2
, x4
, x7
, x8)
22: compare_list_l1(x1, x2, x4, x5) x6 -> cond_compare_list_l1_l2(x5, x1, x2, x4, x6)
23: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
24: compare_list(x1, x2, x4) x5 -> compare_list_1(x1, x2, x4) x5
25: main_4(x0, x1, x2, x3) x4 -> main_5(x0, x3) compare_list(x1, x2, x4)
26: cond_ite2_cond_thenPart_elsePart(True(), x5, x6) -> x5
27: cond_ite2_cond_thenPart_elsePart(False(), x5, x6) -> x6
28: ite2_cond_thenPart(x4, x5) x6 -> cond_ite2_cond_thenPart_elsePart(x4, x5, x6)
29: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
30: ite2() x4 -> ite2_cond(x4)
31: main_3(x0, x1, x2) x3 -> main_4(x0, x1, x2, x3) ite2()
32: cond_ite_cond_thenPart_elsePart(True(), x4, x5) -> x4
33: cond_ite_cond_thenPart_elsePart(False(), x4, x5) -> x5
34: ite_cond_thenPart(x3, x4) x5 -> cond_ite_cond_thenPart_elsePart(x3, x4, x5)
35: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
36: ite() x3 -> ite_cond(x3)
37: main_2(x0, x1) x2 -> main_3(x0, x1, x2) ite()
38: cond_ltNat_x_y_1(0(), x4) -> True()
39: cond_ltNat_x_y_1(S(x5), x4) -> ltNat() x5 x4
40: cond_ltNat_x_y(0(), x2) -> False()
41: cond_ltNat_x_y(S(x4), x2) -> cond_ltNat_x_y_1(x2, x4)
42: ltNat_x(x2) x3 -> cond_ltNat_x_y(x3, x2)
43: ltNat_1() x2 -> ltNat_x(x2)
44: ltNat() x0 -> ltNat_1() x0
45: main_1(x0) x1 -> main_2(x0, x1) ltNat()
46: cond_eqNat_x_y_1(0()) -> True()
47: cond_eqNat_x_y_1(S(x3)) -> False()
48: cond_eqNat_x_y_2(S(x4), x3) -> eqNat() x4 x3
49: cond_eqNat_x_y_2(0(), x3) -> False()
50: cond_eqNat_x_y(0(), x1) -> cond_eqNat_x_y_1(x1)
51: cond_eqNat_x_y(S(x3), x1) -> cond_eqNat_x_y_2(x1, x3)
52: eqNat_x(x1) x2 -> cond_eqNat_x_y(x2, x1)
53: eqNat_1() x1 -> eqNat_x(x1)
54: eqNat() x0 -> eqNat_1() x0
55: main(x0) -> main_1(x0) eqNat()
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
cond_ite_cond_thenPart_elsePart :: bool -> nat list list -> nat list list -> nat list list
cond_ite2_cond_thenPart_elsePart :: bool -> bool -> bool -> bool
cond_isort_le_l :: nat list list
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
cond_insert_le_x_l :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
cond_compare_list_l1_l2 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> bool
cond_eqNat_x_y :: nat -> nat -> bool
cond_ltNat_x_y :: nat -> nat -> bool
cond_compare_list_l1_l2_1 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat
-> nat list
-> bool
cond_eqNat_x_y_1 :: nat -> bool
cond_ltNat_x_y_1 :: nat -> nat -> bool
cond_eqNat_x_y_2 :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 4: Inline MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x0) x17 -> main_10(x17) x0
4: main_7(x0, x11) x15 -> main_9(x0) main_10(x15 x11)
5: cond_isort_le_l(Nil(), x6, x7) -> Nil()
6: cond_isort_le_l(Cons(x9, x10), x6, x7) -> x6 x7 x9 (isort(x6) x7 x10)
7: isort_le(x6, x7) x8 -> cond_isort_le_l(x8, x6, x7)
8: isort_1(x6) x7 -> isort_le(x6, x7)
9: isort(x12) x14 -> isort_le(x12, x14)
10: main_6(x0, x10) x13 -> main_8(x0) (isort(x13) x10)
11: cond_insert_le_x_l(Nil(), x3, x6, x7) -> Cons(x7, Nil())
12: cond_insert_le_x_l(Cons(x9, x10), x3, x6, x7) -> x3 (x6 x9 x7) Cons(x9, insert(x3) x6 x7 x10) Cons(x7
, Cons(x9
, x10))
13: insert_le_x(x3, x6, x7) x8 -> cond_insert_le_x_l(x8, x3, x6, x7)
14: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
15: insert_1(x3) x6 -> insert_le(x3, x6)
16: insert(x6) x12 -> insert_le(x6, x12)
17: main_5(x0, x7) x10 -> main_7(x0, x10) isort(insert(x7))
18: cond_compare_list_l1_l2_1(Nil(), x1, x2, x4, x7, x8) -> False()
19: cond_compare_list_l1_l2_1(Cons(x9, x10), x1, x2, x4, x7, x8) -> x4 (x1 x7 x9) (compare_list(x1, x2, x4)
x8 x10) (x2 x7 x9)
20: cond_compare_list_l1_l2(Nil(), x1, x2, x4, x6) -> True()
21: cond_compare_list_l1_l2(Cons(x7, x8), x1, x2, x4, x6) -> cond_compare_list_l1_l2_1(x6, x1
, x2
, x4
, x7
, x8)
22: compare_list_l1(x1, x2, x4, x5) x6 -> cond_compare_list_l1_l2(x5, x1, x2, x4, x6)
23: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
24: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
25: main_4(x0, x3, x5, x6) x9 -> main_6(x0, compare_list(x3, x5, x9)) insert(x6)
26: cond_ite2_cond_thenPart_elsePart(True(), x5, x6) -> x5
27: cond_ite2_cond_thenPart_elsePart(False(), x5, x6) -> x6
28: ite2_cond_thenPart(x4, x5) x6 -> cond_ite2_cond_thenPart_elsePart(x4, x5, x6)
29: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
30: ite2() x4 -> ite2_cond(x4)
31: main_3(x0, x2, x4) x6 -> main_5(x0, x6) compare_list(x2, x4, ite2())
32: cond_ite_cond_thenPart_elsePart(True(), x4, x5) -> x4
33: cond_ite_cond_thenPart_elsePart(False(), x4, x5) -> x5
34: ite_cond_thenPart(x3, x4) x5 -> cond_ite_cond_thenPart_elsePart(x3, x4, x5)
35: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
36: ite() x3 -> ite_cond(x3)
37: main_2(x0, x2) x4 -> main_4(x0, x2, x4, ite()) ite2()
38: cond_ltNat_x_y_1(0(), x4) -> True()
39: cond_ltNat_x_y_1(S(x5), x4) -> ltNat() x5 x4
40: cond_ltNat_x_y(0(), x2) -> False()
41: cond_ltNat_x_y(S(x4), x2) -> cond_ltNat_x_y_1(x2, x4)
42: ltNat_x(x2) x3 -> cond_ltNat_x_y(x3, x2)
43: ltNat_1() x2 -> ltNat_x(x2)
44: ltNat() x4 -> ltNat_x(x4)
45: main_1(x0) x2 -> main_3(x0, x2, ltNat()) ite()
46: cond_eqNat_x_y_1(0()) -> True()
47: cond_eqNat_x_y_1(S(x3)) -> False()
48: cond_eqNat_x_y_2(S(x4), x3) -> eqNat() x4 x3
49: cond_eqNat_x_y_2(0(), x3) -> False()
50: cond_eqNat_x_y(0(), x1) -> cond_eqNat_x_y_1(x1)
51: cond_eqNat_x_y(S(x3), x1) -> cond_eqNat_x_y_2(x1, x3)
52: eqNat_x(x1) x2 -> cond_eqNat_x_y(x2, x1)
53: eqNat_1() x1 -> eqNat_x(x1)
54: eqNat() x2 -> eqNat_x(x2)
55: main(x0) -> main_2(x0, eqNat()) ltNat()
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
cond_ite_cond_thenPart_elsePart :: bool -> nat list list -> nat list list -> nat list list
cond_ite2_cond_thenPart_elsePart :: bool -> bool -> bool -> bool
cond_isort_le_l :: nat list list
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
cond_insert_le_x_l :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
cond_compare_list_l1_l2 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> bool
cond_eqNat_x_y :: nat -> nat -> bool
cond_ltNat_x_y :: nat -> nat -> bool
cond_compare_list_l1_l2_1 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat
-> nat list
-> bool
cond_eqNat_x_y_1 :: nat -> bool
cond_ltNat_x_y_1 :: nat -> nat -> bool
cond_eqNat_x_y_2 :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 5: Inline MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x18) x16 -> x16 x18
4: main_7(x0, x23) x31 -> main_10(x31 x23) x0
5: cond_isort_le_l(Nil(), x6, x7) -> Nil()
6: cond_isort_le_l(Cons(x9, x10), x6, x7) -> x6 x7 x9 (isort(x6) x7 x10)
7: isort_le(x6, x7) x8 -> cond_isort_le_l(x8, x6, x7)
8: isort_1(x6) x7 -> isort_le(x6, x7)
9: isort(x12) x14 -> isort_le(x12, x14)
10: main_6(x0, x21) x27 -> main_10(isort(x27) x21) x0
11: cond_insert_le_x_l(Nil(), x3, x6, x7) -> Cons(x7, Nil())
12: cond_insert_le_x_l(Cons(x9, x10), x3, x6, x7) -> x3 (x6 x9 x7) Cons(x9, insert(x3) x6 x7 x10) Cons(x7
, Cons(x9
, x10))
13: insert_le_x(x3, x6, x7) x8 -> cond_insert_le_x_l(x8, x3, x6, x7)
14: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
15: insert_1(x3) x6 -> insert_le(x3, x6)
16: insert(x6) x12 -> insert_le(x6, x12)
17: main_5(x0, x15) x22 -> main_9(x0) main_10(isort(insert(x15)) x22)
18: cond_compare_list_l1_l2_1(Nil(), x1, x2, x4, x7, x8) -> False()
19: cond_compare_list_l1_l2_1(Cons(x9, x10), x1, x2, x4, x7, x8) -> x4 (x1 x7 x9) (compare_list(x1, x2, x4)
x8 x10) (x2 x7 x9)
20: cond_compare_list_l1_l2(Nil(), x1, x2, x4, x6) -> True()
21: cond_compare_list_l1_l2(Cons(x7, x8), x1, x2, x4, x6) -> cond_compare_list_l1_l2_1(x6, x1
, x2
, x4
, x7
, x8)
22: compare_list_l1(x1, x2, x4, x5) x6 -> cond_compare_list_l1_l2(x5, x1, x2, x4, x6)
23: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
24: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
25: main_4(x0, x7, x11, x13) x19 -> main_8(x0) (isort(insert(x13)) compare_list(x7, x11, x19))
26: cond_ite2_cond_thenPart_elsePart(True(), x5, x6) -> x5
27: cond_ite2_cond_thenPart_elsePart(False(), x5, x6) -> x6
28: ite2_cond_thenPart(x4, x5) x6 -> cond_ite2_cond_thenPart_elsePart(x4, x5, x6)
29: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
30: ite2() x4 -> ite2_cond(x4)
31: main_3(x0, x5, x9) x14 -> main_7(x0, compare_list(x5, x9, ite2())) isort(insert(x14))
32: cond_ite_cond_thenPart_elsePart(True(), x4, x5) -> x4
33: cond_ite_cond_thenPart_elsePart(False(), x4, x5) -> x5
34: ite_cond_thenPart(x3, x4) x5 -> cond_ite_cond_thenPart_elsePart(x3, x4, x5)
35: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
36: ite() x3 -> ite_cond(x3)
37: main_2(x0, x6) x10 -> main_6(x0, compare_list(x6, x10, ite2())) insert(ite())
38: cond_ltNat_x_y_1(0(), x4) -> True()
39: cond_ltNat_x_y_1(S(x5), x4) -> ltNat() x5 x4
40: cond_ltNat_x_y(0(), x2) -> False()
41: cond_ltNat_x_y(S(x4), x2) -> cond_ltNat_x_y_1(x2, x4)
42: ltNat_x(x2) x3 -> cond_ltNat_x_y(x3, x2)
43: ltNat_1() x2 -> ltNat_x(x2)
44: ltNat() x4 -> ltNat_x(x4)
45: main_1(x0) x4 -> main_5(x0, ite()) compare_list(x4, ltNat(), ite2())
46: cond_eqNat_x_y_1(0()) -> True()
47: cond_eqNat_x_y_1(S(x3)) -> False()
48: cond_eqNat_x_y_2(S(x4), x3) -> eqNat() x4 x3
49: cond_eqNat_x_y_2(0(), x3) -> False()
50: cond_eqNat_x_y(0(), x1) -> cond_eqNat_x_y_1(x1)
51: cond_eqNat_x_y(S(x3), x1) -> cond_eqNat_x_y_2(x1, x3)
52: eqNat_x(x1) x2 -> cond_eqNat_x_y(x2, x1)
53: eqNat_1() x1 -> eqNat_x(x1)
54: eqNat() x2 -> eqNat_x(x2)
55: main(x0) -> main_4(x0, eqNat(), ltNat(), ite()) ite2()
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
cond_ite_cond_thenPart_elsePart :: bool -> nat list list -> nat list list -> nat list list
cond_ite2_cond_thenPart_elsePart :: bool -> bool -> bool -> bool
cond_isort_le_l :: nat list list
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
cond_insert_le_x_l :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
cond_compare_list_l1_l2 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> bool
cond_eqNat_x_y :: nat -> nat -> bool
cond_ltNat_x_y :: nat -> nat -> bool
cond_compare_list_l1_l2_1 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat
-> nat list
-> bool
cond_eqNat_x_y_1 :: nat -> bool
cond_ltNat_x_y_1 :: nat -> nat -> bool
cond_eqNat_x_y_2 :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 6: Inline MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x18) x16 -> x16 x18
4: main_7(x18, x47) x63 -> x63 x47 x18
5: cond_isort_le_l(Nil(), x6, x7) -> Nil()
6: cond_isort_le_l(Cons(x9, x10), x6, x7) -> x6 x7 x9 (isort(x6) x7 x10)
7: isort_le(x6, x7) x8 -> cond_isort_le_l(x8, x6, x7)
8: isort_1(x6) x7 -> isort_le(x6, x7)
9: isort(x12) x14 -> isort_le(x12, x14)
10: main_6(x18, x43) x55 -> isort(x55) x43 x18
11: cond_insert_le_x_l(Nil(), x3, x6, x7) -> Cons(x7, Nil())
12: cond_insert_le_x_l(Cons(x9, x10), x3, x6, x7) -> x3 (x6 x9 x7) Cons(x9, insert(x3) x6 x7 x10) Cons(x7
, Cons(x9
, x10))
13: insert_le_x(x3, x6, x7) x8 -> cond_insert_le_x_l(x8, x3, x6, x7)
14: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
15: insert_1(x3) x6 -> insert_le(x3, x6)
16: insert(x6) x12 -> insert_le(x6, x12)
17: main_5(x0, x31) x45 -> main_10(isort(insert(x31)) x45) x0
18: cond_compare_list_l1_l2_1(Nil(), x1, x2, x4, x7, x8) -> False()
19: cond_compare_list_l1_l2_1(Cons(x9, x10), x1, x2, x4, x7, x8) -> x4 (x1 x7 x9) (compare_list(x1, x2, x4)
x8 x10) (x2 x7 x9)
20: cond_compare_list_l1_l2(Nil(), x1, x2, x4, x6) -> True()
21: cond_compare_list_l1_l2(Cons(x7, x8), x1, x2, x4, x6) -> cond_compare_list_l1_l2_1(x6, x1
, x2
, x4
, x7
, x8)
22: compare_list_l1(x1, x2, x4, x5) x6 -> cond_compare_list_l1_l2(x5, x1, x2, x4, x6)
23: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
24: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
25: main_4(x36, x15, x23, x27) x39 -> isort(insert(x27)) compare_list(x15, x23, x39) x36
26: cond_ite2_cond_thenPart_elsePart(True(), x5, x6) -> x5
27: cond_ite2_cond_thenPart_elsePart(False(), x5, x6) -> x6
28: ite2_cond_thenPart(x4, x5) x6 -> cond_ite2_cond_thenPart_elsePart(x4, x5, x6)
29: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
30: ite2() x4 -> ite2_cond(x4)
31: main_3(x0, x11, x19) x29 -> main_10(isort(insert(x29)) compare_list(x11, x19, ite2())) x0
32: cond_ite_cond_thenPart_elsePart(True(), x4, x5) -> x4
33: cond_ite_cond_thenPart_elsePart(False(), x4, x5) -> x5
34: ite_cond_thenPart(x3, x4) x5 -> cond_ite_cond_thenPart_elsePart(x3, x4, x5)
35: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
36: ite() x3 -> ite_cond(x3)
37: main_2(x0, x13) x21 -> main_10(isort(insert(ite())) compare_list(x13, x21, ite2())) x0
38: cond_ltNat_x_y_1(0(), x4) -> True()
39: cond_ltNat_x_y_1(S(x5), x4) -> ltNat() x5 x4
40: cond_ltNat_x_y(0(), x2) -> False()
41: cond_ltNat_x_y(S(x4), x2) -> cond_ltNat_x_y_1(x2, x4)
42: ltNat_x(x2) x3 -> cond_ltNat_x_y(x3, x2)
43: ltNat_1() x2 -> ltNat_x(x2)
44: ltNat() x4 -> ltNat_x(x4)
45: main_1(x0) x9 -> main_9(x0) main_10(isort(insert(ite())) compare_list(x9, ltNat(), ite2()))
46: cond_eqNat_x_y_1(0()) -> True()
47: cond_eqNat_x_y_1(S(x3)) -> False()
48: cond_eqNat_x_y_2(S(x4), x3) -> eqNat() x4 x3
49: cond_eqNat_x_y_2(0(), x3) -> False()
50: cond_eqNat_x_y(0(), x1) -> cond_eqNat_x_y_1(x1)
51: cond_eqNat_x_y(S(x3), x1) -> cond_eqNat_x_y_2(x1, x3)
52: eqNat_x(x1) x2 -> cond_eqNat_x_y(x2, x1)
53: eqNat_1() x1 -> eqNat_x(x1)
54: eqNat() x2 -> eqNat_x(x2)
55: main(x0) -> main_8(x0) (isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()))
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
cond_ite_cond_thenPart_elsePart :: bool -> nat list list -> nat list list -> nat list list
cond_ite2_cond_thenPart_elsePart :: bool -> bool -> bool -> bool
cond_isort_le_l :: nat list list
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
cond_insert_le_x_l :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
cond_compare_list_l1_l2 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> bool
cond_eqNat_x_y :: nat -> nat -> bool
cond_ltNat_x_y :: nat -> nat -> bool
cond_compare_list_l1_l2_1 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat
-> nat list
-> bool
cond_eqNat_x_y_1 :: nat -> bool
cond_ltNat_x_y_1 :: nat -> nat -> bool
cond_eqNat_x_y_2 :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 7: Inline MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x18) x16 -> x16 x18
4: main_7(x18, x47) x63 -> x63 x47 x18
5: cond_isort_le_l(Nil(), x6, x7) -> Nil()
6: cond_isort_le_l(Cons(x9, x10), x6, x7) -> x6 x7 x9 (isort(x6) x7 x10)
7: isort_le(x6, x7) x8 -> cond_isort_le_l(x8, x6, x7)
8: isort_1(x6) x7 -> isort_le(x6, x7)
9: isort(x12) x14 -> isort_le(x12, x14)
10: main_6(x18, x43) x55 -> isort(x55) x43 x18
11: cond_insert_le_x_l(Nil(), x3, x6, x7) -> Cons(x7, Nil())
12: cond_insert_le_x_l(Cons(x9, x10), x3, x6, x7) -> x3 (x6 x9 x7) Cons(x9, insert(x3) x6 x7 x10) Cons(x7
, Cons(x9
, x10))
13: insert_le_x(x3, x6, x7) x8 -> cond_insert_le_x_l(x8, x3, x6, x7)
14: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
15: insert_1(x3) x6 -> insert_le(x3, x6)
16: insert(x6) x12 -> insert_le(x6, x12)
17: main_5(x18, x63) x91 -> isort(insert(x63)) x91 x18
18: cond_compare_list_l1_l2_1(Nil(), x1, x2, x4, x7, x8) -> False()
19: cond_compare_list_l1_l2_1(Cons(x9, x10), x1, x2, x4, x7, x8) -> x4 (x1 x7 x9) (compare_list(x1, x2, x4)
x8 x10) (x2 x7 x9)
20: cond_compare_list_l1_l2(Nil(), x1, x2, x4, x6) -> True()
21: cond_compare_list_l1_l2(Cons(x7, x8), x1, x2, x4, x6) -> cond_compare_list_l1_l2_1(x6, x1
, x2
, x4
, x7
, x8)
22: compare_list_l1(x1, x2, x4, x5) x6 -> cond_compare_list_l1_l2(x5, x1, x2, x4, x6)
23: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
24: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
25: main_4(x36, x15, x23, x27) x39 -> isort(insert(x27)) compare_list(x15, x23, x39) x36
26: cond_ite2_cond_thenPart_elsePart(True(), x5, x6) -> x5
27: cond_ite2_cond_thenPart_elsePart(False(), x5, x6) -> x6
28: ite2_cond_thenPart(x4, x5) x6 -> cond_ite2_cond_thenPart_elsePart(x4, x5, x6)
29: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
30: ite2() x4 -> ite2_cond(x4)
31: main_3(x18, x23, x39) x59 -> isort(insert(x59)) compare_list(x23, x39, ite2()) x18
32: cond_ite_cond_thenPart_elsePart(True(), x4, x5) -> x4
33: cond_ite_cond_thenPart_elsePart(False(), x4, x5) -> x5
34: ite_cond_thenPart(x3, x4) x5 -> cond_ite_cond_thenPart_elsePart(x3, x4, x5)
35: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
36: ite() x3 -> ite_cond(x3)
37: main_2(x18, x27) x43 -> isort(insert(ite())) compare_list(x27, x43, ite2()) x18
38: cond_ltNat_x_y_1(0(), x4) -> True()
39: cond_ltNat_x_y_1(S(x5), x4) -> ltNat() x5 x4
40: cond_ltNat_x_y(0(), x2) -> False()
41: cond_ltNat_x_y(S(x4), x2) -> cond_ltNat_x_y_1(x2, x4)
42: ltNat_x(x2) x3 -> cond_ltNat_x_y(x3, x2)
43: ltNat_1() x2 -> ltNat_x(x2)
44: ltNat() x4 -> ltNat_x(x4)
45: main_1(x0) x19 -> main_10(isort(insert(ite())) compare_list(x19, ltNat(), ite2())) x0
46: cond_eqNat_x_y_1(0()) -> True()
47: cond_eqNat_x_y_1(S(x3)) -> False()
48: cond_eqNat_x_y_2(S(x4), x3) -> eqNat() x4 x3
49: cond_eqNat_x_y_2(0(), x3) -> False()
50: cond_eqNat_x_y(0(), x1) -> cond_eqNat_x_y_1(x1)
51: cond_eqNat_x_y(S(x3), x1) -> cond_eqNat_x_y_2(x1, x3)
52: eqNat_x(x1) x2 -> cond_eqNat_x_y(x2, x1)
53: eqNat_1() x1 -> eqNat_x(x1)
54: eqNat() x2 -> eqNat_x(x2)
55: main(x36) -> isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) x36
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
cond_ite_cond_thenPart_elsePart :: bool -> nat list list -> nat list list -> nat list list
cond_ite2_cond_thenPart_elsePart :: bool -> bool -> bool -> bool
cond_isort_le_l :: nat list list
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
cond_insert_le_x_l :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
cond_compare_list_l1_l2 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> bool
cond_eqNat_x_y :: nat -> nat -> bool
cond_ltNat_x_y :: nat -> nat -> bool
cond_compare_list_l1_l2_1 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat
-> nat list
-> bool
cond_eqNat_x_y_1 :: nat -> bool
cond_ltNat_x_y_1 :: nat -> nat -> bool
cond_eqNat_x_y_2 :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
+ Details:
none
* Step 8: Inline MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x18) x16 -> x16 x18
4: main_7(x18, x47) x63 -> x63 x47 x18
5: cond_isort_le_l(Nil(), x6, x7) -> Nil()
6: cond_isort_le_l(Cons(x9, x10), x6, x7) -> x6 x7 x9 (isort(x6) x7 x10)
7: isort_le(x6, x7) x8 -> cond_isort_le_l(x8, x6, x7)
8: isort_1(x6) x7 -> isort_le(x6, x7)
9: isort(x12) x14 -> isort_le(x12, x14)
10: main_6(x18, x43) x55 -> isort(x55) x43 x18
11: cond_insert_le_x_l(Nil(), x3, x6, x7) -> Cons(x7, Nil())
12: cond_insert_le_x_l(Cons(x9, x10), x3, x6, x7) -> x3 (x6 x9 x7) Cons(x9, insert(x3) x6 x7 x10) Cons(x7
, Cons(x9
, x10))
13: insert_le_x(x3, x6, x7) x8 -> cond_insert_le_x_l(x8, x3, x6, x7)
14: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
15: insert_1(x3) x6 -> insert_le(x3, x6)
16: insert(x6) x12 -> insert_le(x6, x12)
17: main_5(x18, x63) x91 -> isort(insert(x63)) x91 x18
18: cond_compare_list_l1_l2_1(Nil(), x1, x2, x4, x7, x8) -> False()
19: cond_compare_list_l1_l2_1(Cons(x9, x10), x1, x2, x4, x7, x8) -> x4 (x1 x7 x9) (compare_list(x1, x2, x4)
x8 x10) (x2 x7 x9)
20: cond_compare_list_l1_l2(Nil(), x1, x2, x4, x6) -> True()
21: cond_compare_list_l1_l2(Cons(x7, x8), x1, x2, x4, x6) -> cond_compare_list_l1_l2_1(x6, x1
, x2
, x4
, x7
, x8)
22: compare_list_l1(x1, x2, x4, x5) x6 -> cond_compare_list_l1_l2(x5, x1, x2, x4, x6)
23: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
24: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
25: main_4(x36, x15, x23, x27) x39 -> isort(insert(x27)) compare_list(x15, x23, x39) x36
26: cond_ite2_cond_thenPart_elsePart(True(), x5, x6) -> x5
27: cond_ite2_cond_thenPart_elsePart(False(), x5, x6) -> x6
28: ite2_cond_thenPart(x4, x5) x6 -> cond_ite2_cond_thenPart_elsePart(x4, x5, x6)
29: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
30: ite2() x4 -> ite2_cond(x4)
31: main_3(x18, x23, x39) x59 -> isort(insert(x59)) compare_list(x23, x39, ite2()) x18
32: cond_ite_cond_thenPart_elsePart(True(), x4, x5) -> x4
33: cond_ite_cond_thenPart_elsePart(False(), x4, x5) -> x5
34: ite_cond_thenPart(x3, x4) x5 -> cond_ite_cond_thenPart_elsePart(x3, x4, x5)
35: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
36: ite() x3 -> ite_cond(x3)
37: main_2(x18, x27) x43 -> isort(insert(ite())) compare_list(x27, x43, ite2()) x18
38: cond_ltNat_x_y_1(0(), x4) -> True()
39: cond_ltNat_x_y_1(S(x5), x4) -> ltNat() x5 x4
40: cond_ltNat_x_y(0(), x2) -> False()
41: cond_ltNat_x_y(S(x4), x2) -> cond_ltNat_x_y_1(x2, x4)
42: ltNat_x(x2) x3 -> cond_ltNat_x_y(x3, x2)
43: ltNat_1() x2 -> ltNat_x(x2)
44: ltNat() x4 -> ltNat_x(x4)
45: main_1(x18) x39 -> isort(insert(ite())) compare_list(x39, ltNat(), ite2()) x18
46: cond_eqNat_x_y_1(0()) -> True()
47: cond_eqNat_x_y_1(S(x3)) -> False()
48: cond_eqNat_x_y_2(S(x4), x3) -> eqNat() x4 x3
49: cond_eqNat_x_y_2(0(), x3) -> False()
50: cond_eqNat_x_y(0(), x1) -> cond_eqNat_x_y_1(x1)
51: cond_eqNat_x_y(S(x3), x1) -> cond_eqNat_x_y_2(x1, x3)
52: eqNat_x(x1) x2 -> cond_eqNat_x_y(x2, x1)
53: eqNat_1() x1 -> eqNat_x(x1)
54: eqNat() x2 -> eqNat_x(x2)
55: main(x36) -> isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) x36
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
cond_ite_cond_thenPart_elsePart :: bool -> nat list list -> nat list list -> nat list list
cond_ite2_cond_thenPart_elsePart :: bool -> bool -> bool -> bool
cond_isort_le_l :: nat list list
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
cond_insert_le_x_l :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
cond_compare_list_l1_l2 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> bool
cond_eqNat_x_y :: nat -> nat -> bool
cond_ltNat_x_y :: nat -> nat -> bool
cond_compare_list_l1_l2_1 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat
-> nat list
-> bool
cond_eqNat_x_y_1 :: nat -> bool
cond_ltNat_x_y_1 :: nat -> nat -> bool
cond_eqNat_x_y_2 :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
+ Details:
none
* Step 9: Inline MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x18) x16 -> x16 x18
4: main_7(x18, x47) x63 -> x63 x47 x18
5: cond_isort_le_l(Nil(), x6, x7) -> Nil()
6: cond_isort_le_l(Cons(x9, x10), x6, x7) -> x6 x7 x9 (isort(x6) x7 x10)
7: isort_le(x12, x14) Nil() -> Nil()
8: isort_le(x12, x14) Cons(x18, x20) -> x12 x14 x18 (isort(x12) x14 x20)
9: isort_1(x6) x7 -> isort_le(x6, x7)
10: isort(x12) x14 -> isort_le(x12, x14)
11: main_6(x18, x43) x55 -> isort(x55) x43 x18
12: cond_insert_le_x_l(Nil(), x3, x6, x7) -> Cons(x7, Nil())
13: cond_insert_le_x_l(Cons(x9, x10), x3, x6, x7) -> x3 (x6 x9 x7) Cons(x9, insert(x3) x6 x7 x10) Cons(x7
, Cons(x9
, x10))
14: insert_le_x(x6, x12, x14) Nil() -> Cons(x14, Nil())
15: insert_le_x(x6, x12, x14) Cons(x18, x20) -> x6 (x12 x18 x14) Cons(x18, insert(x6) x12 x14 x20) Cons(x14
, Cons(x18
, x20))
16: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
17: insert_1(x3) x6 -> insert_le(x3, x6)
18: insert(x6) x12 -> insert_le(x6, x12)
19: main_5(x18, x63) x91 -> isort(insert(x63)) x91 x18
20: cond_compare_list_l1_l2_1(Nil(), x1, x2, x4, x7, x8) -> False()
21: cond_compare_list_l1_l2_1(Cons(x9, x10), x1, x2, x4, x7, x8) -> x4 (x1 x7 x9) (compare_list(x1, x2, x4)
x8 x10) (x2 x7 x9)
22: cond_compare_list_l1_l2(Nil(), x1, x2, x4, x6) -> True()
23: cond_compare_list_l1_l2(Cons(x14, x16), x2, x4, x8, Nil()) -> False()
24: cond_compare_list_l1_l2(Cons(x14, x16), x2, x4, x8, Cons(x18, x20)) -> x8 (x2 x14 x18) (compare_list(x2
, x4
, x8)
x16 x20) (x4 x14 x18)
25: compare_list_l1(x2, x4, x8, Nil()) x12 -> True()
26: compare_list_l1(x2, x4, x8, Cons(x14, x16)) x12 -> cond_compare_list_l1_l2_1(x12, x2, x4, x8, x14, x16)
27: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
28: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
29: main_4(x36, x15, x23, x27) x39 -> isort(insert(x27)) compare_list(x15, x23, x39) x36
30: cond_ite2_cond_thenPart_elsePart(True(), x5, x6) -> x5
31: cond_ite2_cond_thenPart_elsePart(False(), x5, x6) -> x6
32: ite2_cond_thenPart(True(), x10) x12 -> x10
33: ite2_cond_thenPart(False(), x10) x12 -> x12
34: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
35: ite2() x4 -> ite2_cond(x4)
36: main_3(x18, x23, x39) x59 -> isort(insert(x59)) compare_list(x23, x39, ite2()) x18
37: cond_ite_cond_thenPart_elsePart(True(), x4, x5) -> x4
38: cond_ite_cond_thenPart_elsePart(False(), x4, x5) -> x5
39: ite_cond_thenPart(True(), x8) x10 -> x8
40: ite_cond_thenPart(False(), x8) x10 -> x10
41: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
42: ite() x3 -> ite_cond(x3)
43: main_2(x18, x27) x43 -> isort(insert(ite())) compare_list(x27, x43, ite2()) x18
44: cond_ltNat_x_y_1(0(), x4) -> True()
45: cond_ltNat_x_y_1(S(x5), x4) -> ltNat() x5 x4
46: cond_ltNat_x_y(0(), x2) -> False()
47: cond_ltNat_x_y(S(x8), 0()) -> True()
48: cond_ltNat_x_y(S(x8), S(x10)) -> ltNat() x10 x8
49: ltNat_x(x4) 0() -> False()
50: ltNat_x(x4) S(x8) -> cond_ltNat_x_y_1(x4, x8)
51: ltNat_1() x2 -> ltNat_x(x2)
52: ltNat() x4 -> ltNat_x(x4)
53: main_1(x18) x39 -> isort(insert(ite())) compare_list(x39, ltNat(), ite2()) x18
54: cond_eqNat_x_y_1(0()) -> True()
55: cond_eqNat_x_y_1(S(x3)) -> False()
56: cond_eqNat_x_y_2(S(x4), x3) -> eqNat() x4 x3
57: cond_eqNat_x_y_2(0(), x3) -> False()
58: cond_eqNat_x_y(0(), 0()) -> True()
59: cond_eqNat_x_y(0(), S(x6)) -> False()
60: cond_eqNat_x_y(S(x6), S(x8)) -> eqNat() x8 x6
61: cond_eqNat_x_y(S(x6), 0()) -> False()
62: eqNat_x(x2) 0() -> cond_eqNat_x_y_1(x2)
63: eqNat_x(x2) S(x6) -> cond_eqNat_x_y_2(x2, x6)
64: eqNat_1() x1 -> eqNat_x(x1)
65: eqNat() x2 -> eqNat_x(x2)
66: main(x36) -> isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) x36
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
cond_ite_cond_thenPart_elsePart :: bool -> nat list list -> nat list list -> nat list list
cond_ite2_cond_thenPart_elsePart :: bool -> bool -> bool -> bool
cond_isort_le_l :: nat list list
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
cond_insert_le_x_l :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
cond_compare_list_l1_l2 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> bool
cond_eqNat_x_y :: nat -> nat -> bool
cond_ltNat_x_y :: nat -> nat -> bool
cond_compare_list_l1_l2_1 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat
-> nat list
-> bool
cond_eqNat_x_y_1 :: nat -> bool
cond_ltNat_x_y_1 :: nat -> nat -> bool
cond_eqNat_x_y_2 :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
+ Details:
none
* Step 10: UsableRules MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x18) x16 -> x16 x18
4: main_7(x18, x47) x63 -> x63 x47 x18
5: cond_isort_le_l(Nil(), x6, x7) -> Nil()
6: cond_isort_le_l(Cons(x9, x10), x6, x7) -> x6 x7 x9 (isort(x6) x7 x10)
7: isort_le(x12, x14) Nil() -> Nil()
8: isort_le(x12, x14) Cons(x18, x20) -> x12 x14 x18 (isort(x12) x14 x20)
9: isort_1(x6) x7 -> isort_le(x6, x7)
10: isort(x12) x14 -> isort_le(x12, x14)
11: main_6(x18, x43) x55 -> isort(x55) x43 x18
12: cond_insert_le_x_l(Nil(), x3, x6, x7) -> Cons(x7, Nil())
13: cond_insert_le_x_l(Cons(x9, x10), x3, x6, x7) -> x3 (x6 x9 x7) Cons(x9, insert(x3) x6 x7 x10) Cons(x7
, Cons(x9
, x10))
14: insert_le_x(x6, x12, x14) Nil() -> Cons(x14, Nil())
15: insert_le_x(x6, x12, x14) Cons(x18, x20) -> x6 (x12 x18 x14) Cons(x18, insert(x6) x12 x14 x20) Cons(x14
, Cons(x18
, x20))
16: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
17: insert_1(x3) x6 -> insert_le(x3, x6)
18: insert(x6) x12 -> insert_le(x6, x12)
19: main_5(x18, x63) x91 -> isort(insert(x63)) x91 x18
20: cond_compare_list_l1_l2_1(Nil(), x1, x2, x4, x7, x8) -> False()
21: cond_compare_list_l1_l2_1(Cons(x9, x10), x1, x2, x4, x7, x8) -> x4 (x1 x7 x9) (compare_list(x1, x2, x4)
x8 x10) (x2 x7 x9)
22: cond_compare_list_l1_l2(Nil(), x1, x2, x4, x6) -> True()
23: cond_compare_list_l1_l2(Cons(x14, x16), x2, x4, x8, Nil()) -> False()
24: cond_compare_list_l1_l2(Cons(x14, x16), x2, x4, x8, Cons(x18, x20)) -> x8 (x2 x14 x18) (compare_list(x2
, x4
, x8)
x16 x20) (x4 x14 x18)
25: compare_list_l1(x2, x4, x8, Nil()) x12 -> True()
26: compare_list_l1(x2, x4, x8, Cons(x14, x16)) Nil() -> False()
27: compare_list_l1(x2, x4, x8, Cons(x14, x16)) Cons(x18, x20) -> x8 (x2 x14 x18) (compare_list(x2, x4, x8)
x16 x20) (x4 x14 x18)
28: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
29: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
30: main_4(x36, x15, x23, x27) x39 -> isort(insert(x27)) compare_list(x15, x23, x39) x36
31: cond_ite2_cond_thenPart_elsePart(True(), x5, x6) -> x5
32: cond_ite2_cond_thenPart_elsePart(False(), x5, x6) -> x6
33: ite2_cond_thenPart(True(), x10) x12 -> x10
34: ite2_cond_thenPart(False(), x10) x12 -> x12
35: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
36: ite2() x4 -> ite2_cond(x4)
37: main_3(x18, x23, x39) x59 -> isort(insert(x59)) compare_list(x23, x39, ite2()) x18
38: cond_ite_cond_thenPart_elsePart(True(), x4, x5) -> x4
39: cond_ite_cond_thenPart_elsePart(False(), x4, x5) -> x5
40: ite_cond_thenPart(True(), x8) x10 -> x8
41: ite_cond_thenPart(False(), x8) x10 -> x10
42: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
43: ite() x3 -> ite_cond(x3)
44: main_2(x18, x27) x43 -> isort(insert(ite())) compare_list(x27, x43, ite2()) x18
45: cond_ltNat_x_y_1(0(), x4) -> True()
46: cond_ltNat_x_y_1(S(x5), x4) -> ltNat() x5 x4
47: cond_ltNat_x_y(0(), x2) -> False()
48: cond_ltNat_x_y(S(x8), 0()) -> True()
49: cond_ltNat_x_y(S(x8), S(x10)) -> ltNat() x10 x8
50: ltNat_x(x4) 0() -> False()
51: ltNat_x(0()) S(x8) -> True()
52: ltNat_x(S(x10)) S(x8) -> ltNat() x10 x8
53: ltNat_1() x2 -> ltNat_x(x2)
54: ltNat() x4 -> ltNat_x(x4)
55: main_1(x18) x39 -> isort(insert(ite())) compare_list(x39, ltNat(), ite2()) x18
56: cond_eqNat_x_y_1(0()) -> True()
57: cond_eqNat_x_y_1(S(x3)) -> False()
58: cond_eqNat_x_y_2(S(x4), x3) -> eqNat() x4 x3
59: cond_eqNat_x_y_2(0(), x3) -> False()
60: cond_eqNat_x_y(0(), 0()) -> True()
61: cond_eqNat_x_y(0(), S(x6)) -> False()
62: cond_eqNat_x_y(S(x6), S(x8)) -> eqNat() x8 x6
63: cond_eqNat_x_y(S(x6), 0()) -> False()
64: eqNat_x(0()) 0() -> True()
65: eqNat_x(S(x6)) 0() -> False()
66: eqNat_x(S(x8)) S(x6) -> eqNat() x8 x6
67: eqNat_x(0()) S(x6) -> False()
68: eqNat_1() x1 -> eqNat_x(x1)
69: eqNat() x2 -> eqNat_x(x2)
70: main(x36) -> isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) x36
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
cond_ite_cond_thenPart_elsePart :: bool -> nat list list -> nat list list -> nat list list
cond_ite2_cond_thenPart_elsePart :: bool -> bool -> bool -> bool
cond_isort_le_l :: nat list list
-> ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
cond_insert_le_x_l :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
cond_compare_list_l1_l2 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> bool
cond_eqNat_x_y :: nat -> nat -> bool
cond_ltNat_x_y :: nat -> nat -> bool
cond_compare_list_l1_l2_1 :: nat list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat
-> nat list
-> bool
cond_eqNat_x_y_1 :: nat -> bool
cond_ltNat_x_y_1 :: nat -> nat -> bool
cond_eqNat_x_y_2 :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 11: NeededRules MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x18) x16 -> x16 x18
4: main_7(x18, x47) x63 -> x63 x47 x18
7: isort_le(x12, x14) Nil() -> Nil()
8: isort_le(x12, x14) Cons(x18, x20) -> x12 x14 x18 (isort(x12) x14 x20)
9: isort_1(x6) x7 -> isort_le(x6, x7)
10: isort(x12) x14 -> isort_le(x12, x14)
11: main_6(x18, x43) x55 -> isort(x55) x43 x18
14: insert_le_x(x6, x12, x14) Nil() -> Cons(x14, Nil())
15: insert_le_x(x6, x12, x14) Cons(x18, x20) -> x6 (x12 x18 x14) Cons(x18, insert(x6) x12 x14 x20) Cons(x14
, Cons(x18
, x20))
16: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
17: insert_1(x3) x6 -> insert_le(x3, x6)
18: insert(x6) x12 -> insert_le(x6, x12)
19: main_5(x18, x63) x91 -> isort(insert(x63)) x91 x18
25: compare_list_l1(x2, x4, x8, Nil()) x12 -> True()
26: compare_list_l1(x2, x4, x8, Cons(x14, x16)) Nil() -> False()
27: compare_list_l1(x2, x4, x8, Cons(x14, x16)) Cons(x18, x20) -> x8 (x2 x14 x18) (compare_list(x2, x4, x8)
x16 x20) (x4 x14 x18)
28: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
29: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
30: main_4(x36, x15, x23, x27) x39 -> isort(insert(x27)) compare_list(x15, x23, x39) x36
33: ite2_cond_thenPart(True(), x10) x12 -> x10
34: ite2_cond_thenPart(False(), x10) x12 -> x12
35: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
36: ite2() x4 -> ite2_cond(x4)
37: main_3(x18, x23, x39) x59 -> isort(insert(x59)) compare_list(x23, x39, ite2()) x18
40: ite_cond_thenPart(True(), x8) x10 -> x8
41: ite_cond_thenPart(False(), x8) x10 -> x10
42: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
43: ite() x3 -> ite_cond(x3)
44: main_2(x18, x27) x43 -> isort(insert(ite())) compare_list(x27, x43, ite2()) x18
50: ltNat_x(x4) 0() -> False()
51: ltNat_x(0()) S(x8) -> True()
52: ltNat_x(S(x10)) S(x8) -> ltNat() x10 x8
53: ltNat_1() x2 -> ltNat_x(x2)
54: ltNat() x4 -> ltNat_x(x4)
55: main_1(x18) x39 -> isort(insert(ite())) compare_list(x39, ltNat(), ite2()) x18
64: eqNat_x(0()) 0() -> True()
65: eqNat_x(S(x6)) 0() -> False()
66: eqNat_x(S(x8)) S(x6) -> eqNat() x8 x6
67: eqNat_x(0()) S(x6) -> False()
68: eqNat_1() x1 -> eqNat_x(x1)
69: eqNat() x2 -> eqNat_x(x2)
70: main(x36) -> isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) x36
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
NeededRules
+ Details:
none
* Step 12: CFA MAYBE
+ Considered Problem:
1: main_9(x0) x9 -> x9 x0
2: main_10(x8) x9 -> x8 x9
3: main_8(x18) x16 -> x16 x18
4: main_7(x18, x47) x63 -> x63 x47 x18
5: isort_le(x12, x14) Nil() -> Nil()
6: isort_le(x12, x14) Cons(x18, x20) -> x12 x14 x18 (isort(x12) x14 x20)
7: isort_1(x6) x7 -> isort_le(x6, x7)
8: isort(x12) x14 -> isort_le(x12, x14)
9: main_6(x18, x43) x55 -> isort(x55) x43 x18
10: insert_le_x(x6, x12, x14) Nil() -> Cons(x14, Nil())
11: insert_le_x(x6, x12, x14) Cons(x18, x20) -> x6 (x12 x18 x14) Cons(x18, insert(x6) x12 x14 x20) Cons(x14
, Cons(x18
, x20))
12: insert_le(x3, x6) x7 -> insert_le_x(x3, x6, x7)
13: insert_1(x3) x6 -> insert_le(x3, x6)
14: insert(x6) x12 -> insert_le(x6, x12)
15: main_5(x18, x63) x91 -> isort(insert(x63)) x91 x18
16: compare_list_l1(x2, x4, x8, Nil()) x12 -> True()
17: compare_list_l1(x2, x4, x8, Cons(x14, x16)) Nil() -> False()
18: compare_list_l1(x2, x4, x8, Cons(x14, x16)) Cons(x18, x20) -> x8 (x2 x14 x18) (compare_list(x2, x4, x8)
x16 x20) (x4 x14 x18)
19: compare_list_1(x1, x2, x4) x5 -> compare_list_l1(x1, x2, x4, x5)
20: compare_list(x2, x4, x8) x10 -> compare_list_l1(x2, x4, x8, x10)
21: main_4(x36, x15, x23, x27) x39 -> isort(insert(x27)) compare_list(x15, x23, x39) x36
22: ite2_cond_thenPart(True(), x10) x12 -> x10
23: ite2_cond_thenPart(False(), x10) x12 -> x12
24: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
25: ite2() x4 -> ite2_cond(x4)
26: main_3(x18, x23, x39) x59 -> isort(insert(x59)) compare_list(x23, x39, ite2()) x18
27: ite_cond_thenPart(True(), x8) x10 -> x8
28: ite_cond_thenPart(False(), x8) x10 -> x10
29: ite_cond(x3) x4 -> ite_cond_thenPart(x3, x4)
30: ite() x3 -> ite_cond(x3)
31: main_2(x18, x27) x43 -> isort(insert(ite())) compare_list(x27, x43, ite2()) x18
32: ltNat_x(x4) 0() -> False()
33: ltNat_x(0()) S(x8) -> True()
34: ltNat_x(S(x10)) S(x8) -> ltNat() x10 x8
35: ltNat_1() x2 -> ltNat_x(x2)
36: ltNat() x4 -> ltNat_x(x4)
37: main_1(x18) x39 -> isort(insert(ite())) compare_list(x39, ltNat(), ite2()) x18
38: eqNat_x(0()) 0() -> True()
39: eqNat_x(S(x6)) 0() -> False()
40: eqNat_x(S(x8)) S(x6) -> eqNat() x8 x6
41: eqNat_x(0()) S(x6) -> False()
42: eqNat_1() x1 -> eqNat_x(x1)
43: eqNat() x2 -> eqNat_x(x2)
44: main(x36) -> isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) x36
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list_1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat_1 :: nat -> nat -> bool
insert_1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_1 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat_1 :: nat -> nat -> bool
main_1 :: nat list list -> (nat -> nat -> bool) -> nat list list
main_2 :: nat list list -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> nat list list
main_3 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> nat list list
main_4 :: nat list list
-> (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> nat list list -> nat list list -> nat list list)
-> (bool -> bool -> bool -> bool)
-> nat list list
main_5 :: nat list list
-> (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
main_6 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> nat list list
main_7 :: nat list list
-> (nat list -> nat list -> bool)
-> ((nat list -> nat list -> bool) -> nat list list -> nat list list)
-> nat list list
main_8 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_9 :: nat list list -> (nat list list -> nat list list) -> nat list list
main_10 :: (nat list list -> nat list list) -> nat list list -> nat list list
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
CFA {cfaRefinement = <control flow analysis>}
+ Details:
{X{*} -> False()
| S(X{*})
| 0()
| S(X{*})
| S(X{*})
| False()
| 0()
| S(X{*})
| True()
| 0()
| 0()
| S(X{*})
| S(X{*})
| True()
| S(X{*})
| 0()
| False()
| 0()
| False()
| True()
| False()
| True()
| Cons(X{*},X{*})
| Cons(X{*},X{*})
| False()
| Nil()
| Cons(X{*},X{*})
| True()
| Nil()
| Cons(X{*},X{*})
| Cons(X{*},X{*})
| Cons(X{*},X{*})
| Cons(X{*},X{*})
| Nil()
| Cons(X{*},X{*})
| Nil()
| Cons(X{*},X{*})
| Nil()
| Nil()
,V{x2_16} -> V{x2_20}
,V{x2_17} -> V{x2_20}
,V{x2_18} -> V{x2_20}
,V{x2_20} -> V{x2_18}
| eqNat()
,V{x2_43} -> V{x8_40}
| V{x14_18}
,V{x3_12} -> V{x6_14}
,V{x3_29} -> V{x3_30}
,V{x3_30} -> R{18}
| R{16}
| R{17}
,V{x4_16} -> V{x4_20}
,V{x4_17} -> V{x4_20}
,V{x4_18} -> V{x4_20}
,V{x4_20} -> V{x4_18}
| ltNat()
,V{x4_24} -> V{x4_25}
,V{x4_25} -> R{40}
| R{38}
| R{39}
| R{41}
,V{x4_29} -> Cons(V{x18_11},R{11})
| Cons(V{x18_11},R{10})
,V{x4_32} -> V{x4_36}
,V{x4_36} -> V{x10_34}
| V{x14_18}
,V{x5_24} -> R{18}
| R{16}
| R{17}
,V{x6_10} -> V{x3_12}
,V{x6_11} -> V{x3_12}
,V{x6_12} -> V{x12_14}
,V{x6_14} -> V{x6_11}
| ite()
,V{x6_39} -> X{*}
,V{x6_40} -> X{*}
,V{x6_41} -> X{*}
,V{x7_12} -> V{x14_11}
| V{x18_6}
,V{x8_16} -> V{x8_20}
,V{x8_17} -> V{x8_20}
,V{x8_18} -> V{x8_20}
,V{x8_20} -> V{x8_18}
| ite2()
,V{x8_27} -> V{x4_29}
,V{x8_28} -> V{x4_29}
,V{x8_33} -> X{*}
,V{x8_34} -> X{*}
,V{x8_40} -> X{*}
,V{x10_20} -> V{x16_18}
| V{x18_11}
,V{x10_22} -> V{x5_24}
,V{x10_23} -> V{x5_24}
,V{x10_27} -> Cons(V{x14_11},Cons(V{x18_11},V{x20_11}))
,V{x10_28} -> Cons(V{x14_11},Cons(V{x18_11},V{x20_11}))
,V{x10_34} -> X{*}
,V{x12_5} -> V{x12_8}
,V{x12_6} -> V{x12_8}
,V{x12_8} -> V{x12_6}
| insert(ite())
,V{x12_10} -> V{x6_12}
,V{x12_11} -> V{x6_12}
,V{x12_14} -> V{x12_11}
| V{x14_6}
,V{x12_16} -> V{x20_18}
| V{x14_11}
,V{x12_22} -> R{34}
| R{33}
| R{32}
,V{x12_23} -> R{34}
| R{33}
| R{32}
,V{x14_5} -> V{x14_8}
,V{x14_6} -> V{x14_8}
,V{x14_8} -> V{x14_6}
| compare_list(eqNat(),ltNat(),ite2())
,V{x14_10} -> V{x7_12}
,V{x14_11} -> V{x7_12}
,V{x14_17} -> X{*}
,V{x14_18} -> X{*}
,V{x16_17} -> X{*}
,V{x16_18} -> X{*}
,V{x18_6} -> X{*}
,V{x18_11} -> V{x18_11}
| V{x14_11}
| V{x14_10}
,V{x18_18} -> X{*}
,V{x20_6} -> X{*}
,V{x20_11} -> R{11}
| V{x20_11}
| R{10}
| Cons(V{x18_11},V{x20_11})
| Nil()
,V{x20_18} -> X{*}
,V{x36_44} -> X{*}
,R{0} -> R{44}
| main(X{*})
,R{5} -> Nil()
,R{6} -> R{11}
| R{10}
| @(R{12},R{6})
| @(R{12},R{5})
| @(@(R{14},V{x18_6}),R{5})
| @(@(R{14},V{x18_6}),R{6})
| @(R{12},@(R{8},V{x20_6}))
| @(R{12},@(@(isort(V{x12_6}),V{x14_6}),V{x20_6}))
| @(@(@(V{x12_6},V{x14_6}),V{x18_6}),R{6})
| @(@(@(V{x12_6},V{x14_6}),V{x18_6}),R{5})
| @(@(R{14},V{x18_6}),@(R{8},V{x20_6}))
| @(@(@(V{x12_6},V{x14_6}),V{x18_6}),@(R{8},V{x20_6}))
| @(@(R{14},V{x18_6}),@(@(isort(V{x12_6}),V{x14_6}),V{x20_6}))
| @(@(@(V{x12_6},V{x14_6}),V{x18_6}),@(@(isort(V{x12_6}),V{x14_6}),V{x20_6}))
,R{8} -> isort_le(V{x12_8},V{x14_8})
,R{10} -> Cons(V{x14_10},Nil())
,R{11} -> @(@(@(V{x6_11},@(@(V{x12_11},V{x18_11}),V{x14_11})),Cons(V{x18_11},R{11}))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(R{20},V{x14_11})),Cons(V{x18_11},R{11})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{16}),Cons(V{x18_11},R{11})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{17}),Cons(V{x18_11},R{11})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{18}),Cons(V{x18_11},R{11})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(R{30},Cons(V{x18_11},R{11})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| R{28}
| R{27}
| @(R{29},Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(R{30},Cons(V{x18_11},R{10})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{16}),Cons(V{x18_11},R{10})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{17}),Cons(V{x18_11},R{10})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{18}),Cons(V{x18_11},R{10})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(R{30},Cons(V{x18_11},@(R{12},V{x20_11}))),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(R{30},Cons(V{x18_11},@(@(R{14},V{x14_11}),V{x20_11}))),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{18}),Cons(V{x18_11},@(R{12},V{x20_11}))),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{17}),Cons(V{x18_11},@(R{12},V{x20_11}))),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{16}),Cons(V{x18_11},@(R{12},V{x20_11}))),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(R{20},V{x14_11})),Cons(V{x18_11},R{10})),Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(@(V{x12_11},V{x18_11}),V{x14_11})),Cons(V{x18_11},R{10}))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(R{20},V{x14_11})),Cons(V{x18_11},@(R{12},V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{16}),Cons(V{x18_11},@(@(R{14},V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{17}),Cons(V{x18_11},@(@(R{14},V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(R{30},Cons(V{x18_11},@(@(@(insert(V{x6_11}),V{x12_11}),V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{18}),Cons(V{x18_11},@(@(R{14},V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{18}),Cons(V{x18_11},@(@(@(insert(V{x6_11}),V{x12_11}),V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{17}),Cons(V{x18_11},@(@(@(insert(V{x6_11}),V{x12_11}),V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},R{16}),Cons(V{x18_11},@(@(@(insert(V{x6_11}),V{x12_11}),V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(@(V{x12_11},V{x18_11}),V{x14_11})),Cons(V{x18_11},@(R{12},V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(R{20},V{x14_11})),Cons(V{x18_11},@(@(R{14},V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(@(V{x12_11},V{x18_11}),V{x14_11})),Cons(V{x18_11},@(@(R{14},V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(R{20},V{x14_11}))
,Cons(V{x18_11},@(@(@(insert(V{x6_11}),V{x12_11}),V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
| @(@(@(V{x6_11},@(@(V{x12_11},V{x18_11}),V{x14_11}))
,Cons(V{x18_11},@(@(@(insert(V{x6_11}),V{x12_11}),V{x14_11}),V{x20_11})))
,Cons(V{x14_11},Cons(V{x18_11},V{x20_11})))
,R{12} -> insert_le_x(V{x3_12},V{x6_12},V{x7_12})
,R{14} -> insert_le(V{x6_14},V{x12_14})
,R{16} -> True()
,R{17} -> False()
,R{18} -> R{23}
| R{22}
| @(R{24},R{32})
| @(R{24},R{33})
| @(R{24},R{34})
| @(@(R{25},R{16}),R{34})
| @(@(R{25},R{16}),R{33})
| @(@(R{25},R{16}),R{32})
| @(@(R{25},R{17}),R{34})
| @(@(R{25},R{17}),R{33})
| @(@(R{25},R{17}),R{32})
| @(@(R{25},R{18}),R{34})
| @(@(R{25},R{18}),R{33})
| @(@(R{25},R{18}),R{32})
| @(R{24},@(R{36},V{x18_18}))
| @(R{24},@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(R{25},R{18}),@(R{36},V{x18_18}))
| @(@(R{25},R{17}),@(R{36},V{x18_18}))
| @(@(R{25},R{16}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{41}),R{18}),R{32})
| @(@(@(V{x8_18},R{41}),R{17}),R{32})
| @(@(@(V{x8_18},R{41}),R{16}),R{32})
| @(@(@(V{x8_18},R{41}),R{18}),R{33})
| @(@(@(V{x8_18},R{41}),R{17}),R{33})
| @(@(@(V{x8_18},R{41}),R{16}),R{33})
| @(@(@(V{x8_18},R{41}),R{18}),R{34})
| @(@(@(V{x8_18},R{41}),R{17}),R{34})
| @(@(@(V{x8_18},R{41}),R{16}),R{34})
| @(@(@(V{x8_18},R{40}),R{18}),R{32})
| @(@(@(V{x8_18},R{40}),R{17}),R{32})
| @(@(@(V{x8_18},R{40}),R{16}),R{32})
| @(@(@(V{x8_18},R{40}),R{18}),R{33})
| @(@(@(V{x8_18},R{40}),R{17}),R{33})
| @(@(@(V{x8_18},R{40}),R{16}),R{33})
| @(@(@(V{x8_18},R{40}),R{18}),R{34})
| @(@(@(V{x8_18},R{40}),R{17}),R{34})
| @(@(@(V{x8_18},R{40}),R{16}),R{34})
| @(@(@(V{x8_18},R{39}),R{18}),R{32})
| @(@(@(V{x8_18},R{39}),R{17}),R{32})
| @(@(@(V{x8_18},R{39}),R{16}),R{32})
| @(@(@(V{x8_18},R{39}),R{18}),R{33})
| @(@(@(V{x8_18},R{39}),R{17}),R{33})
| @(@(@(V{x8_18},R{39}),R{16}),R{33})
| @(@(@(V{x8_18},R{39}),R{18}),R{34})
| @(@(@(V{x8_18},R{39}),R{17}),R{34})
| @(@(@(V{x8_18},R{39}),R{16}),R{34})
| @(@(@(V{x8_18},R{38}),R{18}),R{32})
| @(@(@(V{x8_18},R{38}),R{17}),R{32})
| @(@(@(V{x8_18},R{38}),R{16}),R{32})
| @(@(R{25},@(R{20},V{x20_18})),R{32})
| @(@(@(V{x8_18},R{38}),R{18}),R{33})
| @(@(@(V{x8_18},R{38}),R{17}),R{33})
| @(@(@(V{x8_18},R{38}),R{16}),R{33})
| @(@(R{25},@(R{20},V{x20_18})),R{33})
| @(@(@(V{x8_18},R{38}),R{18}),R{34})
| @(@(@(V{x8_18},R{38}),R{17}),R{34})
| @(@(@(V{x8_18},R{38}),R{16}),R{34})
| @(@(R{25},@(R{20},V{x20_18})),R{34})
| @(@(@(V{x8_18},R{38}),@(R{20},V{x20_18})),R{34})
| @(@(@(V{x8_18},R{38}),@(R{20},V{x20_18})),R{33})
| @(@(@(V{x8_18},R{38}),@(R{20},V{x20_18})),R{32})
| @(@(@(V{x8_18},R{39}),@(R{20},V{x20_18})),R{34})
| @(@(@(V{x8_18},R{39}),@(R{20},V{x20_18})),R{33})
| @(@(@(V{x8_18},R{39}),@(R{20},V{x20_18})),R{32})
| @(@(@(V{x8_18},R{40}),@(R{20},V{x20_18})),R{34})
| @(@(@(V{x8_18},R{40}),@(R{20},V{x20_18})),R{33})
| @(@(@(V{x8_18},R{40}),@(R{20},V{x20_18})),R{32})
| @(@(@(V{x8_18},R{41}),@(R{20},V{x20_18})),R{34})
| @(@(@(V{x8_18},R{41}),@(R{20},V{x20_18})),R{33})
| @(@(@(V{x8_18},R{41}),@(R{20},V{x20_18})),R{32})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{16}),R{34})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{16}),R{33})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{16}),R{32})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{17}),R{34})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{17}),R{33})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{17}),R{32})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{18}),R{34})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{18}),R{33})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{18}),R{32})
| @(@(@(V{x8_18},R{38}),R{16}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{39}),R{16}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{40}),R{16}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{41}),R{16}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{38}),R{17}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{39}),R{17}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{40}),R{17}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{41}),R{17}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{38}),R{18}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{39}),R{18}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{40}),R{18}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{41}),R{18}),@(R{36},V{x18_18}))
| @(@(R{25},@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{34})
| @(@(R{25},@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{33})
| @(@(R{25},@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{32})
| @(@(R{25},@(R{20},V{x20_18})),@(R{36},V{x18_18}))
| @(@(R{25},R{18}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(R{25},R{17}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(R{25},R{16}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(R{25},@(R{20},V{x20_18})),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(R{25},@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{41}),R{18}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{40}),R{18}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{39}),R{18}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{38}),R{18}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{41}),R{17}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{40}),R{17}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{39}),R{17}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{38}),R{17}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{41}),R{16}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{40}),R{16}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{39}),R{16}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{38}),R{16}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{18}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{17}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{16}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{41}),@(R{20},V{x20_18})),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{40}),@(R{20},V{x20_18})),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{39}),@(R{20},V{x20_18})),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{38}),@(R{20},V{x20_18})),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{41}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{34})
| @(@(@(V{x8_18},R{40}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{34})
| @(@(@(V{x8_18},R{39}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{34})
| @(@(@(V{x8_18},R{38}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{34})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{18}),R{34})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{17}),R{34})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{16}),R{34})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(R{20},V{x20_18})),R{34})
| @(@(@(V{x8_18},R{41}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{33})
| @(@(@(V{x8_18},R{40}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{33})
| @(@(@(V{x8_18},R{39}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{33})
| @(@(@(V{x8_18},R{38}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{33})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{18}),R{33})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{17}),R{33})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{16}),R{33})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(R{20},V{x20_18})),R{33})
| @(@(@(V{x8_18},R{41}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{32})
| @(@(@(V{x8_18},R{40}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{32})
| @(@(@(V{x8_18},R{39}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{32})
| @(@(@(V{x8_18},R{38}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18})),R{32})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{18}),R{32})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{17}),R{32})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{16}),R{32})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(R{20},V{x20_18})),R{32})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),@(R{20},V{x20_18})),R{32})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,R{32})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),@(R{20},V{x20_18})),R{33})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,R{33})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),@(R{20},V{x20_18})),R{34})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,R{34})
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(R{20},V{x20_18})),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{16}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{16}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{17}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{17}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{18}),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),R{18}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{38}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{38}),@(R{20},V{x20_18})),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{39}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{39}),@(R{20},V{x20_18})),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{40}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{40}),@(R{20},V{x20_18})),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{41}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(R{36},V{x18_18}))
| @(@(@(V{x8_18},R{41}),@(R{20},V{x20_18})),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(R{25},@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{41}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{40}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{39}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},R{38}),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{18}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{17}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),R{16}),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(R{20},V{x20_18})),@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18}))
,@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,R{34})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18}))
,@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,R{33})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18}))
,@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,R{32})
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),@(R{20},V{x20_18})),@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18}))
,@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(R{36},V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18})),@(R{20},V{x20_18}))
,@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(R{43},V{x18_18})),@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(@(V{x4_18},V{x14_18}),V{x18_18}))
| @(@(@(V{x8_18},@(@(V{x2_18},V{x14_18}),V{x18_18}))
,@(@(compare_list(V{x2_18},V{x4_18},V{x8_18}),V{x16_18}),V{x20_18}))
,@(@(V{x4_18},V{x14_18}),V{x18_18}))
,R{20} -> compare_list_l1(V{x2_20},V{x4_20},V{x8_20},V{x10_20})
,R{22} -> V{x10_22}
,R{23} -> V{x12_23}
,R{24} -> ite2_cond_thenPart(V{x4_24},V{x5_24})
,R{25} -> ite2_cond(V{x4_25})
,R{27} -> V{x8_27}
,R{28} -> V{x10_28}
,R{29} -> ite_cond_thenPart(V{x3_29},V{x4_29})
,R{30} -> ite_cond(V{x3_30})
,R{32} -> False()
,R{33} -> True()
,R{34} -> R{34}
| R{33}
| R{32}
| @(R{36},V{x8_34})
| @(@(ltNat(),V{x10_34}),V{x8_34})
,R{36} -> ltNat_x(V{x4_36})
,R{38} -> True()
,R{39} -> False()
,R{40} -> R{41}
| R{40}
| R{39}
| R{38}
| @(R{43},V{x6_40})
| @(@(eqNat(),V{x8_40}),V{x6_40})
,R{41} -> False()
,R{43} -> eqNat_x(V{x2_43})
,R{44} -> R{6}
| R{5}
| @(R{8},V{x36_44})
| @(@(isort(insert(ite())),compare_list(eqNat(),ltNat(),ite2())),V{x36_44})}
* Step 13: UncurryATRS MAYBE
+ Considered Problem:
5: isort_le(insert(ite()), compare_list(eqNat(), ltNat(), ite2())) Nil() -> Nil()
6: isort_le(insert(ite()), compare_list(eqNat(), ltNat(), ite2())) Cons(x2, x1) -> insert(ite())
compare_list(eqNat(), ltNat(), ite2()) x2 (isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) x1)
8: isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) -> isort_le(insert(ite())
, compare_list(eqNat(), ltNat()
, ite2()))
10: insert_le_x(ite(), compare_list(eqNat(), ltNat(), ite2()), x1) Nil() -> Cons(x1, Nil())
11: insert_le_x(ite(), compare_list(eqNat(), ltNat(), ite2()), x3) Cons(x2, x1) -> ite()
(compare_list(eqNat(), ltNat(), ite2()) x2 x3) Cons(x2, insert(ite()) compare_list(eqNat(), ltNat()
, ite2()) x3 x1)
Cons(x3, Cons(x2, x1))
12: insert_le(ite(), compare_list(eqNat(), ltNat(), ite2())) x1 -> insert_le_x(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x1)
14: insert(ite()) compare_list(eqNat(), ltNat(), ite2()) -> insert_le(ite(), compare_list(eqNat(), ltNat()
, ite2()))
16: compare_list_l1(eqNat(), ltNat(), ite2(), Nil()) x1 -> True()
17: compare_list_l1(eqNat(), ltNat(), ite2(), Cons(x2, x1)) Nil() -> False()
18: compare_list_l1(eqNat(), ltNat(), ite2(), Cons(x4, x3)) Cons(x2, x1) -> ite2() (eqNat() x4 x2)
(compare_list(eqNat(), ltNat(), ite2()) x3 x1) (ltNat() x4 x2)
20: compare_list(eqNat(), ltNat(), ite2()) x1 -> compare_list_l1(eqNat(), ltNat(), ite2(), x1)
22: ite2_cond_thenPart(True(), x10) x12 -> x10
23: ite2_cond_thenPart(False(), x10) x12 -> x12
24: ite2_cond(x4) x5 -> ite2_cond_thenPart(x4, x5)
25: ite2() x4 -> ite2_cond(x4)
27: ite_cond_thenPart(True(), Cons(x4, x5)) Cons(x1, Cons(x2, x3)) -> Cons(x4, x5)
28: ite_cond_thenPart(False(), Cons(x4, x5)) Cons(x1, Cons(x2, x3)) -> Cons(x1, Cons(x2, x3))
29: ite_cond(x3) Cons(x1, x2) -> ite_cond_thenPart(x3, Cons(x1, x2))
30: ite() x3 -> ite_cond(x3)
32: ltNat_x(x4) 0() -> False()
33: ltNat_x(0()) S(x8) -> True()
34: ltNat_x(S(x2)) S(x1) -> ltNat() x2 x1
36: ltNat() x4 -> ltNat_x(x4)
38: eqNat_x(0()) 0() -> True()
39: eqNat_x(S(x6)) 0() -> False()
40: eqNat_x(S(x2)) S(x1) -> eqNat() x2 x1
41: eqNat_x(0()) S(x6) -> False()
43: eqNat() x2 -> eqNat_x(x2)
44: main(x1) -> isort(insert(ite())) compare_list(eqNat(), ltNat(), ite2()) x1
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite2_cond :: bool -> bool -> bool -> bool
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite2_cond_thenPart :: bool -> bool -> bool -> bool
eqNat_x :: nat -> nat -> bool
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
ltNat_x :: nat -> nat -> bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ltNat :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
UncurryATRS
+ Details:
none
* Step 14: Inline MAYBE
+ Considered Problem:
1: isort_le#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Nil()) -> Nil()
2: isort_le#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Cons(x2, x1)) -> insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x2
, isort#2(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x1))
3: isort#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2())) -> isort_le(insert(ite())
, compare_list(eqNat(), ltNat()
, ite2()))
4: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x0) -> isort_le#1(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x0)
5: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, Nil()) -> Cons(x1, Nil())
6: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x3, Cons(x2, x1)) ->
ite#3(compare_list#2(eqNat(), ltNat(), ite2(), x2, x3), Cons(x2, insert#3(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x3
, x1))
, Cons(x3, Cons(x2, x1)))
7: insert_le#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x1) -> insert_le_x(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x1)
8: insert_le#2(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, x2) -> insert_le_x#1(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x1
, x2)
9: insert#1(ite(), compare_list(eqNat(), ltNat(), ite2())) -> insert_le(ite(), compare_list(eqNat(), ltNat()
, ite2()))
10: insert#2(ite(), compare_list(eqNat(), ltNat(), ite2()), x0) -> insert_le#1(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x0)
11: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x0, x1) -> insert_le#2(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x0
, x1)
12: compare_list_l1#1(eqNat(), ltNat(), ite2(), Nil(), x1) -> True()
13: compare_list_l1#1(eqNat(), ltNat(), ite2(), Cons(x2, x1), Nil()) -> False()
14: compare_list_l1#1(eqNat(), ltNat(), ite2(), Cons(x4, x3), Cons(x2, x1)) -> ite2#3(eqNat#2(x4, x2)
, compare_list#2(eqNat()
, ltNat()
, ite2()
, x3
, x1)
, ltNat#2(x4, x2))
15: compare_list#1(eqNat(), ltNat(), ite2(), x1) -> compare_list_l1(eqNat(), ltNat(), ite2(), x1)
16: compare_list#2(eqNat(), ltNat(), ite2(), x1, x2) -> compare_list_l1#1(eqNat(), ltNat(), ite2(), x1, x2)
17: ite2_cond_thenPart#1(True(), x10, x12) -> x10
18: ite2_cond_thenPart#1(False(), x10, x12) -> x12
19: ite2_cond#1(x4, x5) -> ite2_cond_thenPart(x4, x5)
20: ite2_cond#2(x4, x5, x6) -> ite2_cond_thenPart#1(x4, x5, x6)
21: ite2#1(x4) -> ite2_cond(x4)
22: ite2#2(x4, x5) -> ite2_cond#1(x4, x5)
23: ite2#3(x4, x5, x6) -> ite2_cond#2(x4, x5, x6)
24: ite_cond_thenPart#1(True(), Cons(x4, x5), Cons(x1, Cons(x2, x3))) -> Cons(x4, x5)
25: ite_cond_thenPart#1(False(), Cons(x4, x5), Cons(x1, Cons(x2, x3))) -> Cons(x1, Cons(x2, x3))
26: ite_cond#1(x3, Cons(x1, x2)) -> ite_cond_thenPart(x3, Cons(x1, x2))
27: ite_cond#2(x3, Cons(x1, x2), x4) -> ite_cond_thenPart#1(x3, Cons(x1, x2), x4)
28: ite#1(x3) -> ite_cond(x3)
29: ite#2(x3, x4) -> ite_cond#1(x3, x4)
30: ite#3(x3, x4, x5) -> ite_cond#2(x3, x4, x5)
31: ltNat_x#1(x4, 0()) -> False()
32: ltNat_x#1(0(), S(x8)) -> True()
33: ltNat_x#1(S(x2), S(x1)) -> ltNat#2(x2, x1)
34: ltNat#1(x4) -> ltNat_x(x4)
35: ltNat#2(x4, x5) -> ltNat_x#1(x4, x5)
36: eqNat_x#1(0(), 0()) -> True()
37: eqNat_x#1(S(x6), 0()) -> False()
38: eqNat_x#1(S(x2), S(x1)) -> eqNat#2(x2, x1)
39: eqNat_x#1(0(), S(x6)) -> False()
40: eqNat#1(x2) -> eqNat_x(x2)
41: eqNat#2(x2, x3) -> eqNat_x#1(x2, x3)
42: main(x1) -> isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x1)
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#2 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list_l1#1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
eqNat#1 :: nat -> nat -> bool
eqNat#2 :: nat -> nat -> bool
eqNat_x :: nat -> nat -> bool
eqNat_x#1 :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#2 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#3 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le#2 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le_x#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort#1 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
isort#2 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
isort_le#1 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite :: bool -> nat list list -> nat list list -> nat list list
ite#1 :: bool -> nat list list -> nat list list -> nat list list
ite#2 :: bool -> nat list list -> nat list list -> nat list list
ite#3 :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
ite2#1 :: bool -> bool -> bool -> bool
ite2#2 :: bool -> bool -> bool -> bool
ite2#3 :: bool -> bool -> bool -> bool
ite2_cond :: bool -> bool -> bool -> bool
ite2_cond#1 :: bool -> bool -> bool -> bool
ite2_cond#2 :: bool -> bool -> bool -> bool
ite2_cond_thenPart :: bool -> bool -> bool -> bool
ite2_cond_thenPart#1 :: bool -> bool -> bool -> bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite_cond#1 :: bool -> nat list list -> nat list list -> nat list list
ite_cond#2 :: bool -> nat list list -> nat list list -> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite_cond_thenPart#1 :: bool -> nat list list -> nat list list -> nat list list
ltNat :: nat -> nat -> bool
ltNat#1 :: nat -> nat -> bool
ltNat#2 :: nat -> nat -> bool
ltNat_x :: nat -> nat -> bool
ltNat_x#1 :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
+ Details:
none
* Step 15: UsableRules MAYBE
+ Considered Problem:
1: isort_le#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Nil()) -> Nil()
2: isort_le#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Cons(x2, x1)) -> insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x2
, isort#2(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x1))
3: isort#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2())) -> isort_le(insert(ite())
, compare_list(eqNat(), ltNat()
, ite2()))
4: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x0) -> isort_le#1(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x0)
5: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, Nil()) -> Cons(x1, Nil())
6: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x3, Cons(x2, x1)) ->
ite#3(compare_list#2(eqNat(), ltNat(), ite2(), x2, x3), Cons(x2, insert#3(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x3
, x1))
, Cons(x3, Cons(x2, x1)))
7: insert_le#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x1) -> insert_le_x(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x1)
8: insert_le#2(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, x2) -> insert_le_x#1(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x1
, x2)
9: insert#1(ite(), compare_list(eqNat(), ltNat(), ite2())) -> insert_le(ite(), compare_list(eqNat(), ltNat()
, ite2()))
10: insert#2(ite(), compare_list(eqNat(), ltNat(), ite2()), x0) -> insert_le#1(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x0)
11: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x0, x1) -> insert_le#2(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x0
, x1)
12: compare_list_l1#1(eqNat(), ltNat(), ite2(), Nil(), x1) -> True()
13: compare_list_l1#1(eqNat(), ltNat(), ite2(), Cons(x2, x1), Nil()) -> False()
14: compare_list_l1#1(eqNat(), ltNat(), ite2(), Cons(x4, x3), Cons(x2, x1)) -> ite2#3(eqNat#2(x4, x2)
, compare_list#2(eqNat()
, ltNat()
, ite2()
, x3
, x1)
, ltNat#2(x4, x2))
15: compare_list#1(eqNat(), ltNat(), ite2(), x1) -> compare_list_l1(eqNat(), ltNat(), ite2(), x1)
16: compare_list#2(eqNat(), ltNat(), ite2(), x1, x2) -> compare_list_l1#1(eqNat(), ltNat(), ite2(), x1, x2)
17: ite2_cond_thenPart#1(True(), x10, x12) -> x10
18: ite2_cond_thenPart#1(False(), x10, x12) -> x12
19: ite2_cond#1(x4, x5) -> ite2_cond_thenPart(x4, x5)
20: ite2_cond#2(True(), x20, x24) -> x20
21: ite2_cond#2(False(), x20, x24) -> x24
22: ite2#1(x4) -> ite2_cond(x4)
23: ite2#2(x4, x5) -> ite2_cond#1(x4, x5)
24: ite2#3(x4, x5, x6) -> ite2_cond#2(x4, x5, x6)
25: ite_cond_thenPart#1(True(), Cons(x4, x5), Cons(x1, Cons(x2, x3))) -> Cons(x4, x5)
26: ite_cond_thenPart#1(False(), Cons(x4, x5), Cons(x1, Cons(x2, x3))) -> Cons(x1, Cons(x2, x3))
27: ite_cond#1(x3, Cons(x1, x2)) -> ite_cond_thenPart(x3, Cons(x1, x2))
28: ite_cond#2(True(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x8, x10)
29: ite_cond#2(False(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x2, Cons(x4, x6))
30: ite#1(x3) -> ite_cond(x3)
31: ite#2(x3, x4) -> ite_cond#1(x3, x4)
32: ite#3(x3, x4, x5) -> ite_cond#2(x3, x4, x5)
33: ltNat_x#1(x4, 0()) -> False()
34: ltNat_x#1(0(), S(x8)) -> True()
35: ltNat_x#1(S(x2), S(x1)) -> ltNat#2(x2, x1)
36: ltNat#1(x4) -> ltNat_x(x4)
37: ltNat#2(x4, x5) -> ltNat_x#1(x4, x5)
38: eqNat_x#1(0(), 0()) -> True()
39: eqNat_x#1(S(x6), 0()) -> False()
40: eqNat_x#1(S(x2), S(x1)) -> eqNat#2(x2, x1)
41: eqNat_x#1(0(), S(x6)) -> False()
42: eqNat#1(x2) -> eqNat_x(x2)
43: eqNat#2(x2, x3) -> eqNat_x#1(x2, x3)
44: main(x1) -> isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x1)
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#2 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list_l1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list_l1#1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
eqNat#1 :: nat -> nat -> bool
eqNat#2 :: nat -> nat -> bool
eqNat_x :: nat -> nat -> bool
eqNat_x#1 :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#2 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#3 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le#2 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le_x :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le_x#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort#1 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
isort#2 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
isort_le :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
isort_le#1 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite :: bool -> nat list list -> nat list list -> nat list list
ite#1 :: bool -> nat list list -> nat list list -> nat list list
ite#2 :: bool -> nat list list -> nat list list -> nat list list
ite#3 :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
ite2#1 :: bool -> bool -> bool -> bool
ite2#2 :: bool -> bool -> bool -> bool
ite2#3 :: bool -> bool -> bool -> bool
ite2_cond :: bool -> bool -> bool -> bool
ite2_cond#1 :: bool -> bool -> bool -> bool
ite2_cond#2 :: bool -> bool -> bool -> bool
ite2_cond_thenPart :: bool -> bool -> bool -> bool
ite2_cond_thenPart#1 :: bool -> bool -> bool -> bool
ite_cond :: bool -> nat list list -> nat list list -> nat list list
ite_cond#1 :: bool -> nat list list -> nat list list -> nat list list
ite_cond#2 :: bool -> nat list list -> nat list list -> nat list list
ite_cond_thenPart :: bool -> nat list list -> nat list list -> nat list list
ite_cond_thenPart#1 :: bool -> nat list list -> nat list list -> nat list list
ltNat :: nat -> nat -> bool
ltNat#1 :: nat -> nat -> bool
ltNat#2 :: nat -> nat -> bool
ltNat_x :: nat -> nat -> bool
ltNat_x#1 :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 16: Inline MAYBE
+ Considered Problem:
1: isort_le#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Nil()) -> Nil()
2: isort_le#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Cons(x2, x1)) -> insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x2
, isort#2(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x1))
4: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x0) -> isort_le#1(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x0)
5: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, Nil()) -> Cons(x1, Nil())
6: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x3, Cons(x2, x1)) ->
ite#3(compare_list#2(eqNat(), ltNat(), ite2(), x2, x3), Cons(x2, insert#3(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x3
, x1))
, Cons(x3, Cons(x2, x1)))
8: insert_le#2(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, x2) -> insert_le_x#1(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x1
, x2)
11: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x0, x1) -> insert_le#2(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x0
, x1)
12: compare_list_l1#1(eqNat(), ltNat(), ite2(), Nil(), x1) -> True()
13: compare_list_l1#1(eqNat(), ltNat(), ite2(), Cons(x2, x1), Nil()) -> False()
14: compare_list_l1#1(eqNat(), ltNat(), ite2(), Cons(x4, x3), Cons(x2, x1)) -> ite2#3(eqNat#2(x4, x2)
, compare_list#2(eqNat()
, ltNat()
, ite2()
, x3
, x1)
, ltNat#2(x4, x2))
16: compare_list#2(eqNat(), ltNat(), ite2(), x1, x2) -> compare_list_l1#1(eqNat(), ltNat(), ite2(), x1, x2)
20: ite2_cond#2(True(), x20, x24) -> x20
21: ite2_cond#2(False(), x20, x24) -> x24
24: ite2#3(x4, x5, x6) -> ite2_cond#2(x4, x5, x6)
28: ite_cond#2(True(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x8, x10)
29: ite_cond#2(False(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x2, Cons(x4, x6))
32: ite#3(x3, x4, x5) -> ite_cond#2(x3, x4, x5)
33: ltNat_x#1(x4, 0()) -> False()
34: ltNat_x#1(0(), S(x8)) -> True()
35: ltNat_x#1(S(x2), S(x1)) -> ltNat#2(x2, x1)
37: ltNat#2(x4, x5) -> ltNat_x#1(x4, x5)
38: eqNat_x#1(0(), 0()) -> True()
39: eqNat_x#1(S(x6), 0()) -> False()
40: eqNat_x#1(S(x2), S(x1)) -> eqNat#2(x2, x1)
41: eqNat_x#1(0(), S(x6)) -> False()
43: eqNat#2(x2, x3) -> eqNat_x#1(x2, x3)
44: main(x1) -> isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x1)
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#2 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list_l1#1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
eqNat#2 :: nat -> nat -> bool
eqNat_x#1 :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#3 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le#2 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le_x#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort#2 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
isort_le#1 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite :: bool -> nat list list -> nat list list -> nat list list
ite#3 :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
ite2#3 :: bool -> bool -> bool -> bool
ite2_cond#2 :: bool -> bool -> bool -> bool
ite_cond#2 :: bool -> nat list list -> nat list list -> nat list list
ltNat :: nat -> nat -> bool
ltNat#2 :: nat -> nat -> bool
ltNat_x#1 :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
+ Details:
none
* Step 17: UsableRules MAYBE
+ Considered Problem:
1: isort_le#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Nil()) -> Nil()
2: isort_le#1(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Cons(x2, x1)) -> insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x2
, isort#2(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x1))
3: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Nil()) -> Nil()
4: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Cons(x4, x2)) -> insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x4
, isort#2(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x2))
5: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, Nil()) -> Cons(x1, Nil())
6: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x7, Cons(x5, x3)) ->
ite_cond#2(compare_list#2(eqNat(), ltNat(), ite2(), x5, x7), Cons(x5, insert#3(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x7
, x3))
, Cons(x7, Cons(x5, x3)))
7: insert_le#2(ite(), compare_list(eqNat(), ltNat(), ite2()), x2, Nil()) -> Cons(x2, Nil())
8: insert_le#2(ite(), compare_list(eqNat(), ltNat(), ite2()), x6, Cons(x4, x2)) ->
ite#3(compare_list#2(eqNat(), ltNat(), ite2(), x4, x6), Cons(x4, insert#3(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x6
, x2))
, Cons(x6, Cons(x4, x2)))
9: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x2, x4) -> insert_le_x#1(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x2
, x4)
10: compare_list_l1#1(eqNat(), ltNat(), ite2(), Nil(), x1) -> True()
11: compare_list_l1#1(eqNat(), ltNat(), ite2(), Cons(x2, x1), Nil()) -> False()
12: compare_list_l1#1(eqNat(), ltNat(), ite2(), Cons(x9, x7), Cons(x5, x3)) -> ite2_cond#2(eqNat#2(x9, x5)
, compare_list#2(eqNat()
, ltNat()
, ite2()
, x7
, x3)
, ltNat#2(x9, x5))
13: compare_list#2(eqNat(), ltNat(), ite2(), Nil(), x2) -> True()
14: compare_list#2(eqNat(), ltNat(), ite2(), Cons(x4, x2), Nil()) -> False()
15: compare_list#2(eqNat(), ltNat(), ite2(), Cons(x8, x6), Cons(x4, x2)) -> ite2#3(eqNat#2(x8, x4)
, compare_list#2(eqNat()
, ltNat()
, ite2()
, x6
, x2)
, ltNat#2(x8, x4))
16: ite2_cond#2(True(), x20, x24) -> x20
17: ite2_cond#2(False(), x20, x24) -> x24
18: ite2#3(True(), x40, x48) -> x40
19: ite2#3(False(), x40, x48) -> x48
20: ite_cond#2(True(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x8, x10)
21: ite_cond#2(False(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x2, Cons(x4, x6))
22: ite#3(True(), Cons(x16, x20), Cons(x4, Cons(x8, x12))) -> Cons(x16, x20)
23: ite#3(False(), Cons(x16, x20), Cons(x4, Cons(x8, x12))) -> Cons(x4, Cons(x8, x12))
24: ltNat_x#1(x4, 0()) -> False()
25: ltNat_x#1(0(), S(x8)) -> True()
26: ltNat_x#1(S(x2), S(x1)) -> ltNat#2(x2, x1)
27: ltNat#2(x8, 0()) -> False()
28: ltNat#2(0(), S(x16)) -> True()
29: ltNat#2(S(x4), S(x2)) -> ltNat#2(x4, x2)
30: eqNat_x#1(0(), 0()) -> True()
31: eqNat_x#1(S(x6), 0()) -> False()
32: eqNat_x#1(S(x2), S(x1)) -> eqNat#2(x2, x1)
33: eqNat_x#1(0(), S(x6)) -> False()
34: eqNat#2(0(), 0()) -> True()
35: eqNat#2(S(x12), 0()) -> False()
36: eqNat#2(S(x4), S(x2)) -> eqNat#2(x4, x2)
37: eqNat#2(0(), S(x12)) -> False()
38: main(x1) -> isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x1)
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#2 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list_l1#1 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
eqNat#2 :: nat -> nat -> bool
eqNat_x#1 :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#3 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le#2 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le_x#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort#2 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
isort_le#1 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite :: bool -> nat list list -> nat list list -> nat list list
ite#3 :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
ite2#3 :: bool -> bool -> bool -> bool
ite2_cond#2 :: bool -> bool -> bool -> bool
ite_cond#2 :: bool -> nat list list -> nat list list -> nat list list
ltNat :: nat -> nat -> bool
ltNat#2 :: nat -> nat -> bool
ltNat_x#1 :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 18: Inline MAYBE
+ Considered Problem:
3: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Nil()) -> Nil()
4: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Cons(x4, x2)) -> insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x4
, isort#2(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x2))
5: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, Nil()) -> Cons(x1, Nil())
6: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x7, Cons(x5, x3)) ->
ite_cond#2(compare_list#2(eqNat(), ltNat(), ite2(), x5, x7), Cons(x5, insert#3(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x7
, x3))
, Cons(x7, Cons(x5, x3)))
9: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x2, x4) -> insert_le_x#1(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x2
, x4)
13: compare_list#2(eqNat(), ltNat(), ite2(), Nil(), x2) -> True()
14: compare_list#2(eqNat(), ltNat(), ite2(), Cons(x4, x2), Nil()) -> False()
15: compare_list#2(eqNat(), ltNat(), ite2(), Cons(x8, x6), Cons(x4, x2)) -> ite2#3(eqNat#2(x8, x4)
, compare_list#2(eqNat()
, ltNat()
, ite2()
, x6
, x2)
, ltNat#2(x8, x4))
18: ite2#3(True(), x40, x48) -> x40
19: ite2#3(False(), x40, x48) -> x48
20: ite_cond#2(True(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x8, x10)
21: ite_cond#2(False(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x2, Cons(x4, x6))
27: ltNat#2(x8, 0()) -> False()
28: ltNat#2(0(), S(x16)) -> True()
29: ltNat#2(S(x4), S(x2)) -> ltNat#2(x4, x2)
34: eqNat#2(0(), 0()) -> True()
35: eqNat#2(S(x12), 0()) -> False()
36: eqNat#2(S(x4), S(x2)) -> eqNat#2(x4, x2)
37: eqNat#2(0(), S(x12)) -> False()
38: main(x1) -> isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x1)
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#2 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
eqNat#2 :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#3 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le_x#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort#2 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
ite2#3 :: bool -> bool -> bool -> bool
ite_cond#2 :: bool -> nat list list -> nat list list -> nat list list
ltNat :: nat -> nat -> bool
ltNat#2 :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Inline {inlineType = InlineFull, inlineSelect = <inline decreasing>}
+ Details:
none
* Step 19: UsableRules MAYBE
+ Considered Problem:
1: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Nil()) -> Nil()
2: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Cons(x4, x2)) -> insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x4
, isort#2(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x2))
3: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x1, Nil()) -> Cons(x1, Nil())
4: insert_le_x#1(ite(), compare_list(eqNat(), ltNat(), ite2()), x7, Cons(x5, x3)) ->
ite_cond#2(compare_list#2(eqNat(), ltNat(), ite2(), x5, x7), Cons(x5, insert#3(ite(), compare_list(eqNat()
, ltNat()
, ite2())
, x7
, x3))
, Cons(x7, Cons(x5, x3)))
5: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x2, Nil()) -> Cons(x2, Nil())
6: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x14, Cons(x10, x6)) ->
ite_cond#2(compare_list#2(eqNat(), ltNat(), ite2(), x10, x14), Cons(x10, insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x14
, x6))
, Cons(x14, Cons(x10, x6)))
7: compare_list#2(eqNat(), ltNat(), ite2(), Nil(), x2) -> True()
8: compare_list#2(eqNat(), ltNat(), ite2(), Cons(x4, x2), Nil()) -> False()
9: compare_list#2(eqNat(), ltNat(), ite2(), Cons(x8, x6), Cons(x4, x2)) -> ite2#3(eqNat#2(x8, x4)
, compare_list#2(eqNat()
, ltNat()
, ite2()
, x6
, x2)
, ltNat#2(x8, x4))
10: ite2#3(True(), x40, x48) -> x40
11: ite2#3(False(), x40, x48) -> x48
12: ite_cond#2(True(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x8, x10)
13: ite_cond#2(False(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x2, Cons(x4, x6))
14: ltNat#2(x8, 0()) -> False()
15: ltNat#2(0(), S(x16)) -> True()
16: ltNat#2(S(x4), S(x2)) -> ltNat#2(x4, x2)
17: eqNat#2(0(), 0()) -> True()
18: eqNat#2(S(x12), 0()) -> False()
19: eqNat#2(S(x4), S(x2)) -> eqNat#2(x4, x2)
20: eqNat#2(0(), S(x12)) -> False()
21: main(x1) -> isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x1)
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#2 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
eqNat#2 :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#3 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert_le_x#1 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort#2 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
ite2#3 :: bool -> bool -> bool -> bool
ite_cond#2 :: bool -> nat list list -> nat list list -> nat list list
ltNat :: nat -> nat -> bool
ltNat#2 :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
UsableRules {urType = Syntactic}
+ Details:
none
* Step 20: Compression MAYBE
+ Considered Problem:
1: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Nil()) -> Nil()
2: isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), Cons(x4, x2)) -> insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x4
, isort#2(insert(ite())
, compare_list(eqNat()
, ltNat()
, ite2())
, x2))
5: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x2, Nil()) -> Cons(x2, Nil())
6: insert#3(ite(), compare_list(eqNat(), ltNat(), ite2()), x14, Cons(x10, x6)) ->
ite_cond#2(compare_list#2(eqNat(), ltNat(), ite2(), x10, x14), Cons(x10, insert#3(ite()
, compare_list(eqNat()
, ltNat()
, ite2())
, x14
, x6))
, Cons(x14, Cons(x10, x6)))
7: compare_list#2(eqNat(), ltNat(), ite2(), Nil(), x2) -> True()
8: compare_list#2(eqNat(), ltNat(), ite2(), Cons(x4, x2), Nil()) -> False()
9: compare_list#2(eqNat(), ltNat(), ite2(), Cons(x8, x6), Cons(x4, x2)) -> ite2#3(eqNat#2(x8, x4)
, compare_list#2(eqNat()
, ltNat()
, ite2()
, x6
, x2)
, ltNat#2(x8, x4))
10: ite2#3(True(), x40, x48) -> x40
11: ite2#3(False(), x40, x48) -> x48
12: ite_cond#2(True(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x8, x10)
13: ite_cond#2(False(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x2, Cons(x4, x6))
14: ltNat#2(x8, 0()) -> False()
15: ltNat#2(0(), S(x16)) -> True()
16: ltNat#2(S(x4), S(x2)) -> ltNat#2(x4, x2)
17: eqNat#2(0(), 0()) -> True()
18: eqNat#2(S(x12), 0()) -> False()
19: eqNat#2(S(x4), S(x2)) -> eqNat#2(x4, x2)
20: eqNat#2(0(), S(x12)) -> False()
21: main(x1) -> isort#2(insert(ite()), compare_list(eqNat(), ltNat(), ite2()), x1)
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
compare_list :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
compare_list#2 :: (nat -> nat -> bool)
-> (nat -> nat -> bool)
-> (bool -> bool -> bool -> bool)
-> nat list
-> nat list
-> bool
eqNat :: nat -> nat -> bool
eqNat#2 :: nat -> nat -> bool
insert :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
insert#3 :: (bool -> nat list list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list
-> nat list list
-> nat list list
isort#2 :: ((nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list)
-> (nat list -> nat list -> bool)
-> nat list list
-> nat list list
ite :: bool -> nat list list -> nat list list -> nat list list
ite2 :: bool -> bool -> bool -> bool
ite2#3 :: bool -> bool -> bool -> bool
ite_cond#2 :: bool -> nat list list -> nat list list -> nat list list
ltNat :: nat -> nat -> bool
ltNat#2 :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
Compression
+ Details:
none
* Step 21: ToTctProblem MAYBE
+ Considered Problem:
1: isort#2(Nil()) -> Nil()
2: isort#2(Cons(x4, x2)) -> insert#3(x4, isort#2(x2))
3: insert#3(x2, Nil()) -> Cons(x2, Nil())
4: insert#3(x14, Cons(x10, x6)) -> ite_cond#2(compare_list#2(x10, x14), Cons(x10, insert#3(x14, x6))
, Cons(x14, Cons(x10, x6)))
5: compare_list#2(Nil(), x2) -> True()
6: compare_list#2(Cons(x4, x2), Nil()) -> False()
7: compare_list#2(Cons(x8, x6), Cons(x4, x2)) -> ite2#3(eqNat#2(x8, x4), compare_list#2(x6, x2)
, ltNat#2(x8, x4))
8: ite2#3(True(), x40, x48) -> x40
9: ite2#3(False(), x40, x48) -> x48
10: ite_cond#2(True(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x8, x10)
11: ite_cond#2(False(), Cons(x8, x10), Cons(x2, Cons(x4, x6))) -> Cons(x2, Cons(x4, x6))
12: ltNat#2(x8, 0()) -> False()
13: ltNat#2(0(), S(x16)) -> True()
14: ltNat#2(S(x4), S(x2)) -> ltNat#2(x4, x2)
15: eqNat#2(0(), 0()) -> True()
16: eqNat#2(S(x12), 0()) -> False()
17: eqNat#2(S(x4), S(x2)) -> eqNat#2(x4, x2)
18: eqNat#2(0(), S(x12)) -> False()
19: main(x1) -> isort#2(x1)
where
0 :: nat
Cons :: 'a -> 'a list -> 'a list
False :: bool
Nil :: 'a list
S :: nat -> nat
True :: bool
compare_list#2 :: nat list -> nat list -> bool
eqNat#2 :: nat -> nat -> bool
insert#3 :: nat list -> nat list list -> nat list list
isort#2 :: nat list list -> nat list list
ite2#3 :: bool -> bool -> bool -> bool
ite_cond#2 :: bool -> nat list list -> nat list list -> nat list list
ltNat#2 :: nat -> nat -> bool
main :: nat list list -> nat list list
+ Applied Processor:
ToTctProblem
+ Details:
none
* Step 22: Failure MAYBE
+ Considered Problem:
- Strict TRS:
compare_list#2(Cons(x4,x2),Nil()) -> False()
compare_list#2(Cons(x8,x6),Cons(x4,x2)) -> ite2#3(eqNat#2(x8,x4),compare_list#2(x6,x2),ltNat#2(x8,x4))
compare_list#2(Nil(),x2) -> True()
eqNat#2(0(),0()) -> True()
eqNat#2(0(),S(x12)) -> False()
eqNat#2(S(x12),0()) -> False()
eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2)
insert#3(x14,Cons(x10,x6)) -> ite_cond#2(compare_list#2(x10,x14)
,Cons(x10,insert#3(x14,x6))
,Cons(x14,Cons(x10,x6)))
insert#3(x2,Nil()) -> Cons(x2,Nil())
isort#2(Cons(x4,x2)) -> insert#3(x4,isort#2(x2))
isort#2(Nil()) -> Nil()
ite2#3(False(),x40,x48) -> x48
ite2#3(True(),x40,x48) -> x40
ite_cond#2(False(),Cons(x8,x10),Cons(x2,Cons(x4,x6))) -> Cons(x2,Cons(x4,x6))
ite_cond#2(True(),Cons(x8,x10),Cons(x2,Cons(x4,x6))) -> Cons(x8,x10)
ltNat#2(x8,0()) -> False()
ltNat#2(0(),S(x16)) -> True()
ltNat#2(S(x4),S(x2)) -> ltNat#2(x4,x2)
main(x1) -> isort#2(x1)
- Signature:
{compare_list#2/2,eqNat#2/2,insert#3/2,isort#2/1,ite2#3/3,ite_cond#2/3,ltNat#2/2,main/1} / {0/0,Cons/2
,False/0,Nil/0,S/1,True/0}
- Obligation:
innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,False,Nil,S,True}
+ Applied Processor:
EmptyProcessor
+ Details:
The problem is still open.
MAYBE