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: λxs : nat list list. (λeqNat : nat -> nat -> bool. (λltNat : nat -> nat -> bool. (λite : bool -> nat list list -> nat list list -> nat list list. (λite2 : bool -> bool -> bool -> bool. (λcompare_list : nat list -> nat list -> bool. (λinsert : (nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list. (λisort : (nat list -> nat list -> bool) -> nat list list -> nat list list. (λisort_list : nat list list -> nat list list. (λmain : nat list list -> nat list list. main xs) (λxs : nat list list. isort_list xs)) (isort compare_list)) (μisort : (nat list -> nat list -> bool) -> nat list list -> nat list list. λle : nat list -> nat list -> bool. λl : nat list list. case l of | Nil -> Nil | Cons -> λx : nat list. λxs : nat list list. insert le x (isort le xs))) (μinsert : (nat list -> nat list -> bool) -> nat list -> nat list list -> nat list list. λle : nat list -> nat list -> bool. λx : nat list. λl : nat list list. case l of | Nil -> Cons(x,Nil) | Cons -> λy : nat list. λys : nat list list. ite (le y x) Cons(y,insert le x ys) Cons(x,Cons(y,ys)))) (μcompare_list : nat list -> nat list -> bool. λl1 : nat list. λl2 : nat list. case l1 of | Nil -> True | Cons -> λx : nat. λxs : nat list. case l2 of | Nil -> False | Cons -> λy : nat. λys : nat list. ite2 (eqNat x y) (compare_list xs ys) (ltNat x y))) (λcond : bool. λthenPart : bool. λelsePart : bool. case cond of | True -> thenPart | False -> elsePart)) (λcond : bool. λthenPart : nat list list. λelsePart : nat list list. case cond of | True -> thenPart | False -> elsePart)) (μltNat : nat -> nat -> bool. λx : nat. λy : nat. case y of | 0 -> False | S -> λy' : nat. case x of | 0 -> True | S -> λx' : nat. ltNat x' y')) (μeqNat : nat -> nat -> bool. λx : nat. λy : nat. case y of | 0 -> case x of | 0 -> True | S -> λx' : nat. False | S -> λy' : nat. case x of | S -> λx' : nat. eqNat x' y' | 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 = } + 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 = } + 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 = } + 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 = } + 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 = } + 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 = } + 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 = } + 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 = } + 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 = } + 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 = } + 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 = } + 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