WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: let rec leqNat x y = 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 x with | 0 -> False | S(x') -> (match y with | 0 -> True | S(y') -> 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 b th el = match b with | True()-> th | False()-> el ;; let ite2 b th el = match b with | True()-> th | False()-> el ;; 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 'a option = None | Some of 'a ;; type 'a list = Nil | Cons of 'a * 'a list ;; type 'a treelist = NilTree | ConsTree of 'a * 'a treelist ;; type nat = 0 | S of nat ;; type Unit = Unit ;; type ('a,'b) pair = Pair of 'a * 'b ;; type bool = True | False ;; type tree = Leaf of nat list | Node of nat list * tree treelist ;; let rec anyEq nr ys = match ys with | Nil()-> False | Cons(x,xs) -> ite (eqNat nr x) True() (anyEq nr xs) ;; type Exception = Invalid_Tree;; let rec lookup n node = match node with | Leaf(xs) -> anyEq n xs | Node(nrs,tss) -> match nrs with | Nil()-> (match tss with | ConsTree(tGt,empty) -> lookup n tGt | NilTree -> error) | Cons(nr,ns) -> match tss with | ConsTree(t,ts) -> ite2 (leqNat n nr) (lookup n t) (lookup n (Node(ns,ts))) | NilTree -> error ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λn : nat. λnode : tree. (λleqNat : nat -> nat -> bool. (λeqNat : nat -> nat -> bool. (λite : bool -> bool -> bool -> bool. (λite2 : bool -> bool -> bool -> bool. (λanyEq : nat -> nat list -> bool. (λlookup : nat -> tree -> bool. lookup n node) (μlookup : nat -> tree -> bool. λn : nat. λnode : tree. case node of | Leaf -> λxs : nat list. anyEq n xs | Node -> λnrs : nat list. λtss : tree treelist. case nrs of | Nil -> case tss of | ConsTree -> λtGt : tree. λempty : tree treelist. lookup n tGt | NilTree -> ⟘  | Cons -> λnr : nat. λns : nat list. case tss of | ConsTree -> λt : tree. λts : tree treelist. ite2 (leqNat n nr) (lookup n t) (lookup n Node(ns,ts)) | NilTree -> ⟘ )) (μanyEq : nat -> nat list -> bool. λnr : nat. λys : nat list. case ys of | Nil -> False | Cons -> λx : nat. λxs : nat list. ite (eqNat nr x) True (anyEq nr xs))) (λb : bool. λth : bool. λel : bool. case b of | True -> th | False -> el)) (λb : bool. λth : bool. λel : bool. case b of | True -> th | False -> el)) (μ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)) (μleqNat : nat -> nat -> bool. λx : nat. λy : nat. case y of | 0 -> True | S -> λy' : nat. case x of | S -> λx' : nat. leqNat x' y' | 0 -> False) : nat -> tree -> bool where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Invalid_Tree :: Exception Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree 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 WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_7(x0, x1) x7 -> x7 x0 x1 2: cond_lookup_n_node_2(ConsTree(x11, x12), x2, x5, x6, x7) -> lookup(x2, x5, x6) x7 x11 3: cond_lookup_n_node_2(NilTree(), x2, x5, x6, x7) -> bot[0]() 4: cond_lookup_n_node_3(ConsTree(x13, x14), x2, x5, x6, x7, x11, x12) -> x5 (x2 x7 x11) (lookup(x2, x5, x6) x7 x13) (lookup(x2, x5, x6) x7 Node(x12, x14)) 5: cond_lookup_n_node_3(NilTree(), x2, x5, x6, x7, x11, x12) -> bot[1]() 6: cond_lookup_n_node_1(Nil(), x2, x5, x6, x7, x10) -> cond_lookup_n_node_2(x10, x2, x5, x6, x7) 7: cond_lookup_n_node_1(Cons(x11, x12), x2, x5, x6, x7, x10) -> cond_lookup_n_node_3(x10, x2 , x5 , x6 , x7 , x11 , x12) 8: cond_lookup_n_node(Leaf(x9), x2, x5, x6, x7) -> x6 x7 x9 9: cond_lookup_n_node(Node(x9, x10), x2, x5, x6, x7) -> cond_lookup_n_node_1(x9, x2, x5, x6, x7, x10) 10: lookup_n(x2, x5, x6, x7) x8 -> cond_lookup_n_node(x8, x2, x5, x6, x7) 11: lookup_1(x2, x5, x6) x7 -> lookup_n(x2, x5, x6, x7) 12: lookup(x2, x5, x6) x7 -> lookup_1(x2, x5, x6) x7 13: main_6(x0, x1, x2, x5) x6 -> main_7(x0, x1) lookup(x2, x5, x6) 14: cond_anyEq_nr_ys(Nil(), x3, x4, x6) -> False() 15: cond_anyEq_nr_ys(Cons(x8, x9), x3, x4, x6) -> x4 (x3 x6 x8) True() (anyEq(x3, x4) x6 x9) 16: anyEq_nr(x3, x4, x6) x7 -> cond_anyEq_nr_ys(x7, x3, x4, x6) 17: anyEq_1(x3, x4) x6 -> anyEq_nr(x3, x4, x6) 18: anyEq(x3, x4) x5 -> anyEq_1(x3, x4) x5 19: main_5(x0, x1, x2, x3, x4) x5 -> main_6(x0, x1, x2, x5) anyEq(x3, x4) 20: cond_ite2_b_th_el(True(), x6, x7) -> x6 21: cond_ite2_b_th_el(False(), x6, x7) -> x7 22: ite2_b_th(x5, x6) x7 -> cond_ite2_b_th_el(x5, x6, x7) 23: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 24: ite2() x5 -> ite2_b(x5) 25: main_4(x0, x1, x2, x3) x4 -> main_5(x0, x1, x2, x3, x4) ite2() 26: cond_ite_b_th_el(True(), x5, x6) -> x5 27: cond_ite_b_th_el(False(), x5, x6) -> x6 28: ite_b_th(x4, x5) x6 -> cond_ite_b_th_el(x4, x5, x6) 29: ite_b(x4) x5 -> ite_b_th(x4, x5) 30: ite() x4 -> ite_b(x4) 31: main_3(x0, x1, x2) x3 -> main_4(x0, x1, x2, x3) ite() 32: cond_eqNat_x_y_1(0()) -> True() 33: cond_eqNat_x_y_1(S(x5)) -> False() 34: cond_eqNat_x_y_2(S(x6), x5) -> eqNat() x6 x5 35: cond_eqNat_x_y_2(0(), x5) -> False() 36: cond_eqNat_x_y(0(), x3) -> cond_eqNat_x_y_1(x3) 37: cond_eqNat_x_y(S(x5), x3) -> cond_eqNat_x_y_2(x3, x5) 38: eqNat_x(x3) x4 -> cond_eqNat_x_y(x4, x3) 39: eqNat_1() x3 -> eqNat_x(x3) 40: eqNat() x0 -> eqNat_1() x0 41: main_2(x0, x1) x2 -> main_3(x0, x1, x2) eqNat() 42: cond_leqNat_x_y_1(S(x5), x4) -> leqNat() x5 x4 43: cond_leqNat_x_y_1(0(), x4) -> False() 44: cond_leqNat_x_y(0(), x2) -> True() 45: cond_leqNat_x_y(S(x4), x2) -> cond_leqNat_x_y_1(x2, x4) 46: leqNat_x(x2) x3 -> cond_leqNat_x_y(x3, x2) 47: leqNat_1() x2 -> leqNat_x(x2) 48: leqNat() x0 -> leqNat_1() x0 49: main(x0, x1) -> main_2(x0, x1) leqNat() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool anyEq_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat_1 :: nat -> nat -> bool leqNat_1 :: nat -> nat -> bool lookup_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main_2 :: nat -> tree -> (nat -> nat -> bool) -> bool main_3 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> bool main_4 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> bool main_5 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (bool -> bool -> bool -> bool) -> bool main_6 :: nat -> tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> bool main_7 :: nat -> tree -> (nat -> tree -> bool) -> bool bot[0] :: bool bot[1] :: bool cond_ite_b_th_el :: bool -> bool -> bool -> bool cond_ite2_b_th_el :: bool -> bool -> bool -> bool cond_lookup_n_node :: tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y :: nat -> nat -> bool cond_leqNat_x_y :: nat -> nat -> bool cond_anyEq_nr_ys :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> bool cond_lookup_n_node_1 :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree treelist -> bool cond_eqNat_x_y_1 :: nat -> bool cond_leqNat_x_y_1 :: nat -> nat -> bool cond_lookup_n_node_2 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y_2 :: nat -> nat -> bool cond_lookup_n_node_3 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> nat -> nat list -> bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_7(x0, x1) x7 -> x7 x0 x1 2: cond_lookup_n_node_2(ConsTree(x11, x12), x2, x5, x6, x7) -> lookup(x2, x5, x6) x7 x11 3: cond_lookup_n_node_2(NilTree(), x2, x5, x6, x7) -> bot[0]() 4: cond_lookup_n_node_3(ConsTree(x13, x14), x2, x5, x6, x7, x11, x12) -> x5 (x2 x7 x11) (lookup(x2, x5, x6) x7 x13) (lookup(x2, x5, x6) x7 Node(x12, x14)) 5: cond_lookup_n_node_3(NilTree(), x2, x5, x6, x7, x11, x12) -> bot[1]() 6: cond_lookup_n_node_1(Nil(), x2, x5, x6, x7, x10) -> cond_lookup_n_node_2(x10, x2, x5, x6, x7) 7: cond_lookup_n_node_1(Cons(x11, x12), x2, x5, x6, x7, x10) -> cond_lookup_n_node_3(x10, x2 , x5 , x6 , x7 , x11 , x12) 8: cond_lookup_n_node(Leaf(x9), x2, x5, x6, x7) -> x6 x7 x9 9: cond_lookup_n_node(Node(x9, x10), x2, x5, x6, x7) -> cond_lookup_n_node_1(x9, x2, x5, x6, x7, x10) 10: lookup_n(x2, x5, x6, x7) x8 -> cond_lookup_n_node(x8, x2, x5, x6, x7) 11: lookup_1(x2, x5, x6) x7 -> lookup_n(x2, x5, x6, x7) 12: lookup(x4, x10, x12) x14 -> lookup_n(x4, x10, x12, x14) 13: main_6(x0, x2, x5, x11) x13 -> lookup(x5, x11, x13) x0 x2 14: cond_anyEq_nr_ys(Nil(), x3, x4, x6) -> False() 15: cond_anyEq_nr_ys(Cons(x8, x9), x3, x4, x6) -> x4 (x3 x6 x8) True() (anyEq(x3, x4) x6 x9) 16: anyEq_nr(x3, x4, x6) x7 -> cond_anyEq_nr_ys(x7, x3, x4, x6) 17: anyEq_1(x3, x4) x6 -> anyEq_nr(x3, x4, x6) 18: anyEq(x6, x8) x12 -> anyEq_nr(x6, x8, x12) 19: main_5(x0, x2, x4, x7, x9) x10 -> main_7(x0, x2) lookup(x4, x10, anyEq(x7, x9)) 20: cond_ite2_b_th_el(True(), x6, x7) -> x6 21: cond_ite2_b_th_el(False(), x6, x7) -> x7 22: ite2_b_th(x5, x6) x7 -> cond_ite2_b_th_el(x5, x6, x7) 23: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 24: ite2() x5 -> ite2_b(x5) 25: main_4(x0, x2, x4, x6) x8 -> main_6(x0, x2, x4, ite2()) anyEq(x6, x8) 26: cond_ite_b_th_el(True(), x5, x6) -> x5 27: cond_ite_b_th_el(False(), x5, x6) -> x6 28: ite_b_th(x4, x5) x6 -> cond_ite_b_th_el(x4, x5, x6) 29: ite_b(x4) x5 -> ite_b_th(x4, x5) 30: ite() x4 -> ite_b(x4) 31: main_3(x0, x2, x4) x6 -> main_5(x0, x2, x4, x6, ite()) ite2() 32: cond_eqNat_x_y_1(0()) -> True() 33: cond_eqNat_x_y_1(S(x5)) -> False() 34: cond_eqNat_x_y_2(S(x6), x5) -> eqNat() x6 x5 35: cond_eqNat_x_y_2(0(), x5) -> False() 36: cond_eqNat_x_y(0(), x3) -> cond_eqNat_x_y_1(x3) 37: cond_eqNat_x_y(S(x5), x3) -> cond_eqNat_x_y_2(x3, x5) 38: eqNat_x(x3) x4 -> cond_eqNat_x_y(x4, x3) 39: eqNat_1() x3 -> eqNat_x(x3) 40: eqNat() x6 -> eqNat_x(x6) 41: main_2(x0, x2) x4 -> main_4(x0, x2, x4, eqNat()) ite() 42: cond_leqNat_x_y_1(S(x5), x4) -> leqNat() x5 x4 43: cond_leqNat_x_y_1(0(), x4) -> False() 44: cond_leqNat_x_y(0(), x2) -> True() 45: cond_leqNat_x_y(S(x4), x2) -> cond_leqNat_x_y_1(x2, x4) 46: leqNat_x(x2) x3 -> cond_leqNat_x_y(x3, x2) 47: leqNat_1() x2 -> leqNat_x(x2) 48: leqNat() x4 -> leqNat_x(x4) 49: main(x0, x2) -> main_3(x0, x2, leqNat()) eqNat() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool anyEq_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat_1 :: nat -> nat -> bool leqNat_1 :: nat -> nat -> bool lookup_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main_2 :: nat -> tree -> (nat -> nat -> bool) -> bool main_3 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> bool main_4 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> bool main_5 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (bool -> bool -> bool -> bool) -> bool main_6 :: nat -> tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> bool main_7 :: nat -> tree -> (nat -> tree -> bool) -> bool bot[0] :: bool bot[1] :: bool cond_ite_b_th_el :: bool -> bool -> bool -> bool cond_ite2_b_th_el :: bool -> bool -> bool -> bool cond_lookup_n_node :: tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y :: nat -> nat -> bool cond_leqNat_x_y :: nat -> nat -> bool cond_anyEq_nr_ys :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> bool cond_lookup_n_node_1 :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree treelist -> bool cond_eqNat_x_y_1 :: nat -> bool cond_leqNat_x_y_1 :: nat -> nat -> bool cond_lookup_n_node_2 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y_2 :: nat -> nat -> bool cond_lookup_n_node_3 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> nat -> nat list -> bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_7(x0, x1) x7 -> x7 x0 x1 2: cond_lookup_n_node_2(ConsTree(x11, x12), x2, x5, x6, x7) -> lookup(x2, x5, x6) x7 x11 3: cond_lookup_n_node_2(NilTree(), x2, x5, x6, x7) -> bot[0]() 4: cond_lookup_n_node_3(ConsTree(x13, x14), x2, x5, x6, x7, x11, x12) -> x5 (x2 x7 x11) (lookup(x2, x5, x6) x7 x13) (lookup(x2, x5, x6) x7 Node(x12, x14)) 5: cond_lookup_n_node_3(NilTree(), x2, x5, x6, x7, x11, x12) -> bot[1]() 6: cond_lookup_n_node_1(Nil(), x2, x5, x6, x7, x10) -> cond_lookup_n_node_2(x10, x2, x5, x6, x7) 7: cond_lookup_n_node_1(Cons(x11, x12), x2, x5, x6, x7, x10) -> cond_lookup_n_node_3(x10, x2 , x5 , x6 , x7 , x11 , x12) 8: cond_lookup_n_node(Leaf(x9), x2, x5, x6, x7) -> x6 x7 x9 9: cond_lookup_n_node(Node(x9, x10), x2, x5, x6, x7) -> cond_lookup_n_node_1(x9, x2, x5, x6, x7, x10) 10: lookup_n(x2, x5, x6, x7) x8 -> cond_lookup_n_node(x8, x2, x5, x6, x7) 11: lookup_1(x2, x5, x6) x7 -> lookup_n(x2, x5, x6, x7) 12: lookup(x4, x10, x12) x14 -> lookup_n(x4, x10, x12, x14) 13: main_6(x0, x2, x5, x11) x13 -> lookup(x5, x11, x13) x0 x2 14: cond_anyEq_nr_ys(Nil(), x3, x4, x6) -> False() 15: cond_anyEq_nr_ys(Cons(x8, x9), x3, x4, x6) -> x4 (x3 x6 x8) True() (anyEq(x3, x4) x6 x9) 16: anyEq_nr(x3, x4, x6) x7 -> cond_anyEq_nr_ys(x7, x3, x4, x6) 17: anyEq_1(x3, x4) x6 -> anyEq_nr(x3, x4, x6) 18: anyEq(x6, x8) x12 -> anyEq_nr(x6, x8, x12) 19: main_5(x0, x2, x9, x15, x19) x21 -> lookup(x9, x21, anyEq(x15, x19)) x0 x2 20: cond_ite2_b_th_el(True(), x6, x7) -> x6 21: cond_ite2_b_th_el(False(), x6, x7) -> x7 22: ite2_b_th(x5, x6) x7 -> cond_ite2_b_th_el(x5, x6, x7) 23: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 24: ite2() x5 -> ite2_b(x5) 25: main_4(x0, x4, x10, x13) x17 -> lookup(x10, ite2(), anyEq(x13, x17)) x0 x4 26: cond_ite_b_th_el(True(), x5, x6) -> x5 27: cond_ite_b_th_el(False(), x5, x6) -> x6 28: ite_b_th(x4, x5) x6 -> cond_ite_b_th_el(x4, x5, x6) 29: ite_b(x4) x5 -> ite_b_th(x4, x5) 30: ite() x4 -> ite_b(x4) 31: main_3(x0, x4, x8) x14 -> main_7(x0, x4) lookup(x8, ite2(), anyEq(x14, ite())) 32: cond_eqNat_x_y_1(0()) -> True() 33: cond_eqNat_x_y_1(S(x5)) -> False() 34: cond_eqNat_x_y_2(S(x6), x5) -> eqNat() x6 x5 35: cond_eqNat_x_y_2(0(), x5) -> False() 36: cond_eqNat_x_y(0(), x3) -> cond_eqNat_x_y_1(x3) 37: cond_eqNat_x_y(S(x5), x3) -> cond_eqNat_x_y_2(x3, x5) 38: eqNat_x(x3) x4 -> cond_eqNat_x_y(x4, x3) 39: eqNat_1() x3 -> eqNat_x(x3) 40: eqNat() x6 -> eqNat_x(x6) 41: main_2(x0, x4) x8 -> main_6(x0, x4, x8, ite2()) anyEq(eqNat(), ite()) 42: cond_leqNat_x_y_1(S(x5), x4) -> leqNat() x5 x4 43: cond_leqNat_x_y_1(0(), x4) -> False() 44: cond_leqNat_x_y(0(), x2) -> True() 45: cond_leqNat_x_y(S(x4), x2) -> cond_leqNat_x_y_1(x2, x4) 46: leqNat_x(x2) x3 -> cond_leqNat_x_y(x3, x2) 47: leqNat_1() x2 -> leqNat_x(x2) 48: leqNat() x4 -> leqNat_x(x4) 49: main(x0, x4) -> main_5(x0, x4, leqNat(), eqNat(), ite()) ite2() where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool anyEq_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat_1 :: nat -> nat -> bool leqNat_1 :: nat -> nat -> bool lookup_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main_2 :: nat -> tree -> (nat -> nat -> bool) -> bool main_3 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> bool main_4 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> bool main_5 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (bool -> bool -> bool -> bool) -> bool main_6 :: nat -> tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> bool main_7 :: nat -> tree -> (nat -> tree -> bool) -> bool bot[0] :: bool bot[1] :: bool cond_ite_b_th_el :: bool -> bool -> bool -> bool cond_ite2_b_th_el :: bool -> bool -> bool -> bool cond_lookup_n_node :: tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y :: nat -> nat -> bool cond_leqNat_x_y :: nat -> nat -> bool cond_anyEq_nr_ys :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> bool cond_lookup_n_node_1 :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree treelist -> bool cond_eqNat_x_y_1 :: nat -> bool cond_leqNat_x_y_1 :: nat -> nat -> bool cond_lookup_n_node_2 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y_2 :: nat -> nat -> bool cond_lookup_n_node_3 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> nat -> nat list -> bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_7(x0, x1) x7 -> x7 x0 x1 2: cond_lookup_n_node_2(ConsTree(x11, x12), x2, x5, x6, x7) -> lookup(x2, x5, x6) x7 x11 3: cond_lookup_n_node_2(NilTree(), x2, x5, x6, x7) -> bot[0]() 4: cond_lookup_n_node_3(ConsTree(x13, x14), x2, x5, x6, x7, x11, x12) -> x5 (x2 x7 x11) (lookup(x2, x5, x6) x7 x13) (lookup(x2, x5, x6) x7 Node(x12, x14)) 5: cond_lookup_n_node_3(NilTree(), x2, x5, x6, x7, x11, x12) -> bot[1]() 6: cond_lookup_n_node_1(Nil(), x2, x5, x6, x7, x10) -> cond_lookup_n_node_2(x10, x2, x5, x6, x7) 7: cond_lookup_n_node_1(Cons(x11, x12), x2, x5, x6, x7, x10) -> cond_lookup_n_node_3(x10, x2 , x5 , x6 , x7 , x11 , x12) 8: cond_lookup_n_node(Leaf(x9), x2, x5, x6, x7) -> x6 x7 x9 9: cond_lookup_n_node(Node(x9, x10), x2, x5, x6, x7) -> cond_lookup_n_node_1(x9, x2, x5, x6, x7, x10) 10: lookup_n(x2, x5, x6, x7) x8 -> cond_lookup_n_node(x8, x2, x5, x6, x7) 11: lookup_1(x2, x5, x6) x7 -> lookup_n(x2, x5, x6, x7) 12: lookup(x4, x10, x12) x14 -> lookup_n(x4, x10, x12, x14) 13: main_6(x0, x2, x5, x11) x13 -> lookup(x5, x11, x13) x0 x2 14: cond_anyEq_nr_ys(Nil(), x3, x4, x6) -> False() 15: cond_anyEq_nr_ys(Cons(x8, x9), x3, x4, x6) -> x4 (x3 x6 x8) True() (anyEq(x3, x4) x6 x9) 16: anyEq_nr(x3, x4, x6) x7 -> cond_anyEq_nr_ys(x7, x3, x4, x6) 17: anyEq_1(x3, x4) x6 -> anyEq_nr(x3, x4, x6) 18: anyEq(x6, x8) x12 -> anyEq_nr(x6, x8, x12) 19: main_5(x0, x2, x9, x15, x19) x21 -> lookup(x9, x21, anyEq(x15, x19)) x0 x2 20: cond_ite2_b_th_el(True(), x6, x7) -> x6 21: cond_ite2_b_th_el(False(), x6, x7) -> x7 22: ite2_b_th(x5, x6) x7 -> cond_ite2_b_th_el(x5, x6, x7) 23: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 24: ite2() x5 -> ite2_b(x5) 25: main_4(x0, x4, x10, x13) x17 -> lookup(x10, ite2(), anyEq(x13, x17)) x0 x4 26: cond_ite_b_th_el(True(), x5, x6) -> x5 27: cond_ite_b_th_el(False(), x5, x6) -> x6 28: ite_b_th(x4, x5) x6 -> cond_ite_b_th_el(x4, x5, x6) 29: ite_b(x4) x5 -> ite_b_th(x4, x5) 30: ite() x4 -> ite_b(x4) 31: main_3(x0, x2, x17) x29 -> lookup(x17, ite2(), anyEq(x29, ite())) x0 x2 32: cond_eqNat_x_y_1(0()) -> True() 33: cond_eqNat_x_y_1(S(x5)) -> False() 34: cond_eqNat_x_y_2(S(x6), x5) -> eqNat() x6 x5 35: cond_eqNat_x_y_2(0(), x5) -> False() 36: cond_eqNat_x_y(0(), x3) -> cond_eqNat_x_y_1(x3) 37: cond_eqNat_x_y(S(x5), x3) -> cond_eqNat_x_y_2(x3, x5) 38: eqNat_x(x3) x4 -> cond_eqNat_x_y(x4, x3) 39: eqNat_1() x3 -> eqNat_x(x3) 40: eqNat() x6 -> eqNat_x(x6) 41: main_2(x0, x4) x10 -> lookup(x10, ite2(), anyEq(eqNat(), ite())) x0 x4 42: cond_leqNat_x_y_1(S(x5), x4) -> leqNat() x5 x4 43: cond_leqNat_x_y_1(0(), x4) -> False() 44: cond_leqNat_x_y(0(), x2) -> True() 45: cond_leqNat_x_y(S(x4), x2) -> cond_leqNat_x_y_1(x2, x4) 46: leqNat_x(x2) x3 -> cond_leqNat_x_y(x3, x2) 47: leqNat_1() x2 -> leqNat_x(x2) 48: leqNat() x4 -> leqNat_x(x4) 49: main(x0, x4) -> lookup(leqNat(), ite2(), anyEq(eqNat(), ite())) x0 x4 where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool anyEq_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat_1 :: nat -> nat -> bool leqNat_1 :: nat -> nat -> bool lookup_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main_2 :: nat -> tree -> (nat -> nat -> bool) -> bool main_3 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> bool main_4 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> bool main_5 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (bool -> bool -> bool -> bool) -> bool main_6 :: nat -> tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> bool main_7 :: nat -> tree -> (nat -> tree -> bool) -> bool bot[0] :: bool bot[1] :: bool cond_ite_b_th_el :: bool -> bool -> bool -> bool cond_ite2_b_th_el :: bool -> bool -> bool -> bool cond_lookup_n_node :: tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y :: nat -> nat -> bool cond_leqNat_x_y :: nat -> nat -> bool cond_anyEq_nr_ys :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> bool cond_lookup_n_node_1 :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree treelist -> bool cond_eqNat_x_y_1 :: nat -> bool cond_leqNat_x_y_1 :: nat -> nat -> bool cond_lookup_n_node_2 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y_2 :: nat -> nat -> bool cond_lookup_n_node_3 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> nat -> nat list -> bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 7: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_7(x0, x1) x7 -> x7 x0 x1 2: cond_lookup_n_node_2(ConsTree(x11, x12), x2, x5, x6, x7) -> lookup(x2, x5, x6) x7 x11 3: cond_lookup_n_node_2(NilTree(), x2, x5, x6, x7) -> bot[0]() 4: cond_lookup_n_node_3(ConsTree(x13, x14), x2, x5, x6, x7, x11, x12) -> x5 (x2 x7 x11) (lookup(x2, x5, x6) x7 x13) (lookup(x2, x5, x6) x7 Node(x12, x14)) 5: cond_lookup_n_node_3(NilTree(), x2, x5, x6, x7, x11, x12) -> bot[1]() 6: cond_lookup_n_node_1(Nil(), x4, x10, x12, x14, ConsTree(x22, x24)) -> lookup(x4, x10, x12) x14 x22 7: cond_lookup_n_node_1(Nil(), x4, x10, x12, x14, NilTree()) -> bot[0]() 8: cond_lookup_n_node_1(Cons(x22, x24), x4, x10, x12, x14, ConsTree(x26, x28)) -> x10 (x4 x14 x22) (lookup(x4, x10, x12) x14 x26) (lookup(x4, x10, x12) x14 Node(x24, x28)) 9: cond_lookup_n_node_1(Cons(x22, x24), x4, x10, x12, x14, NilTree()) -> bot[1]() 10: cond_lookup_n_node(Leaf(x9), x2, x5, x6, x7) -> x6 x7 x9 11: cond_lookup_n_node(Node(Nil(), x20), x4, x10, x12, x14) -> cond_lookup_n_node_2(x20, x4, x10, x12, x14) 12: cond_lookup_n_node(Node(Cons(x22, x24), x20), x4, x10, x12, x14) -> cond_lookup_n_node_3(x20, x4 , x10 , x12 , x14 , x22 , x24) 13: lookup_n(x4, x10, x12, x14) Leaf(x18) -> x12 x14 x18 14: lookup_n(x4, x10, x12, x14) Node(x18, x20) -> cond_lookup_n_node_1(x18, x4, x10, x12, x14, x20) 15: lookup_1(x2, x5, x6) x7 -> lookup_n(x2, x5, x6, x7) 16: lookup(x4, x10, x12) x14 -> lookup_n(x4, x10, x12, x14) 17: main_6(x0, x2, x5, x11) x13 -> lookup(x5, x11, x13) x0 x2 18: cond_anyEq_nr_ys(Nil(), x3, x4, x6) -> False() 19: cond_anyEq_nr_ys(Cons(x8, x9), x3, x4, x6) -> x4 (x3 x6 x8) True() (anyEq(x3, x4) x6 x9) 20: anyEq_nr(x6, x8, x12) Nil() -> False() 21: anyEq_nr(x6, x8, x12) Cons(x16, x18) -> x8 (x6 x12 x16) True() (anyEq(x6, x8) x12 x18) 22: anyEq_1(x3, x4) x6 -> anyEq_nr(x3, x4, x6) 23: anyEq(x6, x8) x12 -> anyEq_nr(x6, x8, x12) 24: main_5(x0, x2, x9, x15, x19) x21 -> lookup(x9, x21, anyEq(x15, x19)) x0 x2 25: cond_ite2_b_th_el(True(), x6, x7) -> x6 26: cond_ite2_b_th_el(False(), x6, x7) -> x7 27: ite2_b_th(True(), x12) x14 -> x12 28: ite2_b_th(False(), x12) x14 -> x14 29: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 30: ite2() x5 -> ite2_b(x5) 31: main_4(x0, x4, x10, x13) x17 -> lookup(x10, ite2(), anyEq(x13, x17)) x0 x4 32: cond_ite_b_th_el(True(), x5, x6) -> x5 33: cond_ite_b_th_el(False(), x5, x6) -> x6 34: ite_b_th(True(), x10) x12 -> x10 35: ite_b_th(False(), x10) x12 -> x12 36: ite_b(x4) x5 -> ite_b_th(x4, x5) 37: ite() x4 -> ite_b(x4) 38: main_3(x0, x2, x17) x29 -> lookup(x17, ite2(), anyEq(x29, ite())) x0 x2 39: cond_eqNat_x_y_1(0()) -> True() 40: cond_eqNat_x_y_1(S(x5)) -> False() 41: cond_eqNat_x_y_2(S(x6), x5) -> eqNat() x6 x5 42: cond_eqNat_x_y_2(0(), x5) -> False() 43: cond_eqNat_x_y(0(), 0()) -> True() 44: cond_eqNat_x_y(0(), S(x10)) -> False() 45: cond_eqNat_x_y(S(x10), S(x12)) -> eqNat() x12 x10 46: cond_eqNat_x_y(S(x10), 0()) -> False() 47: eqNat_x(x6) 0() -> cond_eqNat_x_y_1(x6) 48: eqNat_x(x6) S(x10) -> cond_eqNat_x_y_2(x6, x10) 49: eqNat_1() x3 -> eqNat_x(x3) 50: eqNat() x6 -> eqNat_x(x6) 51: main_2(x0, x4) x10 -> lookup(x10, ite2(), anyEq(eqNat(), ite())) x0 x4 52: cond_leqNat_x_y_1(S(x5), x4) -> leqNat() x5 x4 53: cond_leqNat_x_y_1(0(), x4) -> False() 54: cond_leqNat_x_y(0(), x2) -> True() 55: cond_leqNat_x_y(S(x8), S(x10)) -> leqNat() x10 x8 56: cond_leqNat_x_y(S(x8), 0()) -> False() 57: leqNat_x(x4) 0() -> True() 58: leqNat_x(x4) S(x8) -> cond_leqNat_x_y_1(x4, x8) 59: leqNat_1() x2 -> leqNat_x(x2) 60: leqNat() x4 -> leqNat_x(x4) 61: main(x0, x4) -> lookup(leqNat(), ite2(), anyEq(eqNat(), ite())) x0 x4 where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool anyEq_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat_1 :: nat -> nat -> bool leqNat_1 :: nat -> nat -> bool lookup_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main_2 :: nat -> tree -> (nat -> nat -> bool) -> bool main_3 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> bool main_4 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> bool main_5 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (bool -> bool -> bool -> bool) -> bool main_6 :: nat -> tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> bool main_7 :: nat -> tree -> (nat -> tree -> bool) -> bool bot[0] :: bool bot[1] :: bool cond_ite_b_th_el :: bool -> bool -> bool -> bool cond_ite2_b_th_el :: bool -> bool -> bool -> bool cond_lookup_n_node :: tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y :: nat -> nat -> bool cond_leqNat_x_y :: nat -> nat -> bool cond_anyEq_nr_ys :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> bool cond_lookup_n_node_1 :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree treelist -> bool cond_eqNat_x_y_1 :: nat -> bool cond_leqNat_x_y_1 :: nat -> nat -> bool cond_lookup_n_node_2 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y_2 :: nat -> nat -> bool cond_lookup_n_node_3 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> nat -> nat list -> bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_7(x0, x1) x7 -> x7 x0 x1 2: cond_lookup_n_node_2(ConsTree(x11, x12), x2, x5, x6, x7) -> lookup(x2, x5, x6) x7 x11 3: cond_lookup_n_node_2(NilTree(), x2, x5, x6, x7) -> bot[0]() 4: cond_lookup_n_node_3(ConsTree(x13, x14), x2, x5, x6, x7, x11, x12) -> x5 (x2 x7 x11) (lookup(x2, x5, x6) x7 x13) (lookup(x2, x5, x6) x7 Node(x12, x14)) 5: cond_lookup_n_node_3(NilTree(), x2, x5, x6, x7, x11, x12) -> bot[1]() 6: cond_lookup_n_node_1(Nil(), x4, x10, x12, x14, ConsTree(x22, x24)) -> lookup(x4, x10, x12) x14 x22 7: cond_lookup_n_node_1(Nil(), x4, x10, x12, x14, NilTree()) -> bot[0]() 8: cond_lookup_n_node_1(Cons(x22, x24), x4, x10, x12, x14, ConsTree(x26, x28)) -> x10 (x4 x14 x22) (lookup(x4, x10, x12) x14 x26) (lookup(x4, x10, x12) x14 Node(x24, x28)) 9: cond_lookup_n_node_1(Cons(x22, x24), x4, x10, x12, x14, NilTree()) -> bot[1]() 10: cond_lookup_n_node(Leaf(x9), x2, x5, x6, x7) -> x6 x7 x9 11: cond_lookup_n_node(Node(Nil(), ConsTree(x22, x24)), x4, x10, x12, x14) -> lookup(x4, x10, x12) x14 x22 12: cond_lookup_n_node(Node(Nil(), NilTree()), x4, x10, x12, x14) -> bot[0]() 13: cond_lookup_n_node(Node(Cons(x22, x24), ConsTree(x26, x28)), x4, x10, x12, x14) -> x10 (x4 x14 x22) (lookup(x4, x10, x12) x14 x26) (lookup(x4, x10, x12) x14 Node(x24, x28)) 14: cond_lookup_n_node(Node(Cons(x22, x24), NilTree()), x4, x10, x12, x14) -> bot[1]() 15: lookup_n(x4, x10, x12, x14) Leaf(x18) -> x12 x14 x18 16: lookup_n(x8, x20, x24, x28) Node(Nil(), ConsTree(x44, x48)) -> lookup(x8, x20, x24) x28 x44 17: lookup_n(x8, x20, x24, x28) Node(Nil(), NilTree()) -> bot[0]() 18: lookup_n(x8, x20, x24, x28) Node(Cons(x44, x48), ConsTree(x52, x56)) -> x20 (x8 x28 x44) (lookup(x8, x20 , x24) x28 x52) (lookup(x8, x20, x24) x28 Node(x48, x56)) 19: lookup_n(x8, x20, x24, x28) Node(Cons(x44, x48), NilTree()) -> bot[1]() 20: lookup_1(x2, x5, x6) x7 -> lookup_n(x2, x5, x6, x7) 21: lookup(x4, x10, x12) x14 -> lookup_n(x4, x10, x12, x14) 22: main_6(x0, x2, x5, x11) x13 -> lookup(x5, x11, x13) x0 x2 23: cond_anyEq_nr_ys(Nil(), x3, x4, x6) -> False() 24: cond_anyEq_nr_ys(Cons(x8, x9), x3, x4, x6) -> x4 (x3 x6 x8) True() (anyEq(x3, x4) x6 x9) 25: anyEq_nr(x6, x8, x12) Nil() -> False() 26: anyEq_nr(x6, x8, x12) Cons(x16, x18) -> x8 (x6 x12 x16) True() (anyEq(x6, x8) x12 x18) 27: anyEq_1(x3, x4) x6 -> anyEq_nr(x3, x4, x6) 28: anyEq(x6, x8) x12 -> anyEq_nr(x6, x8, x12) 29: main_5(x0, x2, x9, x15, x19) x21 -> lookup(x9, x21, anyEq(x15, x19)) x0 x2 30: cond_ite2_b_th_el(True(), x6, x7) -> x6 31: cond_ite2_b_th_el(False(), x6, x7) -> x7 32: ite2_b_th(True(), x12) x14 -> x12 33: ite2_b_th(False(), x12) x14 -> x14 34: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 35: ite2() x5 -> ite2_b(x5) 36: main_4(x0, x4, x10, x13) x17 -> lookup(x10, ite2(), anyEq(x13, x17)) x0 x4 37: cond_ite_b_th_el(True(), x5, x6) -> x5 38: cond_ite_b_th_el(False(), x5, x6) -> x6 39: ite_b_th(True(), x10) x12 -> x10 40: ite_b_th(False(), x10) x12 -> x12 41: ite_b(x4) x5 -> ite_b_th(x4, x5) 42: ite() x4 -> ite_b(x4) 43: main_3(x0, x2, x17) x29 -> lookup(x17, ite2(), anyEq(x29, ite())) x0 x2 44: cond_eqNat_x_y_1(0()) -> True() 45: cond_eqNat_x_y_1(S(x5)) -> False() 46: cond_eqNat_x_y_2(S(x6), x5) -> eqNat() x6 x5 47: cond_eqNat_x_y_2(0(), x5) -> False() 48: cond_eqNat_x_y(0(), 0()) -> True() 49: cond_eqNat_x_y(0(), S(x10)) -> False() 50: cond_eqNat_x_y(S(x10), S(x12)) -> eqNat() x12 x10 51: cond_eqNat_x_y(S(x10), 0()) -> False() 52: eqNat_x(0()) 0() -> True() 53: eqNat_x(S(x10)) 0() -> False() 54: eqNat_x(S(x12)) S(x10) -> eqNat() x12 x10 55: eqNat_x(0()) S(x10) -> False() 56: eqNat_1() x3 -> eqNat_x(x3) 57: eqNat() x6 -> eqNat_x(x6) 58: main_2(x0, x4) x10 -> lookup(x10, ite2(), anyEq(eqNat(), ite())) x0 x4 59: cond_leqNat_x_y_1(S(x5), x4) -> leqNat() x5 x4 60: cond_leqNat_x_y_1(0(), x4) -> False() 61: cond_leqNat_x_y(0(), x2) -> True() 62: cond_leqNat_x_y(S(x8), S(x10)) -> leqNat() x10 x8 63: cond_leqNat_x_y(S(x8), 0()) -> False() 64: leqNat_x(x4) 0() -> True() 65: leqNat_x(S(x10)) S(x8) -> leqNat() x10 x8 66: leqNat_x(0()) S(x8) -> False() 67: leqNat_1() x2 -> leqNat_x(x2) 68: leqNat() x4 -> leqNat_x(x4) 69: main(x0, x4) -> lookup(leqNat(), ite2(), anyEq(eqNat(), ite())) x0 x4 where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool anyEq_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat_1 :: nat -> nat -> bool leqNat_1 :: nat -> nat -> bool lookup_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main_2 :: nat -> tree -> (nat -> nat -> bool) -> bool main_3 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> bool main_4 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> bool main_5 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (bool -> bool -> bool -> bool) -> bool main_6 :: nat -> tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> bool main_7 :: nat -> tree -> (nat -> tree -> bool) -> bool bot[0] :: bool bot[1] :: bool cond_ite_b_th_el :: bool -> bool -> bool -> bool cond_ite2_b_th_el :: bool -> bool -> bool -> bool cond_lookup_n_node :: tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y :: nat -> nat -> bool cond_leqNat_x_y :: nat -> nat -> bool cond_anyEq_nr_ys :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> bool cond_lookup_n_node_1 :: nat list -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree treelist -> bool cond_eqNat_x_y_1 :: nat -> bool cond_leqNat_x_y_1 :: nat -> nat -> bool cond_lookup_n_node_2 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> bool cond_eqNat_x_y_2 :: nat -> nat -> bool cond_lookup_n_node_3 :: tree treelist -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> nat -> nat list -> bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 9: NeededRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_7(x0, x1) x7 -> x7 x0 x1 15: lookup_n(x4, x10, x12, x14) Leaf(x18) -> x12 x14 x18 16: lookup_n(x8, x20, x24, x28) Node(Nil(), ConsTree(x44, x48)) -> lookup(x8, x20, x24) x28 x44 17: lookup_n(x8, x20, x24, x28) Node(Nil(), NilTree()) -> bot[0]() 18: lookup_n(x8, x20, x24, x28) Node(Cons(x44, x48), ConsTree(x52, x56)) -> x20 (x8 x28 x44) (lookup(x8, x20 , x24) x28 x52) (lookup(x8, x20, x24) x28 Node(x48, x56)) 19: lookup_n(x8, x20, x24, x28) Node(Cons(x44, x48), NilTree()) -> bot[1]() 20: lookup_1(x2, x5, x6) x7 -> lookup_n(x2, x5, x6, x7) 21: lookup(x4, x10, x12) x14 -> lookup_n(x4, x10, x12, x14) 22: main_6(x0, x2, x5, x11) x13 -> lookup(x5, x11, x13) x0 x2 25: anyEq_nr(x6, x8, x12) Nil() -> False() 26: anyEq_nr(x6, x8, x12) Cons(x16, x18) -> x8 (x6 x12 x16) True() (anyEq(x6, x8) x12 x18) 27: anyEq_1(x3, x4) x6 -> anyEq_nr(x3, x4, x6) 28: anyEq(x6, x8) x12 -> anyEq_nr(x6, x8, x12) 29: main_5(x0, x2, x9, x15, x19) x21 -> lookup(x9, x21, anyEq(x15, x19)) x0 x2 32: ite2_b_th(True(), x12) x14 -> x12 33: ite2_b_th(False(), x12) x14 -> x14 34: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 35: ite2() x5 -> ite2_b(x5) 36: main_4(x0, x4, x10, x13) x17 -> lookup(x10, ite2(), anyEq(x13, x17)) x0 x4 39: ite_b_th(True(), x10) x12 -> x10 40: ite_b_th(False(), x10) x12 -> x12 41: ite_b(x4) x5 -> ite_b_th(x4, x5) 42: ite() x4 -> ite_b(x4) 43: main_3(x0, x2, x17) x29 -> lookup(x17, ite2(), anyEq(x29, ite())) x0 x2 52: eqNat_x(0()) 0() -> True() 53: eqNat_x(S(x10)) 0() -> False() 54: eqNat_x(S(x12)) S(x10) -> eqNat() x12 x10 55: eqNat_x(0()) S(x10) -> False() 56: eqNat_1() x3 -> eqNat_x(x3) 57: eqNat() x6 -> eqNat_x(x6) 58: main_2(x0, x4) x10 -> lookup(x10, ite2(), anyEq(eqNat(), ite())) x0 x4 64: leqNat_x(x4) 0() -> True() 65: leqNat_x(S(x10)) S(x8) -> leqNat() x10 x8 66: leqNat_x(0()) S(x8) -> False() 67: leqNat_1() x2 -> leqNat_x(x2) 68: leqNat() x4 -> leqNat_x(x4) 69: main(x0, x4) -> lookup(leqNat(), ite2(), anyEq(eqNat(), ite())) x0 x4 where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool anyEq_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat_1 :: nat -> nat -> bool leqNat_1 :: nat -> nat -> bool lookup_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main_2 :: nat -> tree -> (nat -> nat -> bool) -> bool main_3 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> bool main_4 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> bool main_5 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (bool -> bool -> bool -> bool) -> bool main_6 :: nat -> tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> bool main_7 :: nat -> tree -> (nat -> tree -> bool) -> bool bot[0] :: bool bot[1] :: bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: NeededRules + Details: none * Step 10: CFA WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_7(x0, x1) x7 -> x7 x0 x1 2: lookup_n(x4, x10, x12, x14) Leaf(x18) -> x12 x14 x18 3: lookup_n(x8, x20, x24, x28) Node(Nil(), ConsTree(x44, x48)) -> lookup(x8, x20, x24) x28 x44 4: lookup_n(x8, x20, x24, x28) Node(Nil(), NilTree()) -> bot[0]() 5: lookup_n(x8, x20, x24, x28) Node(Cons(x44, x48), ConsTree(x52, x56)) -> x20 (x8 x28 x44) (lookup(x8, x20 , x24) x28 x52) (lookup(x8, x20, x24) x28 Node(x48, x56)) 6: lookup_n(x8, x20, x24, x28) Node(Cons(x44, x48), NilTree()) -> bot[1]() 7: lookup_1(x2, x5, x6) x7 -> lookup_n(x2, x5, x6, x7) 8: lookup(x4, x10, x12) x14 -> lookup_n(x4, x10, x12, x14) 9: main_6(x0, x2, x5, x11) x13 -> lookup(x5, x11, x13) x0 x2 10: anyEq_nr(x6, x8, x12) Nil() -> False() 11: anyEq_nr(x6, x8, x12) Cons(x16, x18) -> x8 (x6 x12 x16) True() (anyEq(x6, x8) x12 x18) 12: anyEq_1(x3, x4) x6 -> anyEq_nr(x3, x4, x6) 13: anyEq(x6, x8) x12 -> anyEq_nr(x6, x8, x12) 14: main_5(x0, x2, x9, x15, x19) x21 -> lookup(x9, x21, anyEq(x15, x19)) x0 x2 15: ite2_b_th(True(), x12) x14 -> x12 16: ite2_b_th(False(), x12) x14 -> x14 17: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 18: ite2() x5 -> ite2_b(x5) 19: main_4(x0, x4, x10, x13) x17 -> lookup(x10, ite2(), anyEq(x13, x17)) x0 x4 20: ite_b_th(True(), x10) x12 -> x10 21: ite_b_th(False(), x10) x12 -> x12 22: ite_b(x4) x5 -> ite_b_th(x4, x5) 23: ite() x4 -> ite_b(x4) 24: main_3(x0, x2, x17) x29 -> lookup(x17, ite2(), anyEq(x29, ite())) x0 x2 25: eqNat_x(0()) 0() -> True() 26: eqNat_x(S(x10)) 0() -> False() 27: eqNat_x(S(x12)) S(x10) -> eqNat() x12 x10 28: eqNat_x(0()) S(x10) -> False() 29: eqNat_1() x3 -> eqNat_x(x3) 30: eqNat() x6 -> eqNat_x(x6) 31: main_2(x0, x4) x10 -> lookup(x10, ite2(), anyEq(eqNat(), ite())) x0 x4 32: leqNat_x(x4) 0() -> True() 33: leqNat_x(S(x10)) S(x8) -> leqNat() x10 x8 34: leqNat_x(0()) S(x8) -> False() 35: leqNat_1() x2 -> leqNat_x(x2) 36: leqNat() x4 -> leqNat_x(x4) 37: main(x0, x4) -> lookup(leqNat(), ite2(), anyEq(eqNat(), ite())) x0 x4 where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool anyEq_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat_1 :: nat -> nat -> bool leqNat_1 :: nat -> nat -> bool lookup_1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main_2 :: nat -> tree -> (nat -> nat -> bool) -> bool main_3 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> bool main_4 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> bool main_5 :: nat -> tree -> (nat -> nat -> bool) -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (bool -> bool -> bool -> bool) -> bool main_6 :: nat -> tree -> (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> bool main_7 :: nat -> tree -> (nat -> tree -> bool) -> bool bot[0] :: bool bot[1] :: bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> False() | S(X{*}) | 0() | S(X{*}) | S(X{*}) | True() | 0() | False() | S(X{*}) | 0() | S(X{*}) | S(X{*}) | False() | 0() | S(X{*}) | True() | 0() | 0() | False() | True() | False() | True() | True() | Cons(X{*},X{*}) | False() | Nil() | NilTree() | Cons(X{*},X{*}) | Node(X{*},X{*}) | Node(X{*},X{*}) | ConsTree(X{*},X{*}) | Cons(X{*},X{*}) | Node(X{*},X{*}) | NilTree() | Nil() | Node(X{*},X{*}) | ConsTree(X{*},X{*}) | Nil() | Node(X{*},X{*}) | Leaf(X{*}) ,V{x0_37} -> X{*} ,V{x4_2} -> V{x4_8} ,V{x4_8} -> V{x8_5} | V{x8_3} | leqNat() ,V{x4_22} -> V{x4_23} ,V{x4_23} -> R{27} | R{25} | R{26} | R{28} ,V{x4_32} -> V{x4_36} ,V{x4_36} -> V{x10_33} | V{x28_5} ,V{x4_37} -> X{*} ,V{x5_17} -> V{x5_18} ,V{x5_18} -> R{33} | R{32} | R{34} ,V{x5_22} -> True() ,V{x6_10} -> V{x6_13} ,V{x6_11} -> V{x6_13} ,V{x6_13} -> V{x6_11} | eqNat() ,V{x6_17} -> R{5} | R{2} | R{3} | R{4} | R{6} ,V{x6_30} -> V{x12_27} | V{x12_11} ,V{x8_3} -> V{x4_8} ,V{x8_4} -> V{x4_8} ,V{x8_5} -> V{x4_8} ,V{x8_6} -> V{x4_8} ,V{x8_10} -> V{x8_13} ,V{x8_11} -> V{x8_13} ,V{x8_13} -> V{x8_11} | ite() ,V{x8_33} -> X{*} ,V{x8_34} -> X{*} ,V{x10_2} -> V{x10_8} ,V{x10_8} -> V{x20_5} | V{x20_3} | ite2() ,V{x10_20} -> V{x5_22} ,V{x10_21} -> V{x5_22} ,V{x10_26} -> X{*} ,V{x10_27} -> X{*} ,V{x10_28} -> X{*} ,V{x10_33} -> X{*} ,V{x12_2} -> V{x12_8} ,V{x12_8} -> V{x24_5} | V{x24_3} | anyEq(eqNat(),ite()) ,V{x12_10} -> V{x12_13} ,V{x12_11} -> V{x12_13} ,V{x12_13} -> V{x12_11} | V{x14_2} ,V{x12_15} -> V{x6_17} ,V{x12_16} -> V{x6_17} ,V{x12_20} -> R{11} | R{10} ,V{x12_21} -> R{11} | R{10} ,V{x12_27} -> X{*} ,V{x14_2} -> V{x14_8} ,V{x14_8} -> V{x28_5} | V{x28_3} | V{x0_37} ,V{x14_15} -> R{6} | R{5} | R{4} | R{3} ,V{x14_16} -> R{6} | R{5} | R{4} | R{3} ,V{x16_11} -> X{*} ,V{x18_2} -> X{*} ,V{x18_11} -> X{*} ,V{x20_3} -> V{x10_8} ,V{x20_4} -> V{x10_8} ,V{x20_5} -> V{x10_8} ,V{x20_6} -> V{x10_8} ,V{x24_3} -> V{x12_8} ,V{x24_4} -> V{x12_8} ,V{x24_5} -> V{x12_8} ,V{x24_6} -> V{x12_8} ,V{x28_3} -> V{x14_8} ,V{x28_4} -> V{x14_8} ,V{x28_5} -> V{x14_8} ,V{x28_6} -> V{x14_8} ,V{x44_3} -> X{*} ,V{x44_5} -> X{*} ,V{x44_6} -> X{*} ,V{x48_3} -> X{*} ,V{x48_5} -> X{*} ,V{x48_6} -> X{*} ,V{x52_5} -> X{*} ,V{x56_5} -> X{*} ,R{0} -> R{37} | main(X{*},X{*}) ,R{2} -> R{11} | R{10} | @(R{13},V{x18_2}) | @(@(V{x12_2},V{x14_2}),V{x18_2}) ,R{3} -> R{6} | R{5} | R{4} | R{3} | R{2} | @(R{8},V{x44_3}) | @(@(lookup(V{x8_3},V{x20_3},V{x24_3}),V{x28_3}),V{x44_3}) ,R{4} -> bot[0]() ,R{5} -> R{16} | R{15} | @(R{17},R{3}) | @(R{17},R{4}) | @(R{17},R{5}) | @(R{17},R{6}) | @(@(R{18},R{2}),R{6}) | @(@(R{18},R{2}),R{5}) | @(@(R{18},R{2}),R{4}) | @(@(R{18},R{2}),R{3}) | @(@(R{18},R{3}),R{6}) | @(@(R{18},R{3}),R{5}) | @(@(R{18},R{3}),R{4}) | @(@(R{18},R{3}),R{3}) | @(@(R{18},R{4}),R{6}) | @(@(R{18},R{4}),R{5}) | @(@(R{18},R{4}),R{4}) | @(@(R{18},R{4}),R{3}) | @(@(R{18},R{5}),R{6}) | @(@(R{18},R{5}),R{5}) | @(@(R{18},R{5}),R{4}) | @(@(R{18},R{5}),R{3}) | @(@(R{18},R{6}),R{6}) | @(@(R{18},R{6}),R{5}) | @(@(R{18},R{6}),R{4}) | @(@(R{18},R{6}),R{3}) | @(R{17},@(R{8},Node(V{x48_5},V{x56_5}))) | @(R{17},@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{6}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{5}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{4}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{3}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{2}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{6}),R{3}) | @(@(@(V{x20_5},R{34}),R{5}),R{3}) | @(@(@(V{x20_5},R{34}),R{4}),R{3}) | @(@(@(V{x20_5},R{34}),R{3}),R{3}) | @(@(@(V{x20_5},R{34}),R{2}),R{3}) | @(@(@(V{x20_5},R{34}),R{6}),R{4}) | @(@(@(V{x20_5},R{34}),R{5}),R{4}) | @(@(@(V{x20_5},R{34}),R{4}),R{4}) | @(@(@(V{x20_5},R{34}),R{3}),R{4}) | @(@(@(V{x20_5},R{34}),R{2}),R{4}) | @(@(@(V{x20_5},R{34}),R{6}),R{5}) | @(@(@(V{x20_5},R{34}),R{5}),R{5}) | @(@(@(V{x20_5},R{34}),R{4}),R{5}) | @(@(@(V{x20_5},R{34}),R{3}),R{5}) | @(@(@(V{x20_5},R{34}),R{2}),R{5}) | @(@(@(V{x20_5},R{34}),R{6}),R{6}) | @(@(@(V{x20_5},R{34}),R{5}),R{6}) | @(@(@(V{x20_5},R{34}),R{4}),R{6}) | @(@(@(V{x20_5},R{34}),R{3}),R{6}) | @(@(@(V{x20_5},R{34}),R{2}),R{6}) | @(@(@(V{x20_5},R{33}),R{6}),R{3}) | @(@(@(V{x20_5},R{33}),R{5}),R{3}) | @(@(@(V{x20_5},R{33}),R{4}),R{3}) | @(@(@(V{x20_5},R{33}),R{3}),R{3}) | @(@(@(V{x20_5},R{33}),R{2}),R{3}) | @(@(@(V{x20_5},R{33}),R{6}),R{4}) | @(@(@(V{x20_5},R{33}),R{5}),R{4}) | @(@(@(V{x20_5},R{33}),R{4}),R{4}) | @(@(@(V{x20_5},R{33}),R{3}),R{4}) | @(@(@(V{x20_5},R{33}),R{2}),R{4}) | @(@(@(V{x20_5},R{33}),R{6}),R{5}) | @(@(@(V{x20_5},R{33}),R{5}),R{5}) | @(@(@(V{x20_5},R{33}),R{4}),R{5}) | @(@(@(V{x20_5},R{33}),R{3}),R{5}) | @(@(@(V{x20_5},R{33}),R{2}),R{5}) | @(@(@(V{x20_5},R{33}),R{6}),R{6}) | @(@(@(V{x20_5},R{33}),R{5}),R{6}) | @(@(@(V{x20_5},R{33}),R{4}),R{6}) | @(@(@(V{x20_5},R{33}),R{3}),R{6}) | @(@(@(V{x20_5},R{33}),R{2}),R{6}) | @(@(@(V{x20_5},R{32}),R{6}),R{3}) | @(@(@(V{x20_5},R{32}),R{5}),R{3}) | @(@(@(V{x20_5},R{32}),R{4}),R{3}) | @(@(@(V{x20_5},R{32}),R{3}),R{3}) | @(@(@(V{x20_5},R{32}),R{2}),R{3}) | @(@(R{18},@(R{8},V{x52_5})),R{3}) | @(@(@(V{x20_5},R{32}),R{6}),R{4}) | @(@(@(V{x20_5},R{32}),R{5}),R{4}) | @(@(@(V{x20_5},R{32}),R{4}),R{4}) | @(@(@(V{x20_5},R{32}),R{3}),R{4}) | @(@(@(V{x20_5},R{32}),R{2}),R{4}) | @(@(R{18},@(R{8},V{x52_5})),R{4}) | @(@(@(V{x20_5},R{32}),R{6}),R{5}) | @(@(@(V{x20_5},R{32}),R{5}),R{5}) | @(@(@(V{x20_5},R{32}),R{4}),R{5}) | @(@(@(V{x20_5},R{32}),R{3}),R{5}) | @(@(@(V{x20_5},R{32}),R{2}),R{5}) | @(@(R{18},@(R{8},V{x52_5})),R{5}) | @(@(@(V{x20_5},R{32}),R{6}),R{6}) | @(@(@(V{x20_5},R{32}),R{5}),R{6}) | @(@(@(V{x20_5},R{32}),R{4}),R{6}) | @(@(@(V{x20_5},R{32}),R{3}),R{6}) | @(@(@(V{x20_5},R{32}),R{2}),R{6}) | @(@(R{18},@(R{8},V{x52_5})),R{6}) | @(@(@(V{x20_5},R{32}),@(R{8},V{x52_5})),R{6}) | @(@(@(V{x20_5},R{32}),@(R{8},V{x52_5})),R{5}) | @(@(@(V{x20_5},R{32}),@(R{8},V{x52_5})),R{4}) | @(@(@(V{x20_5},R{32}),@(R{8},V{x52_5})),R{3}) | @(@(@(V{x20_5},R{33}),@(R{8},V{x52_5})),R{6}) | @(@(@(V{x20_5},R{33}),@(R{8},V{x52_5})),R{5}) | @(@(@(V{x20_5},R{33}),@(R{8},V{x52_5})),R{4}) | @(@(@(V{x20_5},R{33}),@(R{8},V{x52_5})),R{3}) | @(@(@(V{x20_5},R{34}),@(R{8},V{x52_5})),R{6}) | @(@(@(V{x20_5},R{34}),@(R{8},V{x52_5})),R{5}) | @(@(@(V{x20_5},R{34}),@(R{8},V{x52_5})),R{4}) | @(@(@(V{x20_5},R{34}),@(R{8},V{x52_5})),R{3}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{2}),R{6}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{2}),R{5}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{2}),R{4}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{2}),R{3}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{3}),R{6}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{3}),R{5}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{3}),R{4}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{3}),R{3}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{4}),R{6}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{4}),R{5}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{4}),R{4}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{4}),R{3}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{5}),R{6}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{5}),R{5}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{5}),R{4}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{5}),R{3}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{6}),R{6}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{6}),R{5}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{6}),R{4}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{6}),R{3}) | @(@(@(V{x20_5},R{32}),R{2}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{2}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{2}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{3}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{3}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{3}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{4}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{4}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{4}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{5}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{5}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{5}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{6}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{6}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{6}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(R{18},@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{6}) | @(@(R{18},@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{5}) | @(@(R{18},@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{4}) | @(@(R{18},@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{3}) | @(@(R{18},@(R{8},V{x52_5})),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{6}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{5}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{4}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{3}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(R{18},R{2}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(R{18},@(R{8},V{x52_5})),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(R{18},@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{6}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{6}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{6}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{5}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{5}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{5}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{4}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{4}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{4}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{3}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{3}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{3}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),R{2}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),R{2}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),R{2}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{6}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{5}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{4}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{3}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{2}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),@(R{8},V{x52_5})),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),@(R{8},V{x52_5})),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),@(R{8},V{x52_5})),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{6}) | @(@(@(V{x20_5},R{33}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{6}) | @(@(@(V{x20_5},R{32}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{6}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{6}),R{6}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{5}),R{6}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{4}),R{6}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{3}),R{6}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{2}),R{6}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(R{8},V{x52_5})),R{6}) | @(@(@(V{x20_5},R{34}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{5}) | @(@(@(V{x20_5},R{33}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{5}) | @(@(@(V{x20_5},R{32}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{5}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{6}),R{5}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{5}),R{5}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{4}),R{5}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{3}),R{5}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{2}),R{5}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(R{8},V{x52_5})),R{5}) | @(@(@(V{x20_5},R{34}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{4}) | @(@(@(V{x20_5},R{33}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{4}) | @(@(@(V{x20_5},R{32}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{4}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{6}),R{4}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{5}),R{4}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{4}),R{4}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{3}),R{4}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{2}),R{4}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(R{8},V{x52_5})),R{4}) | @(@(@(V{x20_5},R{34}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{3}) | @(@(@(V{x20_5},R{33}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{3}) | @(@(@(V{x20_5},R{32}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{3}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{6}),R{3}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{5}),R{3}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{4}),R{3}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{3}),R{3}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{2}),R{3}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(R{8},V{x52_5})),R{3}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),@(R{8},V{x52_5})),R{3}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{3}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),@(R{8},V{x52_5})),R{4}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{4}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),@(R{8},V{x52_5})),R{5}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{5}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),@(R{8},V{x52_5})),R{6}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})),R{6}) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(R{8},V{x52_5})),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{2}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{2}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{3}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{3}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{4}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{4}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{5}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{5}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{6}),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),R{6}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),@(R{8},V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),@(R{8},V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),@(R{8},V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(R{18},@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{34}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{33}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},R{32}),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{6}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{5}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{4}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{3}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),R{2}) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(R{8},V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,R{6}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,R{5}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,R{4}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,R{3}) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),@(R{8},V{x52_5})),@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(R{8},Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})),@(R{8},V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(R{36},V{x44_5})),@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) | @(@(@(V{x20_5},@(@(V{x8_5},V{x28_5}),V{x44_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),V{x52_5})) ,@(@(lookup(V{x8_5},V{x20_5},V{x24_5}),V{x28_5}),Node(V{x48_5},V{x56_5}))) ,R{6} -> bot[1]() ,R{8} -> lookup_n(V{x4_8},V{x10_8},V{x12_8},V{x14_8}) ,R{10} -> False() ,R{11} -> R{21} | R{20} | @(R{22},R{10}) | @(R{22},R{11}) | @(@(R{23},True()),R{11}) | @(@(R{23},True()),R{10}) | @(R{22},@(R{13},V{x18_11})) | @(R{22},@(@(anyEq(V{x6_11},V{x8_11}),V{x12_11}),V{x18_11})) | @(@(R{23},True()),@(R{13},V{x18_11})) | @(@(@(V{x8_11},R{28}),True()),R{11}) | @(@(@(V{x8_11},R{27}),True()),R{11}) | @(@(@(V{x8_11},R{26}),True()),R{11}) | @(@(@(V{x8_11},R{25}),True()),R{11}) | @(@(@(V{x8_11},R{28}),True()),R{10}) | @(@(@(V{x8_11},R{27}),True()),R{10}) | @(@(@(V{x8_11},R{26}),True()),R{10}) | @(@(@(V{x8_11},R{25}),True()),R{10}) | @(@(@(V{x8_11},@(R{30},V{x16_11})),True()),R{10}) | @(@(@(V{x8_11},@(R{30},V{x16_11})),True()),R{11}) | @(@(@(V{x8_11},R{25}),True()),@(R{13},V{x18_11})) | @(@(@(V{x8_11},R{26}),True()),@(R{13},V{x18_11})) | @(@(@(V{x8_11},R{27}),True()),@(R{13},V{x18_11})) | @(@(@(V{x8_11},R{28}),True()),@(R{13},V{x18_11})) | @(@(R{23},True()),@(@(anyEq(V{x6_11},V{x8_11}),V{x12_11}),V{x18_11})) | @(@(@(V{x8_11},R{28}),True()),@(@(anyEq(V{x6_11},V{x8_11}),V{x12_11}),V{x18_11})) | @(@(@(V{x8_11},R{27}),True()),@(@(anyEq(V{x6_11},V{x8_11}),V{x12_11}),V{x18_11})) | @(@(@(V{x8_11},R{26}),True()),@(@(anyEq(V{x6_11},V{x8_11}),V{x12_11}),V{x18_11})) | @(@(@(V{x8_11},R{25}),True()),@(@(anyEq(V{x6_11},V{x8_11}),V{x12_11}),V{x18_11})) | @(@(@(V{x8_11},@(@(V{x6_11},V{x12_11}),V{x16_11})),True()),R{11}) | @(@(@(V{x8_11},@(@(V{x6_11},V{x12_11}),V{x16_11})),True()),R{10}) | @(@(@(V{x8_11},@(R{30},V{x16_11})),True()),@(R{13},V{x18_11})) | @(@(@(V{x8_11},@(@(V{x6_11},V{x12_11}),V{x16_11})),True()),@(R{13},V{x18_11})) | @(@(@(V{x8_11},@(R{30},V{x16_11})),True()),@(@(anyEq(V{x6_11},V{x8_11}),V{x12_11}),V{x18_11})) | @(@(@(V{x8_11},@(@(V{x6_11},V{x12_11}),V{x16_11})),True()) ,@(@(anyEq(V{x6_11},V{x8_11}),V{x12_11}),V{x18_11})) ,R{13} -> anyEq_nr(V{x6_13},V{x8_13},V{x12_13}) ,R{15} -> V{x12_15} ,R{16} -> V{x14_16} ,R{17} -> ite2_b_th(V{x5_17},V{x6_17}) ,R{18} -> ite2_b(V{x5_18}) ,R{20} -> V{x10_20} ,R{21} -> V{x12_21} ,R{22} -> ite_b_th(V{x4_22},V{x5_22}) ,R{23} -> ite_b(V{x4_23}) ,R{25} -> True() ,R{26} -> False() ,R{27} -> R{28} | R{27} | R{26} | R{25} | @(R{30},V{x10_27}) | @(@(eqNat(),V{x12_27}),V{x10_27}) ,R{28} -> False() ,R{30} -> eqNat_x(V{x6_30}) ,R{32} -> True() ,R{33} -> R{34} | R{33} | R{32} | @(R{36},V{x8_33}) | @(@(leqNat(),V{x10_33}),V{x8_33}) ,R{34} -> False() ,R{36} -> leqNat_x(V{x4_36}) ,R{37} -> R{6} | R{5} | R{4} | R{3} | R{2} | @(R{8},V{x4_37}) | @(@(lookup(leqNat(),ite2(),anyEq(eqNat(),ite())),V{x0_37}),V{x4_37})} * Step 11: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 2: lookup_n(leqNat(), ite2(), anyEq(eqNat(), ite()), x2) Leaf(x1) -> anyEq(eqNat(), ite()) x2 x1 3: lookup_n(leqNat(), ite2(), anyEq(eqNat(), ite()), x3) Node(Nil(), ConsTree(x2, x1)) -> lookup(leqNat() , ite2() , anyEq(eqNat() , ite())) x3 x2 4: lookup_n(leqNat(), ite2(), anyEq(eqNat(), ite()), x1) Node(Nil(), NilTree()) -> bot[0]() 5: lookup_n(leqNat(), ite2(), anyEq(eqNat(), ite()), x5) Node(Cons(x4, x3), ConsTree(x2, x1)) -> ite2() (leqNat() x5 x4) (lookup(leqNat(), ite2(), anyEq(eqNat(), ite())) x5 x2) (lookup(leqNat(), ite2() , anyEq(eqNat(), ite())) x5 Node(x3, x1)) 6: lookup_n(leqNat(), ite2(), anyEq(eqNat(), ite()), x3) Node(Cons(x2, x1), NilTree()) -> bot[1]() 8: lookup(leqNat(), ite2(), anyEq(eqNat(), ite())) x1 -> lookup_n(leqNat(), ite2() , anyEq(eqNat(), ite()) , x1) 10: anyEq_nr(eqNat(), ite(), x1) Nil() -> False() 11: anyEq_nr(eqNat(), ite(), x3) Cons(x2, x1) -> ite() (eqNat() x3 x2) True() (anyEq(eqNat(), ite()) x3 x1) 13: anyEq(eqNat(), ite()) x1 -> anyEq_nr(eqNat(), ite(), x1) 15: ite2_b_th(True(), x12) x14 -> x12 16: ite2_b_th(False(), x12) x14 -> x14 17: ite2_b(x5) x6 -> ite2_b_th(x5, x6) 18: ite2() x5 -> ite2_b(x5) 20: ite_b_th(True(), True()) x1 -> True() 21: ite_b_th(False(), True()) x1 -> x1 22: ite_b(x1) True() -> ite_b_th(x1, True()) 23: ite() x4 -> ite_b(x4) 25: eqNat_x(0()) 0() -> True() 26: eqNat_x(S(x10)) 0() -> False() 27: eqNat_x(S(x2)) S(x1) -> eqNat() x2 x1 28: eqNat_x(0()) S(x10) -> False() 30: eqNat() x6 -> eqNat_x(x6) 32: leqNat_x(x4) 0() -> True() 33: leqNat_x(S(x2)) S(x1) -> leqNat() x2 x1 34: leqNat_x(0()) S(x8) -> False() 36: leqNat() x4 -> leqNat_x(x4) 37: main(x2, x1) -> lookup(leqNat(), ite2(), anyEq(eqNat(), ite())) x2 x1 where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool ite_b :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool ite_b_th :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool eqNat_x :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool bot[0] :: bool bot[1] :: bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool eqNat :: nat -> nat -> bool leqNat :: nat -> nat -> bool lookup :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: UncurryATRS + Details: none * Step 12: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, Leaf(x1)) -> anyEq#2(eqNat(), ite(), x2, x1) 2: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, Node(Nil(), ConsTree(x2, x1))) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, x2) 3: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x1, Node(Nil(), NilTree())) -> bot[0]() 4: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, Node(Cons(x4, x3), ConsTree(x2, x1))) -> ite2#3(leqNat#2(x5, x4), lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, x2) , lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, Node(x3, x1))) 5: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, Node(Cons(x2, x1), NilTree())) -> bot[1]() 6: lookup#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x1) -> lookup_n(leqNat(), ite2() , anyEq(eqNat(), ite()) , x1) 7: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x1, x2) -> lookup_n#1(leqNat(), ite2() , anyEq(eqNat(), ite()) , x1 , x2) 8: anyEq_nr#1(eqNat(), ite(), x1, Nil()) -> False() 9: anyEq_nr#1(eqNat(), ite(), x3, Cons(x2, x1)) -> ite#3(eqNat#2(x3, x2), True() , anyEq#2(eqNat(), ite(), x3, x1)) 10: anyEq#1(eqNat(), ite(), x1) -> anyEq_nr(eqNat(), ite(), x1) 11: anyEq#2(eqNat(), ite(), x1, x2) -> anyEq_nr#1(eqNat(), ite(), x1, x2) 12: ite2_b_th#1(True(), x12, x14) -> x12 13: ite2_b_th#1(False(), x12, x14) -> x14 14: ite2_b#1(x5, x6) -> ite2_b_th(x5, x6) 15: ite2_b#2(x5, x6, x7) -> ite2_b_th#1(x5, x6, x7) 16: ite2#1(x5) -> ite2_b(x5) 17: ite2#2(x5, x6) -> ite2_b#1(x5, x6) 18: ite2#3(x5, x6, x7) -> ite2_b#2(x5, x6, x7) 19: ite_b_th#1(True(), True(), x1) -> True() 20: ite_b_th#1(False(), True(), x1) -> x1 21: ite_b#1(x1, True()) -> ite_b_th(x1, True()) 22: ite_b#2(x1, True(), x2) -> ite_b_th#1(x1, True(), x2) 23: ite#1(x4) -> ite_b(x4) 24: ite#2(x4, x5) -> ite_b#1(x4, x5) 25: ite#3(x4, x5, x6) -> ite_b#2(x4, x5, x6) 26: eqNat_x#1(0(), 0()) -> True() 27: eqNat_x#1(S(x10), 0()) -> False() 28: eqNat_x#1(S(x2), S(x1)) -> eqNat#2(x2, x1) 29: eqNat_x#1(0(), S(x10)) -> False() 30: eqNat#1(x6) -> eqNat_x(x6) 31: eqNat#2(x6, x7) -> eqNat_x#1(x6, x7) 32: leqNat_x#1(x4, 0()) -> True() 33: leqNat_x#1(S(x2), S(x1)) -> leqNat#2(x2, x1) 34: leqNat_x#1(0(), S(x8)) -> False() 35: leqNat#1(x4) -> leqNat_x(x4) 36: leqNat#2(x4, x5) -> leqNat_x#1(x4, x5) 37: main(x2, x1) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq_nr#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool bot[0] :: bool bot[1] :: 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 ite :: bool -> bool -> bool -> bool ite#1 :: bool -> bool -> bool -> bool ite#2 :: bool -> bool -> bool -> bool ite#3 :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool ite2#1 :: bool -> bool -> bool -> bool ite2#2 :: bool -> bool -> bool -> bool ite2#3 :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite2_b#1 :: bool -> bool -> bool -> bool ite2_b#2 :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool ite2_b_th#1 :: bool -> bool -> bool -> bool ite_b :: bool -> bool -> bool -> bool ite_b#1 :: bool -> bool -> bool -> bool ite_b#2 :: bool -> bool -> bool -> bool ite_b_th :: bool -> bool -> bool -> bool ite_b_th#1 :: bool -> bool -> bool -> bool leqNat :: nat -> nat -> bool leqNat#1 :: nat -> nat -> bool leqNat#2 :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool leqNat_x#1 :: nat -> nat -> bool lookup#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool lookup#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool lookup_n#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 13: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, Leaf(x1)) -> anyEq#2(eqNat(), ite(), x2, x1) 2: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, Node(Nil(), ConsTree(x2, x1))) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, x2) 3: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x1, Node(Nil(), NilTree())) -> bot[0]() 4: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, Node(Cons(x4, x3), ConsTree(x2, x1))) -> ite2#3(leqNat#2(x5, x4), lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, x2) , lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, Node(x3, x1))) 5: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, Node(Cons(x2, x1), NilTree())) -> bot[1]() 6: lookup#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x1) -> lookup_n(leqNat(), ite2() , anyEq(eqNat(), ite()) , x1) 7: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x1, x2) -> lookup_n#1(leqNat(), ite2() , anyEq(eqNat(), ite()) , x1 , x2) 8: anyEq_nr#1(eqNat(), ite(), x1, Nil()) -> False() 9: anyEq_nr#1(eqNat(), ite(), x3, Cons(x2, x1)) -> ite#3(eqNat#2(x3, x2), True() , anyEq#2(eqNat(), ite(), x3, x1)) 10: anyEq#1(eqNat(), ite(), x1) -> anyEq_nr(eqNat(), ite(), x1) 11: anyEq#2(eqNat(), ite(), x1, x2) -> anyEq_nr#1(eqNat(), ite(), x1, x2) 12: ite2_b_th#1(True(), x12, x14) -> x12 13: ite2_b_th#1(False(), x12, x14) -> x14 14: ite2_b#1(x5, x6) -> ite2_b_th(x5, x6) 15: ite2_b#2(True(), x24, x28) -> x24 16: ite2_b#2(False(), x24, x28) -> x28 17: ite2#1(x5) -> ite2_b(x5) 18: ite2#2(x5, x6) -> ite2_b#1(x5, x6) 19: ite2#3(x5, x6, x7) -> ite2_b#2(x5, x6, x7) 20: ite_b_th#1(True(), True(), x1) -> True() 21: ite_b_th#1(False(), True(), x1) -> x1 22: ite_b#1(x1, True()) -> ite_b_th(x1, True()) 23: ite_b#2(True(), True(), x2) -> True() 24: ite_b#2(False(), True(), x2) -> x2 25: ite#1(x4) -> ite_b(x4) 26: ite#2(x4, x5) -> ite_b#1(x4, x5) 27: ite#3(x4, x5, x6) -> ite_b#2(x4, x5, x6) 28: eqNat_x#1(0(), 0()) -> True() 29: eqNat_x#1(S(x10), 0()) -> False() 30: eqNat_x#1(S(x2), S(x1)) -> eqNat#2(x2, x1) 31: eqNat_x#1(0(), S(x10)) -> False() 32: eqNat#1(x6) -> eqNat_x(x6) 33: eqNat#2(x6, x7) -> eqNat_x#1(x6, x7) 34: leqNat_x#1(x4, 0()) -> True() 35: leqNat_x#1(S(x2), S(x1)) -> leqNat#2(x2, x1) 36: leqNat_x#1(0(), S(x8)) -> False() 37: leqNat#1(x4) -> leqNat_x(x4) 38: leqNat#2(x4, x5) -> leqNat_x#1(x4, x5) 39: main(x2, x1) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq_nr :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq_nr#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool bot[0] :: bool bot[1] :: 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 ite :: bool -> bool -> bool -> bool ite#1 :: bool -> bool -> bool -> bool ite#2 :: bool -> bool -> bool -> bool ite#3 :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool ite2#1 :: bool -> bool -> bool -> bool ite2#2 :: bool -> bool -> bool -> bool ite2#3 :: bool -> bool -> bool -> bool ite2_b :: bool -> bool -> bool -> bool ite2_b#1 :: bool -> bool -> bool -> bool ite2_b#2 :: bool -> bool -> bool -> bool ite2_b_th :: bool -> bool -> bool -> bool ite2_b_th#1 :: bool -> bool -> bool -> bool ite_b :: bool -> bool -> bool -> bool ite_b#1 :: bool -> bool -> bool -> bool ite_b#2 :: bool -> bool -> bool -> bool ite_b_th :: bool -> bool -> bool -> bool ite_b_th#1 :: bool -> bool -> bool -> bool leqNat :: nat -> nat -> bool leqNat#1 :: nat -> nat -> bool leqNat#2 :: nat -> nat -> bool leqNat_x :: nat -> nat -> bool leqNat_x#1 :: nat -> nat -> bool lookup#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool lookup#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool lookup_n :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool lookup_n#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 14: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, Leaf(x1)) -> anyEq#2(eqNat(), ite(), x2, x1) 2: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, Node(Nil(), ConsTree(x2, x1))) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, x2) 3: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x1, Node(Nil(), NilTree())) -> bot[0]() 4: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, Node(Cons(x4, x3), ConsTree(x2, x1))) -> ite2#3(leqNat#2(x5, x4), lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, x2) , lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x5, Node(x3, x1))) 5: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, Node(Cons(x2, x1), NilTree())) -> bot[1]() 7: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x1, x2) -> lookup_n#1(leqNat(), ite2() , anyEq(eqNat(), ite()) , x1 , x2) 8: anyEq_nr#1(eqNat(), ite(), x1, Nil()) -> False() 9: anyEq_nr#1(eqNat(), ite(), x3, Cons(x2, x1)) -> ite#3(eqNat#2(x3, x2), True() , anyEq#2(eqNat(), ite(), x3, x1)) 11: anyEq#2(eqNat(), ite(), x1, x2) -> anyEq_nr#1(eqNat(), ite(), x1, x2) 15: ite2_b#2(True(), x24, x28) -> x24 16: ite2_b#2(False(), x24, x28) -> x28 19: ite2#3(x5, x6, x7) -> ite2_b#2(x5, x6, x7) 23: ite_b#2(True(), True(), x2) -> True() 24: ite_b#2(False(), True(), x2) -> x2 27: ite#3(x4, x5, x6) -> ite_b#2(x4, x5, x6) 28: eqNat_x#1(0(), 0()) -> True() 29: eqNat_x#1(S(x10), 0()) -> False() 30: eqNat_x#1(S(x2), S(x1)) -> eqNat#2(x2, x1) 31: eqNat_x#1(0(), S(x10)) -> False() 33: eqNat#2(x6, x7) -> eqNat_x#1(x6, x7) 34: leqNat_x#1(x4, 0()) -> True() 35: leqNat_x#1(S(x2), S(x1)) -> leqNat#2(x2, x1) 36: leqNat_x#1(0(), S(x8)) -> False() 38: leqNat#2(x4, x5) -> leqNat_x#1(x4, x5) 39: main(x2, x1) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq_nr#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool bot[0] :: bool bot[1] :: bool eqNat :: nat -> nat -> bool eqNat#2 :: nat -> nat -> bool eqNat_x#1 :: nat -> nat -> bool ite :: bool -> bool -> bool -> bool ite#3 :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool ite2#3 :: bool -> bool -> bool -> bool ite2_b#2 :: bool -> bool -> bool -> bool ite_b#2 :: bool -> bool -> bool -> bool leqNat :: nat -> nat -> bool leqNat#2 :: nat -> nat -> bool leqNat_x#1 :: nat -> nat -> bool lookup#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool lookup_n#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, Leaf(x1)) -> anyEq#2(eqNat(), ite(), x2, x1) 2: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, Node(Nil(), ConsTree(x2, x1))) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, x2) 3: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x1, Node(Nil(), NilTree())) -> bot[0]() 4: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x11, Node(Cons(x9, x7), ConsTree(x5, x3))) -> ite2_b#2(leqNat#2(x11, x9), lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x11, x5) , lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x11, Node(x7, x3))) 5: lookup_n#1(leqNat(), ite2(), anyEq(eqNat(), ite()), x3, Node(Cons(x2, x1), NilTree())) -> bot[1]() 6: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x4, Leaf(x2)) -> anyEq#2(eqNat(), ite(), x4, x2) 7: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x6, Node(Nil(), ConsTree(x4, x2))) -> lookup#2(leqNat() , ite2() , anyEq(eqNat() , ite()) , x6 , x4) 8: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, Node(Nil(), NilTree())) -> bot[0]() 9: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x10, Node(Cons(x8, x6), ConsTree(x4, x2))) -> ite2#3(leqNat#2(x10, x8), lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x10, x4) , lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x10, Node(x6, x2))) 10: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x6, Node(Cons(x4, x2), NilTree())) -> bot[1]() 11: anyEq_nr#1(eqNat(), ite(), x1, Nil()) -> False() 12: anyEq_nr#1(eqNat(), ite(), x7, Cons(x5, x3)) -> ite_b#2(eqNat#2(x7, x5), True() , anyEq#2(eqNat(), ite(), x7, x3)) 13: anyEq#2(eqNat(), ite(), x2, Nil()) -> False() 14: anyEq#2(eqNat(), ite(), x6, Cons(x4, x2)) -> ite#3(eqNat#2(x6, x4), True() , anyEq#2(eqNat(), ite(), x6, x2)) 15: ite2_b#2(True(), x24, x28) -> x24 16: ite2_b#2(False(), x24, x28) -> x28 17: ite2#3(True(), x48, x56) -> x48 18: ite2#3(False(), x48, x56) -> x56 19: ite_b#2(True(), True(), x2) -> True() 20: ite_b#2(False(), True(), x2) -> x2 21: ite#3(True(), True(), x4) -> True() 22: ite#3(False(), True(), x4) -> x4 23: eqNat_x#1(0(), 0()) -> True() 24: eqNat_x#1(S(x10), 0()) -> False() 25: eqNat_x#1(S(x2), S(x1)) -> eqNat#2(x2, x1) 26: eqNat_x#1(0(), S(x10)) -> False() 27: eqNat#2(0(), 0()) -> True() 28: eqNat#2(S(x20), 0()) -> False() 29: eqNat#2(S(x4), S(x2)) -> eqNat#2(x4, x2) 30: eqNat#2(0(), S(x20)) -> False() 31: leqNat_x#1(x4, 0()) -> True() 32: leqNat_x#1(S(x2), S(x1)) -> leqNat#2(x2, x1) 33: leqNat_x#1(0(), S(x8)) -> False() 34: leqNat#2(x8, 0()) -> True() 35: leqNat#2(S(x4), S(x2)) -> leqNat#2(x4, x2) 36: leqNat#2(0(), S(x16)) -> False() 37: main(x2, x1) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq_nr#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool bot[0] :: bool bot[1] :: bool eqNat :: nat -> nat -> bool eqNat#2 :: nat -> nat -> bool eqNat_x#1 :: nat -> nat -> bool ite :: bool -> bool -> bool -> bool ite#3 :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool ite2#3 :: bool -> bool -> bool -> bool ite2_b#2 :: bool -> bool -> bool -> bool ite_b#2 :: bool -> bool -> bool -> bool leqNat :: nat -> nat -> bool leqNat#2 :: nat -> nat -> bool leqNat_x#1 :: nat -> nat -> bool lookup#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool lookup_n#1 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 6: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x4, Leaf(x2)) -> anyEq#2(eqNat(), ite(), x4, x2) 7: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x6, Node(Nil(), ConsTree(x4, x2))) -> lookup#2(leqNat() , ite2() , anyEq(eqNat() , ite()) , x6 , x4) 8: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, Node(Nil(), NilTree())) -> bot[0]() 9: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x10, Node(Cons(x8, x6), ConsTree(x4, x2))) -> ite2#3(leqNat#2(x10, x8), lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x10, x4) , lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x10, Node(x6, x2))) 10: lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x6, Node(Cons(x4, x2), NilTree())) -> bot[1]() 13: anyEq#2(eqNat(), ite(), x2, Nil()) -> False() 14: anyEq#2(eqNat(), ite(), x6, Cons(x4, x2)) -> ite#3(eqNat#2(x6, x4), True() , anyEq#2(eqNat(), ite(), x6, x2)) 17: ite2#3(True(), x48, x56) -> x48 18: ite2#3(False(), x48, x56) -> x56 21: ite#3(True(), True(), x4) -> True() 22: ite#3(False(), True(), x4) -> x4 27: eqNat#2(0(), 0()) -> True() 28: eqNat#2(S(x20), 0()) -> False() 29: eqNat#2(S(x4), S(x2)) -> eqNat#2(x4, x2) 30: eqNat#2(0(), S(x20)) -> False() 34: leqNat#2(x8, 0()) -> True() 35: leqNat#2(S(x4), S(x2)) -> leqNat#2(x4, x2) 36: leqNat#2(0(), S(x16)) -> False() 37: main(x2, x1) -> lookup#2(leqNat(), ite2(), anyEq(eqNat(), ite()), x2, x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool anyEq :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool anyEq#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> nat -> nat list -> bool bot[0] :: bool bot[1] :: bool eqNat :: nat -> nat -> bool eqNat#2 :: nat -> nat -> bool ite :: bool -> bool -> bool -> bool ite#3 :: bool -> bool -> bool -> bool ite2 :: bool -> bool -> bool -> bool ite2#3 :: bool -> bool -> bool -> bool leqNat :: nat -> nat -> bool leqNat#2 :: nat -> nat -> bool lookup#2 :: (nat -> nat -> bool) -> (bool -> bool -> bool -> bool) -> (nat -> nat list -> bool) -> nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: Compression + Details: none * Step 17: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: lookup#2(x4, Leaf(x2)) -> anyEq#2(x4, x2) 2: lookup#2(x6, Node(Nil(), ConsTree(x4, x2))) -> lookup#2(x6, x4) 3: lookup#2(x2, Node(Nil(), NilTree())) -> bot[0]() 4: lookup#2(x10, Node(Cons(x8, x6), ConsTree(x4, x2))) -> ite2#3(leqNat#2(x10, x8), lookup#2(x10, x4) , lookup#2(x10, Node(x6, x2))) 5: lookup#2(x6, Node(Cons(x4, x2), NilTree())) -> bot[1]() 6: anyEq#2(x2, Nil()) -> False() 7: anyEq#2(x6, Cons(x4, x2)) -> ite#3(eqNat#2(x6, x4), anyEq#2(x6, x2)) 8: ite2#3(True(), x48, x56) -> x48 9: ite2#3(False(), x48, x56) -> x56 10: ite#3(True(), x4) -> True() 11: ite#3(False(), x4) -> x4 12: eqNat#2(0(), 0()) -> True() 13: eqNat#2(S(x20), 0()) -> False() 14: eqNat#2(S(x4), S(x2)) -> eqNat#2(x4, x2) 15: eqNat#2(0(), S(x20)) -> False() 16: leqNat#2(x8, 0()) -> True() 17: leqNat#2(S(x4), S(x2)) -> leqNat#2(x4, x2) 18: leqNat#2(0(), S(x16)) -> False() 19: main(x2, x1) -> lookup#2(x2, x1) where 0 :: nat Cons :: 'a -> 'a list -> 'a list ConsTree :: 'a -> 'a treelist -> 'a treelist False :: bool Leaf :: nat list -> tree Nil :: 'a list NilTree :: 'a treelist Node :: nat list -> tree treelist -> tree S :: nat -> nat True :: bool anyEq#2 :: nat -> nat list -> bool bot[0] :: bool bot[1] :: bool eqNat#2 :: nat -> nat -> bool ite#3 :: bool -> bool -> bool ite2#3 :: bool -> bool -> bool -> bool leqNat#2 :: nat -> nat -> bool lookup#2 :: nat -> tree -> bool main :: nat -> tree -> bool + Applied Processor: ToTctProblem + Details: none * Step 18: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anyEq#2(x2,Nil()) -> False() anyEq#2(x6,Cons(x4,x2)) -> ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) -> True() eqNat#2(0(),S(x20)) -> False() eqNat#2(S(x20),0()) -> False() eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2) ite#3(False(),x4) -> x4 ite#3(True(),x4) -> True() ite2#3(False(),x48,x56) -> x56 ite2#3(True(),x48,x56) -> x48 leqNat#2(x8,0()) -> True() leqNat#2(0(),S(x16)) -> False() leqNat#2(S(x4),S(x2)) -> leqNat#2(x4,x2) lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) -> ite2#3(leqNat#2(x10,x8) ,lookup#2(x10,x4) ,lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) -> bot[0]() lookup#2(x4,Leaf(x2)) -> anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) -> bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) -> lookup#2(x6,x4) main(x2,x1) -> lookup#2(x2,x1) - Signature: {anyEq#2/2,eqNat#2/2,ite#3/2,ite2#3/3,leqNat#2/2,lookup#2/2,main/2} / {0/0,Cons/2,ConsTree/2,False/0,Leaf/1 ,Nil/0,NilTree/0,Node/2,S/1,True/0,bot[0]/0,bot[1]/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,ConsTree,False,Leaf,Nil ,NilTree,Node,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(ite#3) = {1,2}, uargs(ite2#3) = {1,2,3} Following symbols are considered usable: {anyEq#2,eqNat#2,ite#3,ite2#3,leqNat#2,lookup#2,main} TcT has computed the following interpretation: p(0) = 0 p(Cons) = x1 p(ConsTree) = 0 p(False) = 0 p(Leaf) = 0 p(Nil) = 0 p(NilTree) = 0 p(Node) = 0 p(S) = 0 p(True) = 0 p(anyEq#2) = 0 p(bot[0]) = 0 p(bot[1]) = 0 p(eqNat#2) = 0 p(ite#3) = 4*x1 + x2 p(ite2#3) = 4*x1 + x2 + x3 p(leqNat#2) = 0 p(lookup#2) = 0 p(main) = 5 Following rules are strictly oriented: main(x2,x1) = 5 > 0 = lookup#2(x2,x1) Following rules are (at-least) weakly oriented: anyEq#2(x2,Nil()) = 0 >= 0 = False() anyEq#2(x6,Cons(x4,x2)) = 0 >= 0 = ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) = 0 >= 0 = True() eqNat#2(0(),S(x20)) = 0 >= 0 = False() eqNat#2(S(x20),0()) = 0 >= 0 = False() eqNat#2(S(x4),S(x2)) = 0 >= 0 = eqNat#2(x4,x2) ite#3(False(),x4) = x4 >= x4 = x4 ite#3(True(),x4) = x4 >= 0 = True() ite2#3(False(),x48,x56) = x48 + x56 >= x56 = x56 ite2#3(True(),x48,x56) = x48 + x56 >= x48 = x48 leqNat#2(x8,0()) = 0 >= 0 = True() leqNat#2(0(),S(x16)) = 0 >= 0 = False() leqNat#2(S(x4),S(x2)) = 0 >= 0 = leqNat#2(x4,x2) lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) = 0 >= 0 = ite2#3(leqNat#2(x10,x8),lookup#2(x10,x4),lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) = 0 >= 0 = bot[0]() lookup#2(x4,Leaf(x2)) = 0 >= 0 = anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) = 0 >= 0 = bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) = 0 >= 0 = lookup#2(x6,x4) * Step 19: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anyEq#2(x2,Nil()) -> False() anyEq#2(x6,Cons(x4,x2)) -> ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) -> True() eqNat#2(0(),S(x20)) -> False() eqNat#2(S(x20),0()) -> False() eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2) ite#3(False(),x4) -> x4 ite#3(True(),x4) -> True() ite2#3(False(),x48,x56) -> x56 ite2#3(True(),x48,x56) -> x48 leqNat#2(x8,0()) -> True() leqNat#2(0(),S(x16)) -> False() leqNat#2(S(x4),S(x2)) -> leqNat#2(x4,x2) lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) -> ite2#3(leqNat#2(x10,x8) ,lookup#2(x10,x4) ,lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) -> bot[0]() lookup#2(x4,Leaf(x2)) -> anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) -> bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) -> lookup#2(x6,x4) - Weak TRS: main(x2,x1) -> lookup#2(x2,x1) - Signature: {anyEq#2/2,eqNat#2/2,ite#3/2,ite2#3/3,leqNat#2/2,lookup#2/2,main/2} / {0/0,Cons/2,ConsTree/2,False/0,Leaf/1 ,Nil/0,NilTree/0,Node/2,S/1,True/0,bot[0]/0,bot[1]/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,ConsTree,False,Leaf,Nil ,NilTree,Node,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(ite#3) = {1,2}, uargs(ite2#3) = {1,2,3} Following symbols are considered usable: {anyEq#2,eqNat#2,ite#3,ite2#3,leqNat#2,lookup#2,main} TcT has computed the following interpretation: p(0) = 4 p(Cons) = 7 + x1 + x2 p(ConsTree) = 7 + x1 + x2 p(False) = 0 p(Leaf) = x1 p(Nil) = 1 p(NilTree) = 3 p(Node) = x1 + x2 p(S) = 2 + x1 p(True) = 0 p(anyEq#2) = 0 p(bot[0]) = 5 p(bot[1]) = 7 p(eqNat#2) = 0 p(ite#3) = 4*x1 + x2 p(ite2#3) = 1 + 6*x1 + x2 + x3 p(leqNat#2) = 2 p(lookup#2) = 1 + x2 p(main) = 6 + 6*x1 + 3*x2 Following rules are strictly oriented: ite2#3(False(),x48,x56) = 1 + x48 + x56 > x56 = x56 ite2#3(True(),x48,x56) = 1 + x48 + x56 > x48 = x48 leqNat#2(x8,0()) = 2 > 0 = True() leqNat#2(0(),S(x16)) = 2 > 0 = False() lookup#2(x4,Leaf(x2)) = 1 + x2 > 0 = anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) = 11 + x2 + x4 > 7 = bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) = 9 + x2 + x4 > 1 + x4 = lookup#2(x6,x4) Following rules are (at-least) weakly oriented: anyEq#2(x2,Nil()) = 0 >= 0 = False() anyEq#2(x6,Cons(x4,x2)) = 0 >= 0 = ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) = 0 >= 0 = True() eqNat#2(0(),S(x20)) = 0 >= 0 = False() eqNat#2(S(x20),0()) = 0 >= 0 = False() eqNat#2(S(x4),S(x2)) = 0 >= 0 = eqNat#2(x4,x2) ite#3(False(),x4) = x4 >= x4 = x4 ite#3(True(),x4) = x4 >= 0 = True() leqNat#2(S(x4),S(x2)) = 2 >= 2 = leqNat#2(x4,x2) lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) = 15 + x2 + x4 + x6 + x8 >= 15 + x2 + x4 + x6 = ite2#3(leqNat#2(x10,x8),lookup#2(x10,x4),lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) = 5 >= 5 = bot[0]() main(x2,x1) = 6 + 3*x1 + 6*x2 >= 1 + x1 = lookup#2(x2,x1) * Step 20: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: anyEq#2(x2,Nil()) -> False() anyEq#2(x6,Cons(x4,x2)) -> ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) -> True() eqNat#2(0(),S(x20)) -> False() eqNat#2(S(x20),0()) -> False() eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2) ite#3(False(),x4) -> x4 ite#3(True(),x4) -> True() leqNat#2(S(x4),S(x2)) -> leqNat#2(x4,x2) lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) -> ite2#3(leqNat#2(x10,x8) ,lookup#2(x10,x4) ,lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) -> bot[0]() - Weak TRS: ite2#3(False(),x48,x56) -> x56 ite2#3(True(),x48,x56) -> x48 leqNat#2(x8,0()) -> True() leqNat#2(0(),S(x16)) -> False() lookup#2(x4,Leaf(x2)) -> anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) -> bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) -> lookup#2(x6,x4) main(x2,x1) -> lookup#2(x2,x1) - Signature: {anyEq#2/2,eqNat#2/2,ite#3/2,ite2#3/3,leqNat#2/2,lookup#2/2,main/2} / {0/0,Cons/2,ConsTree/2,False/0,Leaf/1 ,Nil/0,NilTree/0,Node/2,S/1,True/0,bot[0]/0,bot[1]/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,ConsTree,False,Leaf,Nil ,NilTree,Node,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(ite#3) = {1,2}, uargs(ite2#3) = {1,2,3} Following symbols are considered usable: {anyEq#2,eqNat#2,ite#3,ite2#3,leqNat#2,lookup#2,main} TcT has computed the following interpretation: p(0) = 2 p(Cons) = 7 + x2 p(ConsTree) = 4 + x1 + x2 p(False) = 0 p(Leaf) = x1 p(Nil) = 6 p(NilTree) = 4 p(Node) = x2 p(S) = 2 p(True) = 0 p(anyEq#2) = 2*x2 p(bot[0]) = 0 p(bot[1]) = 4 p(eqNat#2) = 2 p(ite#3) = 7 + x1 + x2 p(ite2#3) = 1 + 2*x1 + x2 + x3 p(leqNat#2) = 0 p(lookup#2) = 1 + 2*x2 p(main) = 4 + 2*x1 + 5*x2 Following rules are strictly oriented: anyEq#2(x2,Nil()) = 12 > 0 = False() anyEq#2(x6,Cons(x4,x2)) = 14 + 2*x2 > 9 + 2*x2 = ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) = 2 > 0 = True() eqNat#2(0(),S(x20)) = 2 > 0 = False() eqNat#2(S(x20),0()) = 2 > 0 = False() ite#3(False(),x4) = 7 + x4 > x4 = x4 ite#3(True(),x4) = 7 + x4 > 0 = True() lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) = 9 + 2*x2 + 2*x4 > 3 + 2*x2 + 2*x4 = ite2#3(leqNat#2(x10,x8),lookup#2(x10,x4),lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) = 9 > 0 = bot[0]() Following rules are (at-least) weakly oriented: eqNat#2(S(x4),S(x2)) = 2 >= 2 = eqNat#2(x4,x2) ite2#3(False(),x48,x56) = 1 + x48 + x56 >= x56 = x56 ite2#3(True(),x48,x56) = 1 + x48 + x56 >= x48 = x48 leqNat#2(x8,0()) = 0 >= 0 = True() leqNat#2(0(),S(x16)) = 0 >= 0 = False() leqNat#2(S(x4),S(x2)) = 0 >= 0 = leqNat#2(x4,x2) lookup#2(x4,Leaf(x2)) = 1 + 2*x2 >= 2*x2 = anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) = 9 >= 4 = bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) = 9 + 2*x2 + 2*x4 >= 1 + 2*x4 = lookup#2(x6,x4) main(x2,x1) = 4 + 5*x1 + 2*x2 >= 1 + 2*x1 = lookup#2(x2,x1) * Step 21: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2) leqNat#2(S(x4),S(x2)) -> leqNat#2(x4,x2) - Weak TRS: anyEq#2(x2,Nil()) -> False() anyEq#2(x6,Cons(x4,x2)) -> ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) -> True() eqNat#2(0(),S(x20)) -> False() eqNat#2(S(x20),0()) -> False() ite#3(False(),x4) -> x4 ite#3(True(),x4) -> True() ite2#3(False(),x48,x56) -> x56 ite2#3(True(),x48,x56) -> x48 leqNat#2(x8,0()) -> True() leqNat#2(0(),S(x16)) -> False() lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) -> ite2#3(leqNat#2(x10,x8) ,lookup#2(x10,x4) ,lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) -> bot[0]() lookup#2(x4,Leaf(x2)) -> anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) -> bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) -> lookup#2(x6,x4) main(x2,x1) -> lookup#2(x2,x1) - Signature: {anyEq#2/2,eqNat#2/2,ite#3/2,ite2#3/3,leqNat#2/2,lookup#2/2,main/2} / {0/0,Cons/2,ConsTree/2,False/0,Leaf/1 ,Nil/0,NilTree/0,Node/2,S/1,True/0,bot[0]/0,bot[1]/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,ConsTree,False,Leaf,Nil ,NilTree,Node,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: uargs(ite#3) = {1,2}, uargs(ite2#3) = {1,2,3} Following symbols are considered usable: {anyEq#2,eqNat#2,ite#3,ite2#3,leqNat#2,lookup#2,main} TcT has computed the following interpretation: p(0) = 5 p(Cons) = 1 + x1 + x2 p(ConsTree) = x1 + x2 p(False) = 0 p(Leaf) = x1 p(Nil) = 0 p(NilTree) = 0 p(Node) = 2 + x1 + x2 p(S) = 2 + x1 p(True) = 6 p(anyEq#2) = 4*x2 p(bot[0]) = 0 p(bot[1]) = 0 p(eqNat#2) = 1 + x2 p(ite#3) = 2*x1 + x2 p(ite2#3) = x1 + x2 + x3 p(leqNat#2) = 4 + 2*x2 p(lookup#2) = 4*x2 p(main) = 5 + 5*x2 Following rules are strictly oriented: eqNat#2(S(x4),S(x2)) = 3 + x2 > 1 + x2 = eqNat#2(x4,x2) leqNat#2(S(x4),S(x2)) = 8 + 2*x2 > 4 + 2*x2 = leqNat#2(x4,x2) Following rules are (at-least) weakly oriented: anyEq#2(x2,Nil()) = 0 >= 0 = False() anyEq#2(x6,Cons(x4,x2)) = 4 + 4*x2 + 4*x4 >= 2 + 4*x2 + 2*x4 = ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) = 6 >= 6 = True() eqNat#2(0(),S(x20)) = 3 + x20 >= 0 = False() eqNat#2(S(x20),0()) = 6 >= 0 = False() ite#3(False(),x4) = x4 >= x4 = x4 ite#3(True(),x4) = 12 + x4 >= 6 = True() ite2#3(False(),x48,x56) = x48 + x56 >= x56 = x56 ite2#3(True(),x48,x56) = 6 + x48 + x56 >= x48 = x48 leqNat#2(x8,0()) = 14 >= 6 = True() leqNat#2(0(),S(x16)) = 8 + 2*x16 >= 0 = False() lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) = 12 + 4*x2 + 4*x4 + 4*x6 + 4*x8 >= 12 + 4*x2 + 4*x4 + 4*x6 + 2*x8 = ite2#3(leqNat#2(x10,x8),lookup#2(x10,x4),lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) = 8 >= 0 = bot[0]() lookup#2(x4,Leaf(x2)) = 4*x2 >= 4*x2 = anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) = 12 + 4*x2 + 4*x4 >= 0 = bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) = 8 + 4*x2 + 4*x4 >= 4*x4 = lookup#2(x6,x4) main(x2,x1) = 5 + 5*x1 >= 4*x1 = lookup#2(x2,x1) * Step 22: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: anyEq#2(x2,Nil()) -> False() anyEq#2(x6,Cons(x4,x2)) -> ite#3(eqNat#2(x6,x4),anyEq#2(x6,x2)) eqNat#2(0(),0()) -> True() eqNat#2(0(),S(x20)) -> False() eqNat#2(S(x20),0()) -> False() eqNat#2(S(x4),S(x2)) -> eqNat#2(x4,x2) ite#3(False(),x4) -> x4 ite#3(True(),x4) -> True() ite2#3(False(),x48,x56) -> x56 ite2#3(True(),x48,x56) -> x48 leqNat#2(x8,0()) -> True() leqNat#2(0(),S(x16)) -> False() leqNat#2(S(x4),S(x2)) -> leqNat#2(x4,x2) lookup#2(x10,Node(Cons(x8,x6),ConsTree(x4,x2))) -> ite2#3(leqNat#2(x10,x8) ,lookup#2(x10,x4) ,lookup#2(x10,Node(x6,x2))) lookup#2(x2,Node(Nil(),NilTree())) -> bot[0]() lookup#2(x4,Leaf(x2)) -> anyEq#2(x4,x2) lookup#2(x6,Node(Cons(x4,x2),NilTree())) -> bot[1]() lookup#2(x6,Node(Nil(),ConsTree(x4,x2))) -> lookup#2(x6,x4) main(x2,x1) -> lookup#2(x2,x1) - Signature: {anyEq#2/2,eqNat#2/2,ite#3/2,ite2#3/3,leqNat#2/2,lookup#2/2,main/2} / {0/0,Cons/2,ConsTree/2,False/0,Leaf/1 ,Nil/0,NilTree/0,Node/2,S/1,True/0,bot[0]/0,bot[1]/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Cons,ConsTree,False,Leaf,Nil ,NilTree,Node,S,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))