MAYBE * Step 1: Desugar MAYBE + Considered Problem: let rec leqNat y x = match y with | 0 -> True | S(y') -> match x with | S(x') -> leqNat x' y' | 0 -> False ;; let rec eqNat x y = match y with | 0 -> match x with | 0 -> True | S(x') -> False | S(y') -> match x with | S(x') -> eqNat x' y' | 0 -> False ;; let rec geqNat x y = match y with | 0 -> True | S(y') -> (match x with | 0 -> False | S(x') -> geqNat x' y') ;; let rec ltNat x y = match y with | 0 -> False | S(y') -> match x with | 0 -> True | S(x') -> ltNat x' y' ;; let rec gtNat x y = match x with | 0 -> False | S(x') -> match y with | 0 -> True | S(y') -> gtNat x' y' ;; let ifz n th el = match n with | 0 -> th 0 | S(x) -> el x ;; let ite 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 bool = True | False ;; type 'a option = None | Some of 'a ;; type 'a list = Nil | Cons of 'a * 'a list ;; type nat = 0 | S of nat ;; type Unit = Unit ;; type ('a,'b) pair = Pair of 'a * 'b ;; type var = Var of nat ;; let eq_var vv1 vv2 = match vv1 with | Var(v1) -> match vv2 with | Var(v2) -> eqNat v1 v2 ;; type funct = Fun of nat ;; let eq_fun ff1 ff2 = match ff1 with | Fun (f1) -> match ff2 with | Fun (f1) -> eqNat f1 f1 ;; type exp = Eadd of exp * exp | Emult of exp * exp | Ediv of exp * exp | Econst of nat | Evar of var * exp | Elet of var * exp * exp | Eapp of funct * exp ;; let eval1 e = let rec eval e = match e with | Eadd(e1, e2) -> plus (eval e1) (eval e2) | Emult(e1, e2) -> mult (eval e1) (eval e2) | Ediv(e1, e2) -> (match div_mod (eval e1) (eval e2) with | Triple(d,m,u) -> d) | Econst(n) -> n in eval e ;; let main e = eval1 e ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization MAYBE + Considered Problem: Ī»e : exp. (Ī»minus : nat -> nat -> (nat,nat) pair. (Ī»plus : nat -> nat -> nat. (Ī»div_mod : nat -> nat -> (nat,nat,nat) triple. (Ī»mult : nat -> nat -> nat. (Ī»eval1 : exp -> nat. (Ī»main : exp -> nat. main e) (Ī»e : exp. eval1 e)) (Ī»e : exp. (Ī»eval : exp -> nat. eval e) (Ī¼eval : exp -> nat. Ī»e : exp. case e of | Eadd -> Ī»e1 : exp. Ī»e2 : exp. plus (eval e1) (eval e2) | Emult -> Ī»e1 : exp. Ī»e2 : exp. mult (eval e1) (eval e2) | Ediv -> Ī»e1 : exp. Ī»e2 : exp. case div_mod (eval e1) (eval e2) of | Triple -> Ī»d : nat. Ī»m : nat. Ī»u : nat. d | Econst -> Ī»n : nat. n))) (Ī¼mult : nat -> nat -> nat. Ī»n : nat. Ī»m : nat. case n of | 0 -> 0 | S -> Ī»x : nat. S(plus (mult x m) m))) (Ī¼div_mod : nat -> nat -> (nat,nat,nat) triple. Ī»n : nat. Ī»m : nat. case minus n m of | Pair -> Ī»res : nat. Ī»m : nat. case res of | 0 -> Triple(0,n,m) | S -> Ī»x : nat. case div_mod res m of | Triple -> Ī»a : nat. Ī»rest : nat. Ī»unusedM : nat. Triple(plus S(0) a,rest,m))) (Ī¼plus : nat -> nat -> nat. Ī»n : nat. Ī»m : nat. case m of | 0 -> n | S -> Ī»x : nat. S(plus n x))) (Ī»n : nat. Ī»m : nat. (Ī»minus' : nat -> nat -> nat. Pair(minus' n m,m)) (Ī¼minus' : nat -> nat -> nat. Ī»m : nat. Ī»n : nat. case m of | 0 -> 0 | S -> Ī»x : nat. case n of | 0 -> m | S -> Ī»y : nat. minus' x y)) : exp -> nat where 0 :: nat Cons :: 'a -> 'a list -> 'a list Eadd :: exp -> exp -> exp Eapp :: funct -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Elet :: var -> exp -> exp -> exp Emult :: exp -> exp -> exp Evar :: var -> exp -> exp False :: bool Fun :: nat -> funct Nil :: 'a list None :: 'a option Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Some :: 'a -> 'a option Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple True :: bool Unit :: Unit Var :: nat -> var + Applied Processor: Defunctionalization + Details: none * Step 3: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x0) x5 -> main_6(x0) main_7(x5) 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: cond_eval_e(Eadd(x7, x8), x2, x3, x4) -> x2 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 7: cond_eval_e(Emult(x7, x8), x2, x3, x4) -> x4 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 8: cond_eval_e(Ediv(x7, x8), x2, x3, x4) -> cond_eval_e_1(x3 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8)) 9: cond_eval_e(Econst(x7), x2, x3, x4) -> x7 10: eval_1(x2, x3, x4) x6 -> cond_eval_e(x6, x2, x3, x4) 11: eval(x2, x3, x4) x5 -> eval_1(x2, x3, x4) x5 12: eval1(x2, x3, x4) x5 -> eval1_e(x5) eval(x2, x3, x4) 13: main_4(x0, x2, x3) x4 -> main_5(x0) eval1(x2, x3, x4) 14: cond_mult_n_m(0(), x2, x5) -> 0() 15: cond_mult_n_m(S(x6), x2, x5) -> S(x2 (mult(x2) x6 x5) x5) 16: mult_n(x2, x4) x5 -> cond_mult_n_m(x4, x2, x5) 17: mult_1(x2) x4 -> mult_n(x2, x4) 18: mult(x2) x3 -> mult_1(x2) x3 19: main_3(x0, x2) x3 -> main_4(x0, x2, x3) mult(x2) 20: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 21: cond_div_mod_n_m_1(0(), x1, x2, x3, x5, x6) -> Triple(0(), x3, x6) 22: cond_div_mod_n_m_1(S(x7), x1, x2, x3, x5, x6) -> cond_div_mod_n_m_2(div_mod(x1, x2) x5 x6, x2, x6) 23: cond_div_mod_n_m(Pair(x5, x6), x1, x2, x3) -> cond_div_mod_n_m_1(x5, x1, x2, x3, x5, x6) 24: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 25: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 26: div_mod(x1, x2) x3 -> div_mod_1(x1, x2) x3 27: main_2(x0, x1) x2 -> main_3(x0, x2) div_mod(x1, x2) 28: cond_plus_n_m(0(), x2) -> x2 29: cond_plus_n_m(S(x4), x2) -> S(plus() x2 x4) 30: plus_n(x2) x3 -> cond_plus_n_m(x3, x2) 31: plus_1() x2 -> plus_n(x2) 32: plus() x0 -> plus_1() x0 33: main_1(x0) x1 -> main_2(x0, x1) plus() 34: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 35: cond_minus'_m_n_1(0(), x3, x5) -> x3 36: cond_minus'_m_n_1(S(x6), x3, x5) -> minus'() x5 x6 37: cond_minus'_m_n(0(), x3, x4) -> 0() 38: cond_minus'_m_n(S(x5), x3, x4) -> cond_minus'_m_n_1(x4, x3, x5) 39: minus'_m(x3) x4 -> cond_minus'_m_n(x3, x3, x4) 40: minus'_1() x3 -> minus'_m(x3) 41: minus'() x0 -> minus'_1() x0 42: minus_n(x1) x2 -> minus_n_m(x1, x2) minus'() 43: minus() x1 -> minus_n(x1) 44: main(x0) -> main_1(x0) minus() where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_eval_e :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat cond_minus'_m_n :: nat -> nat -> nat -> nat cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_1 :: nat -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> nat -> (nat,nat,nat) triple cond_minus'_m_n_1 :: nat -> nat -> nat -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x0) x11 -> main_7(x11) x0 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: cond_eval_e(Eadd(x7, x8), x2, x3, x4) -> x2 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 7: cond_eval_e(Emult(x7, x8), x2, x3, x4) -> x4 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 8: cond_eval_e(Ediv(x7, x8), x2, x3, x4) -> cond_eval_e_1(x3 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8)) 9: cond_eval_e(Econst(x7), x2, x3, x4) -> x7 10: eval_1(x2, x3, x4) x6 -> cond_eval_e(x6, x2, x3, x4) 11: eval(x4, x6, x8) x12 -> cond_eval_e(x12, x4, x6, x8) 12: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 13: main_4(x0, x5, x7) x9 -> main_6(x0) main_7(eval1(x5, x7, x9)) 14: cond_mult_n_m(0(), x2, x5) -> 0() 15: cond_mult_n_m(S(x6), x2, x5) -> S(x2 (mult(x2) x6 x5) x5) 16: mult_n(x2, x4) x5 -> cond_mult_n_m(x4, x2, x5) 17: mult_1(x2) x4 -> mult_n(x2, x4) 18: mult(x4) x8 -> mult_n(x4, x8) 19: main_3(x0, x4) x6 -> main_5(x0) eval1(x4, x6, mult(x4)) 20: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 21: cond_div_mod_n_m_1(0(), x1, x2, x3, x5, x6) -> Triple(0(), x3, x6) 22: cond_div_mod_n_m_1(S(x7), x1, x2, x3, x5, x6) -> cond_div_mod_n_m_2(div_mod(x1, x2) x5 x6, x2, x6) 23: cond_div_mod_n_m(Pair(x5, x6), x1, x2, x3) -> cond_div_mod_n_m_1(x5, x1, x2, x3, x5, x6) 24: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 25: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 26: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 27: main_2(x0, x3) x4 -> main_4(x0, x4, div_mod(x3, x4)) mult(x4) 28: cond_plus_n_m(0(), x2) -> x2 29: cond_plus_n_m(S(x4), x2) -> S(plus() x2 x4) 30: plus_n(x2) x3 -> cond_plus_n_m(x3, x2) 31: plus_1() x2 -> plus_n(x2) 32: plus() x4 -> plus_n(x4) 33: main_1(x0) x2 -> main_3(x0, plus()) div_mod(x2, plus()) 34: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 35: cond_minus'_m_n_1(0(), x3, x5) -> x3 36: cond_minus'_m_n_1(S(x6), x3, x5) -> minus'() x5 x6 37: cond_minus'_m_n(0(), x3, x4) -> 0() 38: cond_minus'_m_n(S(x5), x3, x4) -> cond_minus'_m_n_1(x4, x3, x5) 39: minus'_m(x3) x4 -> cond_minus'_m_n(x3, x3, x4) 40: minus'_1() x3 -> minus'_m(x3) 41: minus'() x6 -> minus'_m(x6) 42: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 43: minus() x1 -> minus_n(x1) 44: main(x0) -> main_2(x0, minus()) plus() where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_eval_e :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat cond_minus'_m_n :: nat -> nat -> nat -> nat cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_1 :: nat -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> nat -> (nat,nat,nat) triple cond_minus'_m_n_1 :: nat -> nat -> nat -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x12) x10 -> x10 x12 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: cond_eval_e(Eadd(x7, x8), x2, x3, x4) -> x2 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 7: cond_eval_e(Emult(x7, x8), x2, x3, x4) -> x4 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 8: cond_eval_e(Ediv(x7, x8), x2, x3, x4) -> cond_eval_e_1(x3 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8)) 9: cond_eval_e(Econst(x7), x2, x3, x4) -> x7 10: eval_1(x2, x3, x4) x6 -> cond_eval_e(x6, x2, x3, x4) 11: eval(x4, x6, x8) x12 -> cond_eval_e(x12, x4, x6, x8) 12: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 13: main_4(x0, x11, x15) x19 -> main_7(eval1(x11, x15, x19)) x0 14: cond_mult_n_m(0(), x2, x5) -> 0() 15: cond_mult_n_m(S(x6), x2, x5) -> S(x2 (mult(x2) x6 x5) x5) 16: mult_n(x2, x4) x5 -> cond_mult_n_m(x4, x2, x5) 17: mult_1(x2) x4 -> mult_n(x2, x4) 18: mult(x4) x8 -> mult_n(x4, x8) 19: main_3(x0, x9) x13 -> main_7(eval1(x9, x13, mult(x9))) x0 20: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 21: cond_div_mod_n_m_1(0(), x1, x2, x3, x5, x6) -> Triple(0(), x3, x6) 22: cond_div_mod_n_m_1(S(x7), x1, x2, x3, x5, x6) -> cond_div_mod_n_m_2(div_mod(x1, x2) x5 x6, x2, x6) 23: cond_div_mod_n_m(Pair(x5, x6), x1, x2, x3) -> cond_div_mod_n_m_1(x5, x1, x2, x3, x5, x6) 24: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 25: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 26: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 27: main_2(x0, x7) x10 -> main_6(x0) main_7(eval1(x10, div_mod(x7, x10), mult(x10))) 28: cond_plus_n_m(0(), x2) -> x2 29: cond_plus_n_m(S(x4), x2) -> S(plus() x2 x4) 30: plus_n(x2) x3 -> cond_plus_n_m(x3, x2) 31: plus_1() x2 -> plus_n(x2) 32: plus() x4 -> plus_n(x4) 33: main_1(x0) x5 -> main_5(x0) eval1(plus(), div_mod(x5, plus()), mult(plus())) 34: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 35: cond_minus'_m_n_1(0(), x3, x5) -> x3 36: cond_minus'_m_n_1(S(x6), x3, x5) -> minus'() x5 x6 37: cond_minus'_m_n(0(), x3, x4) -> 0() 38: cond_minus'_m_n(S(x5), x3, x4) -> cond_minus'_m_n_1(x4, x3, x5) 39: minus'_m(x3) x4 -> cond_minus'_m_n(x3, x3, x4) 40: minus'_1() x3 -> minus'_m(x3) 41: minus'() x6 -> minus'_m(x6) 42: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 43: minus() x1 -> minus_n(x1) 44: main(x0) -> main_4(x0, plus(), div_mod(minus(), plus())) mult(plus()) where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_eval_e :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat cond_minus'_m_n :: nat -> nat -> nat -> nat cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_1 :: nat -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> nat -> (nat,nat,nat) triple cond_minus'_m_n_1 :: nat -> nat -> nat -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x12) x10 -> x10 x12 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: cond_eval_e(Eadd(x7, x8), x2, x3, x4) -> x2 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 7: cond_eval_e(Emult(x7, x8), x2, x3, x4) -> x4 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 8: cond_eval_e(Ediv(x7, x8), x2, x3, x4) -> cond_eval_e_1(x3 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8)) 9: cond_eval_e(Econst(x7), x2, x3, x4) -> x7 10: eval_1(x2, x3, x4) x6 -> cond_eval_e(x6, x2, x3, x4) 11: eval(x4, x6, x8) x12 -> cond_eval_e(x12, x4, x6, x8) 12: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 13: main_4(x12, x23, x31) x39 -> eval1(x23, x31, x39) x12 14: cond_mult_n_m(0(), x2, x5) -> 0() 15: cond_mult_n_m(S(x6), x2, x5) -> S(x2 (mult(x2) x6 x5) x5) 16: mult_n(x2, x4) x5 -> cond_mult_n_m(x4, x2, x5) 17: mult_1(x2) x4 -> mult_n(x2, x4) 18: mult(x4) x8 -> mult_n(x4, x8) 19: main_3(x12, x19) x27 -> eval1(x19, x27, mult(x19)) x12 20: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 21: cond_div_mod_n_m_1(0(), x1, x2, x3, x5, x6) -> Triple(0(), x3, x6) 22: cond_div_mod_n_m_1(S(x7), x1, x2, x3, x5, x6) -> cond_div_mod_n_m_2(div_mod(x1, x2) x5 x6, x2, x6) 23: cond_div_mod_n_m(Pair(x5, x6), x1, x2, x3) -> cond_div_mod_n_m_1(x5, x1, x2, x3, x5, x6) 24: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 25: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 26: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 27: main_2(x0, x15) x21 -> main_7(eval1(x21, div_mod(x15, x21), mult(x21))) x0 28: cond_plus_n_m(0(), x2) -> x2 29: cond_plus_n_m(S(x4), x2) -> S(plus() x2 x4) 30: plus_n(x2) x3 -> cond_plus_n_m(x3, x2) 31: plus_1() x2 -> plus_n(x2) 32: plus() x4 -> plus_n(x4) 33: main_1(x24) x11 -> eval1(plus(), div_mod(x11, plus()), mult(plus())) x24 34: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 35: cond_minus'_m_n_1(0(), x3, x5) -> x3 36: cond_minus'_m_n_1(S(x6), x3, x5) -> minus'() x5 x6 37: cond_minus'_m_n(0(), x3, x4) -> 0() 38: cond_minus'_m_n(S(x5), x3, x4) -> cond_minus'_m_n_1(x4, x3, x5) 39: minus'_m(x3) x4 -> cond_minus'_m_n(x3, x3, x4) 40: minus'_1() x3 -> minus'_m(x3) 41: minus'() x6 -> minus'_m(x6) 42: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 43: minus() x1 -> minus_n(x1) 44: main(x0) -> main_7(eval1(plus(), div_mod(minus(), plus()), mult(plus()))) x0 where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_eval_e :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat cond_minus'_m_n :: nat -> nat -> nat -> nat cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_1 :: nat -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> nat -> (nat,nat,nat) triple cond_minus'_m_n_1 :: nat -> nat -> nat -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x12) x10 -> x10 x12 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: cond_eval_e(Eadd(x7, x8), x2, x3, x4) -> x2 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 7: cond_eval_e(Emult(x7, x8), x2, x3, x4) -> x4 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 8: cond_eval_e(Ediv(x7, x8), x2, x3, x4) -> cond_eval_e_1(x3 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8)) 9: cond_eval_e(Econst(x7), x2, x3, x4) -> x7 10: eval_1(x2, x3, x4) x6 -> cond_eval_e(x6, x2, x3, x4) 11: eval(x4, x6, x8) x12 -> cond_eval_e(x12, x4, x6, x8) 12: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 13: main_4(x20, x10, x14) x18 -> eval(x10, x14, x18) x20 14: cond_mult_n_m(0(), x2, x5) -> 0() 15: cond_mult_n_m(S(x6), x2, x5) -> S(x2 (mult(x2) x6 x5) x5) 16: mult_n(x2, x4) x5 -> cond_mult_n_m(x4, x2, x5) 17: mult_1(x2) x4 -> mult_n(x2, x4) 18: mult(x4) x8 -> mult_n(x4, x8) 19: main_3(x20, x10) x14 -> eval(x10, x14, mult(x10)) x20 20: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 21: cond_div_mod_n_m_1(0(), x1, x2, x3, x5, x6) -> Triple(0(), x3, x6) 22: cond_div_mod_n_m_1(S(x7), x1, x2, x3, x5, x6) -> cond_div_mod_n_m_2(div_mod(x1, x2) x5 x6, x2, x6) 23: cond_div_mod_n_m(Pair(x5, x6), x1, x2, x3) -> cond_div_mod_n_m_1(x5, x1, x2, x3, x5, x6) 24: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 25: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 26: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 27: main_2(x12, x31) x43 -> eval1(x43, div_mod(x31, x43), mult(x43)) x12 28: cond_plus_n_m(0(), x2) -> x2 29: cond_plus_n_m(S(x4), x2) -> S(plus() x2 x4) 30: plus_n(x2) x3 -> cond_plus_n_m(x3, x2) 31: plus_1() x2 -> plus_n(x2) 32: plus() x4 -> plus_n(x4) 33: main_1(x20) x23 -> eval(plus(), div_mod(x23, plus()), mult(plus())) x20 34: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 35: cond_minus'_m_n_1(0(), x3, x5) -> x3 36: cond_minus'_m_n_1(S(x6), x3, x5) -> minus'() x5 x6 37: cond_minus'_m_n(0(), x3, x4) -> 0() 38: cond_minus'_m_n(S(x5), x3, x4) -> cond_minus'_m_n_1(x4, x3, x5) 39: minus'_m(x3) x4 -> cond_minus'_m_n(x3, x3, x4) 40: minus'_1() x3 -> minus'_m(x3) 41: minus'() x6 -> minus'_m(x6) 42: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 43: minus() x1 -> minus_n(x1) 44: main(x12) -> eval1(plus(), div_mod(minus(), plus()), mult(plus())) x12 where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_eval_e :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat cond_minus'_m_n :: nat -> nat -> nat -> nat cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_1 :: nat -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> nat -> (nat,nat,nat) triple cond_minus'_m_n_1 :: nat -> nat -> nat -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 8: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x12) x10 -> x10 x12 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: cond_eval_e(Eadd(x7, x8), x2, x3, x4) -> x2 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 7: cond_eval_e(Emult(x7, x8), x2, x3, x4) -> x4 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 8: cond_eval_e(Ediv(x7, x8), x2, x3, x4) -> cond_eval_e_1(x3 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8)) 9: cond_eval_e(Econst(x7), x2, x3, x4) -> x7 10: eval_1(x2, x3, x4) x6 -> cond_eval_e(x6, x2, x3, x4) 11: eval(x4, x6, x8) x12 -> cond_eval_e(x12, x4, x6, x8) 12: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 13: main_4(x20, x10, x14) x18 -> eval(x10, x14, x18) x20 14: cond_mult_n_m(0(), x2, x5) -> 0() 15: cond_mult_n_m(S(x6), x2, x5) -> S(x2 (mult(x2) x6 x5) x5) 16: mult_n(x2, x4) x5 -> cond_mult_n_m(x4, x2, x5) 17: mult_1(x2) x4 -> mult_n(x2, x4) 18: mult(x4) x8 -> mult_n(x4, x8) 19: main_3(x20, x10) x14 -> eval(x10, x14, mult(x10)) x20 20: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 21: cond_div_mod_n_m_1(0(), x1, x2, x3, x5, x6) -> Triple(0(), x3, x6) 22: cond_div_mod_n_m_1(S(x7), x1, x2, x3, x5, x6) -> cond_div_mod_n_m_2(div_mod(x1, x2) x5 x6, x2, x6) 23: cond_div_mod_n_m(Pair(x5, x6), x1, x2, x3) -> cond_div_mod_n_m_1(x5, x1, x2, x3, x5, x6) 24: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 25: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 26: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 27: main_2(x20, x63) x10 -> eval(x10, div_mod(x63, x10), mult(x10)) x20 28: cond_plus_n_m(0(), x2) -> x2 29: cond_plus_n_m(S(x4), x2) -> S(plus() x2 x4) 30: plus_n(x2) x3 -> cond_plus_n_m(x3, x2) 31: plus_1() x2 -> plus_n(x2) 32: plus() x4 -> plus_n(x4) 33: main_1(x20) x23 -> eval(plus(), div_mod(x23, plus()), mult(plus())) x20 34: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 35: cond_minus'_m_n_1(0(), x3, x5) -> x3 36: cond_minus'_m_n_1(S(x6), x3, x5) -> minus'() x5 x6 37: cond_minus'_m_n(0(), x3, x4) -> 0() 38: cond_minus'_m_n(S(x5), x3, x4) -> cond_minus'_m_n_1(x4, x3, x5) 39: minus'_m(x3) x4 -> cond_minus'_m_n(x3, x3, x4) 40: minus'_1() x3 -> minus'_m(x3) 41: minus'() x6 -> minus'_m(x6) 42: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 43: minus() x1 -> minus_n(x1) 44: main(x20) -> eval(plus(), div_mod(minus(), plus()), mult(plus())) x20 where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_eval_e :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat cond_minus'_m_n :: nat -> nat -> nat -> nat cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_1 :: nat -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> nat -> (nat,nat,nat) triple cond_minus'_m_n_1 :: nat -> nat -> nat -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 9: Inline MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x12) x10 -> x10 x12 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: cond_eval_e(Eadd(x7, x8), x2, x3, x4) -> x2 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 7: cond_eval_e(Emult(x7, x8), x2, x3, x4) -> x4 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 8: cond_eval_e(Ediv(x7, x8), x2, x3, x4) -> cond_eval_e_1(x3 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8)) 9: cond_eval_e(Econst(x7), x2, x3, x4) -> x7 10: eval_1(x4, x6, x8) Eadd(x14, x16) -> x4 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 11: eval_1(x4, x6, x8) Emult(x14, x16) -> x8 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 12: eval_1(x4, x6, x8) Ediv(x14, x16) -> cond_eval_e_1(x6 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16)) 13: eval_1(x4, x6, x8) Econst(x14) -> x14 14: eval(x4, x6, x8) Eadd(x14, x16) -> x4 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 15: eval(x4, x6, x8) Emult(x14, x16) -> x8 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 16: eval(x4, x6, x8) Ediv(x14, x16) -> cond_eval_e_1(x6 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16)) 17: eval(x4, x6, x8) Econst(x14) -> x14 18: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 19: main_4(x20, x10, x14) x18 -> eval(x10, x14, x18) x20 20: cond_mult_n_m(0(), x2, x5) -> 0() 21: cond_mult_n_m(S(x6), x2, x5) -> S(x2 (mult(x2) x6 x5) x5) 22: mult_n(x4, 0()) x10 -> 0() 23: mult_n(x4, S(x12)) x10 -> S(x4 (mult(x4) x12 x10) x10) 24: mult_1(x2) x4 -> mult_n(x2, x4) 25: mult(x4) x8 -> mult_n(x4, x8) 26: main_3(x20, x10) x14 -> eval(x10, x14, mult(x10)) x20 27: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 28: cond_div_mod_n_m_1(0(), x1, x2, x3, x5, x6) -> Triple(0(), x3, x6) 29: cond_div_mod_n_m_1(S(x7), x1, x2, x3, x5, x6) -> cond_div_mod_n_m_2(div_mod(x1, x2) x5 x6, x2, x6) 30: cond_div_mod_n_m(Pair(0(), x12), x2, x4, x6) -> Triple(0(), x6, x12) 31: cond_div_mod_n_m(Pair(S(x14), x12), x2, x4, x6) -> cond_div_mod_n_m_2(div_mod(x2, x4) S(x14) x12, x4 , x12) 32: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 33: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 34: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 35: main_2(x20, x63) x10 -> eval(x10, div_mod(x63, x10), mult(x10)) x20 36: cond_plus_n_m(0(), x2) -> x2 37: cond_plus_n_m(S(x4), x2) -> S(plus() x2 x4) 38: plus_n(x4) 0() -> x4 39: plus_n(x4) S(x8) -> S(plus() x4 x8) 40: plus_1() x2 -> plus_n(x2) 41: plus() x4 -> plus_n(x4) 42: main_1(x20) x23 -> eval(plus(), div_mod(x23, plus()), mult(plus())) x20 43: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 44: cond_minus'_m_n_1(0(), x3, x5) -> x3 45: cond_minus'_m_n_1(S(x6), x3, x5) -> minus'() x5 x6 46: cond_minus'_m_n(0(), x3, x4) -> 0() 47: cond_minus'_m_n(S(x10), x6, 0()) -> x6 48: cond_minus'_m_n(S(x10), x6, S(x12)) -> minus'() x10 x12 49: minus'_m(0()) x8 -> 0() 50: minus'_m(S(x10)) x8 -> cond_minus'_m_n_1(x8, S(x10), x10) 51: minus'_1() x3 -> minus'_m(x3) 52: minus'() x6 -> minus'_m(x6) 53: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 54: minus() x1 -> minus_n(x1) 55: main(x20) -> eval(plus(), div_mod(minus(), plus()), mult(plus())) x20 where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_eval_e :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat cond_minus'_m_n :: nat -> nat -> nat -> nat cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_1 :: nat -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> nat -> (nat,nat,nat) triple cond_minus'_m_n_1 :: nat -> nat -> nat -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 10: UsableRules MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x12) x10 -> x10 x12 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: cond_eval_e(Eadd(x7, x8), x2, x3, x4) -> x2 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 7: cond_eval_e(Emult(x7, x8), x2, x3, x4) -> x4 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8) 8: cond_eval_e(Ediv(x7, x8), x2, x3, x4) -> cond_eval_e_1(x3 (eval(x2, x3, x4) x7) (eval(x2, x3, x4) x8)) 9: cond_eval_e(Econst(x7), x2, x3, x4) -> x7 10: eval_1(x4, x6, x8) Eadd(x14, x16) -> x4 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 11: eval_1(x4, x6, x8) Emult(x14, x16) -> x8 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 12: eval_1(x4, x6, x8) Ediv(x14, x16) -> cond_eval_e_1(x6 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16)) 13: eval_1(x4, x6, x8) Econst(x14) -> x14 14: eval(x4, x6, x8) Eadd(x14, x16) -> x4 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 15: eval(x4, x6, x8) Emult(x14, x16) -> x8 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 16: eval(x4, x6, x8) Ediv(x14, x16) -> cond_eval_e_1(x6 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16)) 17: eval(x4, x6, x8) Econst(x14) -> x14 18: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 19: main_4(x20, x10, x14) x18 -> eval(x10, x14, x18) x20 20: cond_mult_n_m(0(), x2, x5) -> 0() 21: cond_mult_n_m(S(x6), x2, x5) -> S(x2 (mult(x2) x6 x5) x5) 22: mult_n(x4, 0()) x10 -> 0() 23: mult_n(x4, S(x12)) x10 -> S(x4 (mult(x4) x12 x10) x10) 24: mult_1(x2) x4 -> mult_n(x2, x4) 25: mult(x4) x8 -> mult_n(x4, x8) 26: main_3(x20, x10) x14 -> eval(x10, x14, mult(x10)) x20 27: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 28: cond_div_mod_n_m_1(0(), x1, x2, x3, x5, x6) -> Triple(0(), x3, x6) 29: cond_div_mod_n_m_1(S(x7), x1, x2, x3, x5, x6) -> cond_div_mod_n_m_2(div_mod(x1, x2) x5 x6, x2, x6) 30: cond_div_mod_n_m(Pair(0(), x12), x2, x4, x6) -> Triple(0(), x6, x12) 31: cond_div_mod_n_m(Pair(S(x14), x12), x2, x4, x6) -> cond_div_mod_n_m_2(div_mod(x2, x4) S(x14) x12, x4 , x12) 32: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 33: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 34: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 35: main_2(x20, x63) x10 -> eval(x10, div_mod(x63, x10), mult(x10)) x20 36: cond_plus_n_m(0(), x2) -> x2 37: cond_plus_n_m(S(x4), x2) -> S(plus() x2 x4) 38: plus_n(x4) 0() -> x4 39: plus_n(x4) S(x8) -> S(plus() x4 x8) 40: plus_1() x2 -> plus_n(x2) 41: plus() x4 -> plus_n(x4) 42: main_1(x20) x23 -> eval(plus(), div_mod(x23, plus()), mult(plus())) x20 43: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 44: cond_minus'_m_n_1(0(), x3, x5) -> x3 45: cond_minus'_m_n_1(S(x6), x3, x5) -> minus'() x5 x6 46: cond_minus'_m_n(0(), x3, x4) -> 0() 47: cond_minus'_m_n(S(x10), x6, 0()) -> x6 48: cond_minus'_m_n(S(x10), x6, S(x12)) -> minus'() x10 x12 49: minus'_m(0()) x8 -> 0() 50: minus'_m(S(x10)) 0() -> S(x10) 51: minus'_m(S(x10)) S(x12) -> minus'() x10 x12 52: minus'_1() x3 -> minus'_m(x3) 53: minus'() x6 -> minus'_m(x6) 54: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 55: minus() x1 -> minus_n(x1) 56: main(x20) -> eval(plus(), div_mod(minus(), plus()), mult(plus())) x20 where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_eval_e :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_mult_n_m :: nat -> (nat -> nat -> nat) -> nat -> nat cond_plus_n_m :: nat -> nat -> nat cond_minus'_m_n :: nat -> nat -> nat -> nat cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_1 :: nat -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> nat -> (nat,nat,nat) triple cond_minus'_m_n_1 :: nat -> nat -> nat -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 11: NeededRules MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x12) x10 -> x10 x12 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 10: eval_1(x4, x6, x8) Eadd(x14, x16) -> x4 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 11: eval_1(x4, x6, x8) Emult(x14, x16) -> x8 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 12: eval_1(x4, x6, x8) Ediv(x14, x16) -> cond_eval_e_1(x6 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16)) 13: eval_1(x4, x6, x8) Econst(x14) -> x14 14: eval(x4, x6, x8) Eadd(x14, x16) -> x4 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 15: eval(x4, x6, x8) Emult(x14, x16) -> x8 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 16: eval(x4, x6, x8) Ediv(x14, x16) -> cond_eval_e_1(x6 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16)) 17: eval(x4, x6, x8) Econst(x14) -> x14 18: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 19: main_4(x20, x10, x14) x18 -> eval(x10, x14, x18) x20 22: mult_n(x4, 0()) x10 -> 0() 23: mult_n(x4, S(x12)) x10 -> S(x4 (mult(x4) x12 x10) x10) 24: mult_1(x2) x4 -> mult_n(x2, x4) 25: mult(x4) x8 -> mult_n(x4, x8) 26: main_3(x20, x10) x14 -> eval(x10, x14, mult(x10)) x20 27: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 30: cond_div_mod_n_m(Pair(0(), x12), x2, x4, x6) -> Triple(0(), x6, x12) 31: cond_div_mod_n_m(Pair(S(x14), x12), x2, x4, x6) -> cond_div_mod_n_m_2(div_mod(x2, x4) S(x14) x12, x4 , x12) 32: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 33: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 34: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 35: main_2(x20, x63) x10 -> eval(x10, div_mod(x63, x10), mult(x10)) x20 38: plus_n(x4) 0() -> x4 39: plus_n(x4) S(x8) -> S(plus() x4 x8) 40: plus_1() x2 -> plus_n(x2) 41: plus() x4 -> plus_n(x4) 42: main_1(x20) x23 -> eval(plus(), div_mod(x23, plus()), mult(plus())) x20 43: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 49: minus'_m(0()) x8 -> 0() 50: minus'_m(S(x10)) 0() -> S(x10) 51: minus'_m(S(x10)) S(x12) -> minus'() x10 x12 52: minus'_1() x3 -> minus'_m(x3) 53: minus'() x6 -> minus'_m(x6) 54: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 55: minus() x1 -> minus_n(x1) 56: main(x20) -> eval(plus(), div_mod(minus(), plus()), mult(plus())) x20 where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: NeededRules + Details: none * Step 12: CFA MAYBE + Considered Problem: 1: main_6(x0) x6 -> x6 x0 2: main_7(x5) x6 -> x5 x6 3: main_5(x12) x10 -> x10 x12 4: eval1_e(x5) x6 -> x6 x5 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 6: eval_1(x4, x6, x8) Eadd(x14, x16) -> x4 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 7: eval_1(x4, x6, x8) Emult(x14, x16) -> x8 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 8: eval_1(x4, x6, x8) Ediv(x14, x16) -> cond_eval_e_1(x6 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16)) 9: eval_1(x4, x6, x8) Econst(x14) -> x14 10: eval(x4, x6, x8) Eadd(x14, x16) -> x4 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 11: eval(x4, x6, x8) Emult(x14, x16) -> x8 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16) 12: eval(x4, x6, x8) Ediv(x14, x16) -> cond_eval_e_1(x6 (eval(x4, x6, x8) x14) (eval(x4, x6, x8) x16)) 13: eval(x4, x6, x8) Econst(x14) -> x14 14: eval1(x5, x7, x9) x10 -> eval(x5, x7, x9) x10 15: main_4(x20, x10, x14) x18 -> eval(x10, x14, x18) x20 16: mult_n(x4, 0()) x10 -> 0() 17: mult_n(x4, S(x12)) x10 -> S(x4 (mult(x4) x12 x10) x10) 18: mult_1(x2) x4 -> mult_n(x2, x4) 19: mult(x4) x8 -> mult_n(x4, x8) 20: main_3(x20, x10) x14 -> eval(x10, x14, mult(x10)) x20 21: cond_div_mod_n_m_2(Triple(x8, x9, x10), x2, x6) -> Triple(x2 S(0()) x8, x9, x6) 22: cond_div_mod_n_m(Pair(0(), x12), x2, x4, x6) -> Triple(0(), x6, x12) 23: cond_div_mod_n_m(Pair(S(x14), x12), x2, x4, x6) -> cond_div_mod_n_m_2(div_mod(x2, x4) S(x14) x12, x4 , x12) 24: div_mod_n(x1, x2, x3) x4 -> cond_div_mod_n_m(x1 x3 x4, x1, x2, x3) 25: div_mod_1(x1, x2) x3 -> div_mod_n(x1, x2, x3) 26: div_mod(x2, x4) x6 -> div_mod_n(x2, x4, x6) 27: main_2(x20, x63) x10 -> eval(x10, div_mod(x63, x10), mult(x10)) x20 28: plus_n(x4) 0() -> x4 29: plus_n(x4) S(x8) -> S(plus() x4 x8) 30: plus_1() x2 -> plus_n(x2) 31: plus() x4 -> plus_n(x4) 32: main_1(x20) x23 -> eval(plus(), div_mod(x23, plus()), mult(plus())) x20 33: minus_n_m(x1, x2) x3 -> Pair(x3 x1 x2, x2) 34: minus'_m(0()) x8 -> 0() 35: minus'_m(S(x10)) 0() -> S(x10) 36: minus'_m(S(x10)) S(x12) -> minus'() x10 x12 37: minus'_1() x3 -> minus'_m(x3) 38: minus'() x6 -> minus'_m(x6) 39: minus_n(x2) x4 -> Pair(minus'() x2 x4, x4) 40: minus() x1 -> minus_n(x1) 41: main(x20) -> eval(plus(), div_mod(minus(), plus()), mult(plus())) x20 where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple eval1_e :: exp -> (exp -> nat) -> nat eval1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus'_m :: nat -> nat -> nat minus_n_m :: nat -> nat -> (nat -> nat -> nat) -> (nat,nat) pair minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat div_mod_1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval_1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main_1 :: exp -> (nat -> nat -> (nat,nat) pair) -> nat minus'_1 :: nat -> nat -> nat mult_1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus_1 :: nat -> nat -> nat main_2 :: exp -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat main_3 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> nat main_4 :: exp -> (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> nat main_5 :: exp -> (exp -> nat) -> nat main_6 :: exp -> (exp -> nat) -> nat main_7 :: (exp -> nat) -> exp -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> Pair(X{*},X{*}) | S(X{*}) | S(X{*}) | S(X{*}) | 0() | S(X{*}) | 0() | 0() | Pair(X{*},X{*}) | S(X{*}) | S(X{*}) | 0() | S(X{*}) | S(X{*}) | Pair(X{*},X{*}) | 0() | Triple(X{*},X{*},X{*}) | 0() | Pair(X{*},X{*}) | 0() | S(X{*}) | Triple(X{*},X{*},X{*}) | Triple(X{*},X{*},X{*}) | S(X{*}) | S(X{*}) | 0() | 0() | Econst(X{*}) | Ediv(X{*},X{*}) | Emult(X{*},X{*}) | Eadd(X{*},X{*}) | Econst(X{*}) | Ediv(X{*},X{*}) | Emult(X{*},X{*}) | Eadd(X{*},X{*}) | Triple(X{*},X{*},X{*}) ,V{x1_24} -> V{x2_26} ,V{x1_40} -> V{x3_24} ,V{x2_21} -> V{x4_23} ,V{x2_22} -> V{x1_24} ,V{x2_23} -> V{x1_24} ,V{x2_24} -> V{x4_26} ,V{x2_26} -> V{x2_23} | minus() ,V{x2_39} -> V{x1_40} ,V{x3_24} -> V{x6_26} ,V{x4_10} -> V{x4_12} | V{x4_11} | V{x4_10} | plus() ,V{x4_11} -> V{x4_12} | V{x4_11} | V{x4_10} | plus() ,V{x4_12} -> V{x4_12} | V{x4_11} | V{x4_10} | plus() ,V{x4_13} -> V{x4_12} | V{x4_11} | V{x4_10} | plus() ,V{x4_16} -> V{x4_19} ,V{x4_17} -> V{x4_19} ,V{x4_19} -> V{x4_17} | plus() ,V{x4_22} -> V{x2_24} ,V{x4_23} -> V{x2_24} ,V{x4_24} -> V{x12_23} | R{10} | R{11} | R{12} | R{13} ,V{x4_26} -> V{x4_23} | plus() ,V{x4_28} -> V{x4_31} ,V{x4_29} -> V{x4_31} ,V{x4_31} -> S(0()) | R{17} | R{16} | R{11} | R{12} | V{x4_29} | R{10} | R{13} ,V{x4_39} -> V{x4_24} ,V{x6_10} -> V{x6_12} | V{x6_11} | V{x6_10} | div_mod(minus(),plus()) ,V{x6_11} -> V{x6_12} | V{x6_11} | V{x6_10} | div_mod(minus(),plus()) ,V{x6_12} -> V{x6_12} | V{x6_11} | V{x6_10} | div_mod(minus(),plus()) ,V{x6_13} -> V{x6_12} | V{x6_11} | V{x6_10} | div_mod(minus(),plus()) ,V{x6_21} -> V{x12_23} ,V{x6_22} -> V{x3_24} ,V{x6_23} -> V{x3_24} ,V{x6_26} -> S(V{x14_23}) | R{11} | R{12} | R{10} | R{13} ,V{x6_38} -> V{x10_36} | V{x2_39} ,V{x8_10} -> V{x8_12} | V{x8_11} | V{x8_10} | mult(plus()) ,V{x8_11} -> V{x8_12} | V{x8_11} | V{x8_10} | mult(plus()) ,V{x8_12} -> V{x8_12} | V{x8_11} | V{x8_10} | mult(plus()) ,V{x8_13} -> V{x8_12} | V{x8_11} | V{x8_10} | mult(plus()) ,V{x8_19} -> V{x12_17} | R{12} | R{11} | R{10} | R{13} ,V{x8_21} -> R{29} | R{28} | @(@(V{x2_21},S(0())),V{x8_21}) | @(R{31},V{x8_21}) | 0() ,V{x8_29} -> 0() | @(R{31},V{x10_17}) | @(@(V{x4_17},R{16}),V{x10_17}) | @(@(V{x4_17},R{17}),V{x10_17}) | R{29} | R{28} | @(@(V{x4_17},@(R{19},V{x10_17})),V{x10_17}) | @(@(V{x4_17},@(@(mult(V{x4_17}),V{x12_17}),V{x10_17})),V{x10_17}) | @(R{31},V{x8_29}) | @(@(plus(),V{x4_29}),V{x8_29}) | X{*} ,V{x8_34} -> V{x12_36} | V{x4_39} ,V{x9_5} -> R{29} | R{28} | @(R{31},V{x8_21}) | @(@(V{x2_21},S(0())),V{x8_21}) | 0() ,V{x9_21} -> V{x9_21} | V{x6_22} ,V{x10_5} -> V{x9_21} | V{x6_22} ,V{x10_16} -> V{x10_17} | R{12} | R{10} | R{11} | R{13} ,V{x10_17} -> V{x10_17} | R{12} | R{10} | R{11} | R{13} ,V{x10_21} -> V{x6_21} | V{x12_22} ,V{x10_35} -> 0() | V{x14_23} | X{*} | @(@(plus(),V{x4_29}),V{x8_29}) | @(R{31},V{x8_29}) | @(@(V{x4_17},@(@(mult(V{x4_17}),V{x12_17}),V{x10_17})),V{x10_17}) | @(@(V{x4_17},@(R{19},V{x10_17})),V{x10_17}) | @(@(V{x4_17},R{16}),V{x10_17}) | @(@(V{x4_17},R{17}),V{x10_17}) | @(R{31},V{x10_17}) | R{28} | R{29} ,V{x10_36} -> 0() | V{x14_23} | X{*} | @(@(plus(),V{x4_29}),V{x8_29}) | @(R{31},V{x8_29}) | @(@(V{x4_17},@(@(mult(V{x4_17}),V{x12_17}),V{x10_17})),V{x10_17}) | @(@(V{x4_17},@(R{19},V{x10_17})),V{x10_17}) | @(@(V{x4_17},R{16}),V{x10_17}) | @(@(V{x4_17},R{17}),V{x10_17}) | @(R{31},V{x10_17}) | R{28} | R{29} ,V{x11_5} -> V{x6_21} | V{x12_22} ,V{x12_17} -> 0() | @(R{31},V{x10_17}) | @(@(V{x4_17},R{16}),V{x10_17}) | @(@(V{x4_17},R{17}),V{x10_17}) | R{29} | R{28} | @(@(V{x4_17},@(R{19},V{x10_17})),V{x10_17}) | @(@(V{x4_17},@(@(mult(V{x4_17}),V{x12_17}),V{x10_17})),V{x10_17}) | @(R{31},V{x8_29}) | X{*} | @(@(plus(),V{x4_29}),V{x8_29}) ,V{x12_22} -> V{x4_39} ,V{x12_23} -> V{x4_39} ,V{x12_36} -> 0() | X{*} | @(@(V{x4_17},@(@(mult(V{x4_17}),V{x12_17}),V{x10_17})),V{x10_17}) | @(@(V{x4_17},@(R{19},V{x10_17})),V{x10_17}) | @(@(V{x4_17},R{16}),V{x10_17}) | @(@(V{x4_17},R{17}),V{x10_17}) | @(R{31},V{x10_17}) | @(@(plus(),V{x4_29}),V{x8_29}) | @(R{31},V{x8_29}) | R{28} | R{29} ,V{x14_10} -> X{*} ,V{x14_11} -> X{*} ,V{x14_12} -> X{*} ,V{x14_13} -> X{*} ,V{x14_23} -> V{x10_35} ,V{x16_10} -> X{*} ,V{x16_11} -> X{*} ,V{x16_12} -> X{*} ,V{x20_41} -> X{*} ,R{0} -> R{41} | main(X{*}) ,R{5} -> V{x9_5} ,R{10} -> R{29} | R{28} | @(R{31},R{13}) | @(R{31},R{12}) | @(R{31},R{11}) | @(R{31},R{10}) | @(R{31},@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x16_10})) | @(@(V{x4_10},R{13}),R{10}) | @(@(V{x4_10},R{12}),R{10}) | @(@(V{x4_10},R{11}),R{10}) | @(@(V{x4_10},R{10}),R{10}) | @(@(V{x4_10},R{13}),R{11}) | @(@(V{x4_10},R{12}),R{11}) | @(@(V{x4_10},R{11}),R{11}) | @(@(V{x4_10},R{10}),R{11}) | @(@(V{x4_10},R{13}),R{12}) | @(@(V{x4_10},R{12}),R{12}) | @(@(V{x4_10},R{11}),R{12}) | @(@(V{x4_10},R{10}),R{12}) | @(@(V{x4_10},R{13}),R{13}) | @(@(V{x4_10},R{12}),R{13}) | @(@(V{x4_10},R{11}),R{13}) | @(@(V{x4_10},R{10}),R{13}) | @(@(V{x4_10},@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x14_10})),R{13}) | @(@(V{x4_10},@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x14_10})),R{12}) | @(@(V{x4_10},@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x14_10})),R{11}) | @(@(V{x4_10},@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x14_10})),R{10}) | @(@(V{x4_10},R{13}),@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x16_10})) | @(@(V{x4_10},R{12}),@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x16_10})) | @(@(V{x4_10},R{11}),@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x16_10})) | @(@(V{x4_10},R{10}),@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x16_10})) | @(@(V{x4_10},@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x14_10})) ,@(eval(V{x4_10},V{x6_10},V{x8_10}),V{x16_10})) ,R{11} -> R{17} | R{16} | @(R{19},R{13}) | @(R{19},R{12}) | @(R{19},R{11}) | @(R{19},R{10}) | @(R{19},@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x16_11})) | @(@(V{x8_11},R{13}),R{10}) | @(@(V{x8_11},R{12}),R{10}) | @(@(V{x8_11},R{11}),R{10}) | @(@(V{x8_11},R{10}),R{10}) | @(@(V{x8_11},R{13}),R{11}) | @(@(V{x8_11},R{12}),R{11}) | @(@(V{x8_11},R{11}),R{11}) | @(@(V{x8_11},R{10}),R{11}) | @(@(V{x8_11},R{13}),R{12}) | @(@(V{x8_11},R{12}),R{12}) | @(@(V{x8_11},R{11}),R{12}) | @(@(V{x8_11},R{10}),R{12}) | @(@(V{x8_11},R{13}),R{13}) | @(@(V{x8_11},R{12}),R{13}) | @(@(V{x8_11},R{11}),R{13}) | @(@(V{x8_11},R{10}),R{13}) | @(@(V{x8_11},@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x14_11})),R{13}) | @(@(V{x8_11},@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x14_11})),R{12}) | @(@(V{x8_11},@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x14_11})),R{11}) | @(@(V{x8_11},@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x14_11})),R{10}) | @(@(V{x8_11},R{13}),@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x16_11})) | @(@(V{x8_11},R{12}),@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x16_11})) | @(@(V{x8_11},R{11}),@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x16_11})) | @(@(V{x8_11},R{10}),@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x16_11})) | @(@(V{x8_11},@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x14_11})) ,@(eval(V{x4_11},V{x6_11},V{x8_11}),V{x16_11})) ,R{12} -> R{5} | cond_eval_e_1(R{24}) | cond_eval_e_1(@(R{26},R{13})) | cond_eval_e_1(@(R{26},R{12})) | cond_eval_e_1(@(R{26},R{11})) | cond_eval_e_1(@(R{26},R{10})) | cond_eval_e_1(@(R{26},@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x16_12}))) | cond_eval_e_1(@(@(V{x6_12},R{13}),R{10})) | cond_eval_e_1(@(@(V{x6_12},R{12}),R{10})) | cond_eval_e_1(@(@(V{x6_12},R{11}),R{10})) | cond_eval_e_1(@(@(V{x6_12},R{10}),R{10})) | cond_eval_e_1(@(@(V{x6_12},R{13}),R{11})) | cond_eval_e_1(@(@(V{x6_12},R{12}),R{11})) | cond_eval_e_1(@(@(V{x6_12},R{11}),R{11})) | cond_eval_e_1(@(@(V{x6_12},R{10}),R{11})) | cond_eval_e_1(@(@(V{x6_12},R{13}),R{12})) | cond_eval_e_1(@(@(V{x6_12},R{12}),R{12})) | cond_eval_e_1(@(@(V{x6_12},R{11}),R{12})) | cond_eval_e_1(@(@(V{x6_12},R{10}),R{12})) | cond_eval_e_1(@(@(V{x6_12},R{13}),R{13})) | cond_eval_e_1(@(@(V{x6_12},R{12}),R{13})) | cond_eval_e_1(@(@(V{x6_12},R{11}),R{13})) | cond_eval_e_1(@(@(V{x6_12},R{10}),R{13})) | cond_eval_e_1(@(@(V{x6_12},@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x14_12})),R{13})) | cond_eval_e_1(@(@(V{x6_12},@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x14_12})),R{12})) | cond_eval_e_1(@(@(V{x6_12},@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x14_12})),R{11})) | cond_eval_e_1(@(@(V{x6_12},@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x14_12})),R{10})) | cond_eval_e_1(@(@(V{x6_12},R{13}),@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x16_12}))) | cond_eval_e_1(@(@(V{x6_12},R{12}),@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x16_12}))) | cond_eval_e_1(@(@(V{x6_12},R{11}),@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x16_12}))) | cond_eval_e_1(@(@(V{x6_12},R{10}),@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x16_12}))) | cond_eval_e_1(@(@(V{x6_12},@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x14_12})) ,@(eval(V{x4_12},V{x6_12},V{x8_12}),V{x16_12}))) ,R{13} -> V{x14_13} ,R{16} -> 0() ,R{17} -> S(R{29}) | S(R{28}) | S(@(R{31},V{x10_17})) | S(@(@(V{x4_17},R{17}),V{x10_17})) | S(@(@(V{x4_17},R{16}),V{x10_17})) | S(@(@(V{x4_17},@(R{19},V{x10_17})),V{x10_17})) | S(@(@(V{x4_17},@(@(mult(V{x4_17}),V{x12_17}),V{x10_17})),V{x10_17})) ,R{19} -> mult_n(V{x4_19},V{x8_19}) ,R{21} -> Triple(R{29},V{x9_21},V{x6_21}) | Triple(R{28},V{x9_21},V{x6_21}) | Triple(@(R{31},V{x8_21}),V{x9_21},V{x6_21}) | Triple(@(@(V{x2_21},S(0())),V{x8_21}),V{x9_21},V{x6_21}) ,R{22} -> Triple(0(),V{x6_22},V{x12_22}) ,R{23} -> R{21} | cond_div_mod_n_m_2(R{24},V{x4_23},V{x12_23}) | cond_div_mod_n_m_2(@(R{26},V{x12_23}),V{x4_23},V{x12_23}) | cond_div_mod_n_m_2(@(@(div_mod(V{x2_23},V{x4_23}),S(V{x14_23})),V{x12_23}),V{x4_23},V{x12_23}) ,R{24} -> R{23} | R{22} | cond_div_mod_n_m(R{39},V{x1_24},V{x2_24},V{x3_24}) | cond_div_mod_n_m(@(R{40},V{x4_24}),V{x1_24},V{x2_24},V{x3_24}) | cond_div_mod_n_m(@(@(V{x1_24},V{x3_24}),V{x4_24}),V{x1_24},V{x2_24},V{x3_24}) ,R{26} -> div_mod_n(V{x2_26},V{x4_26},V{x6_26}) ,R{28} -> V{x4_28} ,R{29} -> S(R{29}) | S(R{28}) | S(@(R{31},V{x8_29})) | S(@(@(plus(),V{x4_29}),V{x8_29})) ,R{31} -> plus_n(V{x4_31}) ,R{34} -> 0() ,R{35} -> S(V{x10_35}) ,R{36} -> R{36} | R{35} | R{34} | @(R{38},V{x12_36}) | @(@(minus'(),V{x10_36}),V{x12_36}) ,R{38} -> minus'_m(V{x6_38}) ,R{39} -> Pair(R{36},V{x4_39}) | Pair(R{35},V{x4_39}) | Pair(R{34},V{x4_39}) | Pair(@(R{38},V{x4_39}),V{x4_39}) | Pair(@(@(minus'(),V{x2_39}),V{x4_39}),V{x4_39}) ,R{40} -> minus_n(V{x1_40}) ,R{41} -> R{13} | R{12} | R{11} | R{10} | @(eval(plus(),div_mod(minus(),plus()),mult(plus())),V{x20_41})} * Step 13: UncurryATRS MAYBE + Considered Problem: 5: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 10: eval(plus(), div_mod(minus(), plus()), mult(plus())) Eadd(x2, x1) -> plus() (eval(plus() , div_mod(minus(), plus()) , mult(plus())) x2) (eval(plus(), div_mod(minus(), plus()), mult(plus())) x1) 11: eval(plus(), div_mod(minus(), plus()), mult(plus())) Emult(x2, x1) -> mult(plus()) (eval(plus() , div_mod(minus() , plus()) , mult(plus())) x2) (eval(plus(), div_mod(minus(), plus()), mult(plus())) x1) 12: eval(plus(), div_mod(minus(), plus()), mult(plus())) Ediv(x2, x1) -> cond_eval_e_1(div_mod(minus() , plus()) (eval(plus(), div_mod(minus(), plus()), mult(plus())) x2) (eval(plus(), div_mod(minus(), plus()) , mult(plus())) x1)) 13: eval(plus(), div_mod(minus(), plus()), mult(plus())) Econst(x1) -> x1 16: mult_n(plus(), 0()) x1 -> 0() 17: mult_n(plus(), S(x2)) x1 -> S(plus() (mult(plus()) x2 x1) x1) 19: mult(plus()) x1 -> mult_n(plus(), x1) 21: cond_div_mod_n_m_2(Triple(x4, x3, x2), plus(), x1) -> Triple(plus() S(0()) x4, x3, x1) 22: cond_div_mod_n_m(Pair(0(), x2), minus(), plus(), x1) -> Triple(0(), x1, x2) 23: cond_div_mod_n_m(Pair(S(x3), x2), minus(), plus(), x1) -> cond_div_mod_n_m_2(div_mod(minus(), plus()) S(x3) x2, plus(), x2) 24: div_mod_n(minus(), plus(), x2) x1 -> cond_div_mod_n_m(minus() x2 x1, minus(), plus(), x2) 26: div_mod(minus(), plus()) x1 -> div_mod_n(minus(), plus(), x1) 28: plus_n(x4) 0() -> x4 29: plus_n(x2) S(x1) -> S(plus() x2 x1) 31: plus() x4 -> plus_n(x4) 34: minus'_m(0()) x8 -> 0() 35: minus'_m(S(x10)) 0() -> S(x10) 36: minus'_m(S(x2)) S(x1) -> minus'() x2 x1 38: minus'() x6 -> minus'_m(x6) 39: minus_n(x2) x1 -> Pair(minus'() x2 x1, x1) 40: minus() x1 -> minus_n(x1) 41: main(x20) -> eval(plus(), div_mod(minus(), plus()), mult(plus())) x20 where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple minus'_m :: nat -> nat -> nat minus :: nat -> nat -> (nat,nat) pair div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple minus_n :: nat -> nat -> (nat,nat) pair mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat plus_n :: nat -> nat -> nat cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat minus' :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat main :: exp -> nat + Applied Processor: UncurryATRS + Details: none * Step 14: UsableRules MAYBE + Considered Problem: 1: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 2: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Eadd(x2, x1)) -> plus#2(eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 3: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Emult(x2, x1)) -> mult#2(plus(), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 4: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Ediv(x2, x1)) -> cond_eval_e_1(div_mod#2(minus() , plus() , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1))) 5: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Econst(x1)) -> x1 6: mult_n#1(plus(), 0(), x1) -> 0() 7: mult_n#1(plus(), S(x2), x1) -> S(plus#2(mult#2(plus(), x2, x1), x1)) 8: mult#1(plus(), x1) -> mult_n(plus(), x1) 9: mult#2(plus(), x1, x2) -> mult_n#1(plus(), x1, x2) 10: cond_div_mod_n_m_2(Triple(x4, x3, x2), plus(), x1) -> Triple(plus#2(S(0()), x4), x3, x1) 11: cond_div_mod_n_m(Pair(0(), x2), minus(), plus(), x1) -> Triple(0(), x1, x2) 12: cond_div_mod_n_m(Pair(S(x3), x2), minus(), plus(), x1) -> cond_div_mod_n_m_2(div_mod#2(minus(), plus() , S(x3) , x2), plus(), x2) 13: div_mod_n#1(minus(), plus(), x2, x1) -> cond_div_mod_n_m(minus#2(x2, x1), minus(), plus(), x2) 14: div_mod#1(minus(), plus(), x1) -> div_mod_n(minus(), plus(), x1) 15: div_mod#2(minus(), plus(), x1, x2) -> div_mod_n#1(minus(), plus(), x1, x2) 16: plus_n#1(x4, 0()) -> x4 17: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 18: plus#1(x4) -> plus_n(x4) 19: plus#2(x4, x5) -> plus_n#1(x4, x5) 20: minus'_m#1(0(), x8) -> 0() 21: minus'_m#1(S(x10), 0()) -> S(x10) 22: minus'_m#1(S(x2), S(x1)) -> minus'#2(x2, x1) 23: minus'#1(x6) -> minus'_m(x6) 24: minus'#2(x6, x7) -> minus'_m#1(x6, x7) 25: minus_n#1(x2, x1) -> Pair(minus'#2(x2, x1), x1) 26: minus#1(x1) -> minus_n(x1) 27: minus#2(x1, x2) -> minus_n#1(x1, x2) 28: main(x20) -> eval#1(plus(), div_mod(minus(), plus()), mult(plus()), x20) where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod#1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod#2 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod_n :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod_n#1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval#1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main :: exp -> nat minus :: nat -> nat -> (nat,nat) pair minus#1 :: nat -> nat -> (nat,nat) pair minus#2 :: nat -> nat -> (nat,nat) pair minus'#1 :: nat -> nat -> nat minus'#2 :: nat -> nat -> nat minus'_m :: nat -> nat -> nat minus'_m#1 :: nat -> nat -> nat minus_n :: nat -> nat -> (nat,nat) pair minus_n#1 :: nat -> nat -> (nat,nat) pair mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#1 :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_n :: (nat -> nat -> nat) -> nat -> nat -> nat mult_n#1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#1 :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_n :: nat -> nat -> nat plus_n#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 15: Inline MAYBE + Considered Problem: 1: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 2: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Eadd(x2, x1)) -> plus#2(eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 3: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Emult(x2, x1)) -> mult#2(plus(), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 4: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Ediv(x2, x1)) -> cond_eval_e_1(div_mod#2(minus() , plus() , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1))) 5: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Econst(x1)) -> x1 6: mult_n#1(plus(), 0(), x1) -> 0() 7: mult_n#1(plus(), S(x2), x1) -> S(plus#2(mult#2(plus(), x2, x1), x1)) 9: mult#2(plus(), x1, x2) -> mult_n#1(plus(), x1, x2) 10: cond_div_mod_n_m_2(Triple(x4, x3, x2), plus(), x1) -> Triple(plus#2(S(0()), x4), x3, x1) 11: cond_div_mod_n_m(Pair(0(), x2), minus(), plus(), x1) -> Triple(0(), x1, x2) 12: cond_div_mod_n_m(Pair(S(x3), x2), minus(), plus(), x1) -> cond_div_mod_n_m_2(div_mod#2(minus(), plus() , S(x3) , x2), plus(), x2) 13: div_mod_n#1(minus(), plus(), x2, x1) -> cond_div_mod_n_m(minus#2(x2, x1), minus(), plus(), x2) 15: div_mod#2(minus(), plus(), x1, x2) -> div_mod_n#1(minus(), plus(), x1, x2) 16: plus_n#1(x4, 0()) -> x4 17: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 19: plus#2(x4, x5) -> plus_n#1(x4, x5) 20: minus'_m#1(0(), x8) -> 0() 21: minus'_m#1(S(x10), 0()) -> S(x10) 22: minus'_m#1(S(x2), S(x1)) -> minus'#2(x2, x1) 24: minus'#2(x6, x7) -> minus'_m#1(x6, x7) 25: minus_n#1(x2, x1) -> Pair(minus'#2(x2, x1), x1) 27: minus#2(x1, x2) -> minus_n#1(x1, x2) 28: main(x20) -> eval#1(plus(), div_mod(minus(), plus()), mult(plus()), x20) where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod#2 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod_n#1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval#1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main :: exp -> nat minus :: nat -> nat -> (nat,nat) pair minus#2 :: nat -> nat -> (nat,nat) pair minus'#2 :: nat -> nat -> nat minus'_m#1 :: nat -> nat -> nat minus_n#1 :: nat -> nat -> (nat,nat) pair mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_n#1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_n#1 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 16: UsableRules MAYBE + Considered Problem: 1: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 2: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Eadd(x2, x1)) -> plus#2(eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 3: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Emult(x2, x1)) -> mult#2(plus(), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 4: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Ediv(x2, x1)) -> cond_eval_e_1(div_mod#2(minus() , plus() , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1))) 5: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Econst(x1)) -> x1 6: mult_n#1(plus(), 0(), x1) -> 0() 7: mult_n#1(plus(), S(x2), x1) -> S(plus#2(mult#2(plus(), x2, x1), x1)) 8: mult#2(plus(), 0(), x2) -> 0() 9: mult#2(plus(), S(x4), x2) -> S(plus#2(mult#2(plus(), x4, x2), x2)) 10: cond_div_mod_n_m_2(Triple(x4, x3, x2), plus(), x1) -> Triple(plus#2(S(0()), x4), x3, x1) 11: cond_div_mod_n_m(Pair(0(), x2), minus(), plus(), x1) -> Triple(0(), x1, x2) 12: cond_div_mod_n_m(Pair(S(x3), x2), minus(), plus(), x1) -> cond_div_mod_n_m_2(div_mod#2(minus(), plus() , S(x3) , x2), plus(), x2) 13: div_mod_n#1(minus(), plus(), x2, x4) -> cond_div_mod_n_m(minus_n#1(x2, x4), minus(), plus(), x2) 14: div_mod#2(minus(), plus(), x4, x2) -> cond_div_mod_n_m(minus#2(x4, x2), minus(), plus(), x4) 15: plus_n#1(x4, 0()) -> x4 16: plus_n#1(x2, S(x1)) -> S(plus#2(x2, x1)) 17: plus#2(x8, 0()) -> x8 18: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 19: minus'_m#1(0(), x8) -> 0() 20: minus'_m#1(S(x10), 0()) -> S(x10) 21: minus'_m#1(S(x2), S(x1)) -> minus'#2(x2, x1) 22: minus'#2(0(), x16) -> 0() 23: minus'#2(S(x20), 0()) -> S(x20) 24: minus'#2(S(x4), S(x2)) -> minus'#2(x4, x2) 25: minus_n#1(x2, x1) -> Pair(minus'#2(x2, x1), x1) 26: minus#2(x4, x2) -> Pair(minus'#2(x4, x2), x2) 27: main(x20) -> eval#1(plus(), div_mod(minus(), plus()), mult(plus()), x20) where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod#2 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod_n#1 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval#1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main :: exp -> nat minus :: nat -> nat -> (nat,nat) pair minus#2 :: nat -> nat -> (nat,nat) pair minus'#2 :: nat -> nat -> nat minus'_m#1 :: nat -> nat -> nat minus_n#1 :: nat -> nat -> (nat,nat) pair mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat mult_n#1 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat plus_n#1 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 17: Inline MAYBE + Considered Problem: 1: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 2: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Eadd(x2, x1)) -> plus#2(eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 3: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Emult(x2, x1)) -> mult#2(plus(), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 4: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Ediv(x2, x1)) -> cond_eval_e_1(div_mod#2(minus() , plus() , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1))) 5: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Econst(x1)) -> x1 8: mult#2(plus(), 0(), x2) -> 0() 9: mult#2(plus(), S(x4), x2) -> S(plus#2(mult#2(plus(), x4, x2), x2)) 10: cond_div_mod_n_m_2(Triple(x4, x3, x2), plus(), x1) -> Triple(plus#2(S(0()), x4), x3, x1) 11: cond_div_mod_n_m(Pair(0(), x2), minus(), plus(), x1) -> Triple(0(), x1, x2) 12: cond_div_mod_n_m(Pair(S(x3), x2), minus(), plus(), x1) -> cond_div_mod_n_m_2(div_mod#2(minus(), plus() , S(x3) , x2), plus(), x2) 14: div_mod#2(minus(), plus(), x4, x2) -> cond_div_mod_n_m(minus#2(x4, x2), minus(), plus(), x4) 17: plus#2(x8, 0()) -> x8 18: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 22: minus'#2(0(), x16) -> 0() 23: minus'#2(S(x20), 0()) -> S(x20) 24: minus'#2(S(x4), S(x2)) -> minus'#2(x4, x2) 26: minus#2(x4, x2) -> Pair(minus'#2(x4, x2), x2) 27: main(x20) -> eval#1(plus(), div_mod(minus(), plus()), mult(plus()), x20) where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod#2 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval#1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main :: exp -> nat minus :: nat -> nat -> (nat,nat) pair minus#2 :: nat -> nat -> (nat,nat) pair minus'#2 :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 18: UsableRules MAYBE + Considered Problem: 1: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 2: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Eadd(x2, x1)) -> plus#2(eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 3: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Emult(x2, x1)) -> mult#2(plus(), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 4: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Ediv(x2, x1)) -> cond_eval_e_1(div_mod#2(minus() , plus() , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1))) 5: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Econst(x1)) -> x1 6: mult#2(plus(), 0(), x2) -> 0() 7: mult#2(plus(), S(x4), x2) -> S(plus#2(mult#2(plus(), x4, x2), x2)) 8: cond_div_mod_n_m_2(Triple(x4, x3, x2), plus(), x1) -> Triple(plus#2(S(0()), x4), x3, x1) 9: cond_div_mod_n_m(Pair(0(), x2), minus(), plus(), x1) -> Triple(0(), x1, x2) 10: cond_div_mod_n_m(Pair(S(x3), x2), minus(), plus(), x1) -> cond_div_mod_n_m_2(div_mod#2(minus(), plus() , S(x3) , x2), plus(), x2) 11: div_mod#2(minus(), plus(), x8, x4) -> cond_div_mod_n_m(Pair(minus'#2(x8, x4), x4), minus(), plus(), x8) 12: plus#2(x8, 0()) -> x8 13: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 14: minus'#2(0(), x16) -> 0() 15: minus'#2(S(x20), 0()) -> S(x20) 16: minus'#2(S(x4), S(x2)) -> minus'#2(x4, x2) 17: minus#2(x4, x2) -> Pair(minus'#2(x4, x2), x2) 18: main(x20) -> eval#1(plus(), div_mod(minus(), plus()), mult(plus()), x20) where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod#2 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval#1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main :: exp -> nat minus :: nat -> nat -> (nat,nat) pair minus#2 :: nat -> nat -> (nat,nat) pair minus'#2 :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 19: Compression MAYBE + Considered Problem: 1: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 2: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Eadd(x2, x1)) -> plus#2(eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 3: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Emult(x2, x1)) -> mult#2(plus(), eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1)) 4: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Ediv(x2, x1)) -> cond_eval_e_1(div_mod#2(minus() , plus() , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x2) , eval#1(plus() , div_mod(minus() , plus()) , mult(plus()) , x1))) 5: eval#1(plus(), div_mod(minus(), plus()), mult(plus()), Econst(x1)) -> x1 6: mult#2(plus(), 0(), x2) -> 0() 7: mult#2(plus(), S(x4), x2) -> S(plus#2(mult#2(plus(), x4, x2), x2)) 8: cond_div_mod_n_m_2(Triple(x4, x3, x2), plus(), x1) -> Triple(plus#2(S(0()), x4), x3, x1) 9: cond_div_mod_n_m(Pair(0(), x2), minus(), plus(), x1) -> Triple(0(), x1, x2) 10: cond_div_mod_n_m(Pair(S(x3), x2), minus(), plus(), x1) -> cond_div_mod_n_m_2(div_mod#2(minus(), plus() , S(x3) , x2), plus(), x2) 11: div_mod#2(minus(), plus(), x8, x4) -> cond_div_mod_n_m(Pair(minus'#2(x8, x4), x4), minus(), plus(), x8) 12: plus#2(x8, 0()) -> x8 13: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 14: minus'#2(0(), x16) -> 0() 15: minus'#2(S(x20), 0()) -> S(x20) 16: minus'#2(S(x4), S(x2)) -> minus'#2(x4, x2) 18: main(x20) -> eval#1(plus(), div_mod(minus(), plus()), mult(plus()), x20) where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple cond_div_mod_n_m :: (nat,nat) pair -> (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> (nat -> nat -> nat) -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat div_mod :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple div_mod#2 :: (nat -> nat -> (nat,nat) pair) -> (nat -> nat -> nat) -> nat -> nat -> (nat,nat,nat) triple eval#1 :: (nat -> nat -> nat) -> (nat -> nat -> (nat,nat,nat) triple) -> (nat -> nat -> nat) -> exp -> nat main :: exp -> nat minus :: nat -> nat -> (nat,nat) pair minus'#2 :: nat -> nat -> nat mult :: (nat -> nat -> nat) -> nat -> nat -> nat mult#2 :: (nat -> nat -> nat) -> nat -> nat -> nat plus :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: Compression + Details: none * Step 20: ToTctProblem MAYBE + Considered Problem: 1: cond_eval_e_1(Triple(x9, x10, x11)) -> x9 2: eval#1(Eadd(x2, x1)) -> plus#2(eval#1(x2), eval#1(x1)) 3: eval#1(Emult(x2, x1)) -> mult#2(eval#1(x2), eval#1(x1)) 4: eval#1(Ediv(x2, x1)) -> cond_eval_e_1(div_mod#2(eval#1(x2), eval#1(x1))) 5: eval#1(Econst(x1)) -> x1 6: mult#2(0(), x2) -> 0() 7: mult#2(S(x4), x2) -> S(plus#2(mult#2(x4, x2), x2)) 8: cond_div_mod_n_m_2(Triple(x4, x3, x2), x1) -> Triple(plus#2(S(0()), x4), x3, x1) 9: cond_div_mod_n_m(Pair(0(), x2), x1) -> Triple(0(), x1, x2) 10: cond_div_mod_n_m(Pair(S(x3), x2), x1) -> cond_div_mod_n_m_2(div_mod#2(S(x3), x2), x2) 11: div_mod#2(x8, x4) -> cond_div_mod_n_m(Pair(minus'#2(x8, x4), x4), x8) 12: plus#2(x8, 0()) -> x8 13: plus#2(x4, S(x2)) -> S(plus#2(x4, x2)) 14: minus'#2(0(), x16) -> 0() 15: minus'#2(S(x20), 0()) -> S(x20) 16: minus'#2(S(x4), S(x2)) -> minus'#2(x4, x2) 17: main(x20) -> eval#1(x20) where 0 :: nat Eadd :: exp -> exp -> exp Econst :: nat -> exp Ediv :: exp -> exp -> exp Emult :: exp -> exp -> exp Pair :: 'a -> 'b -> ('a,'b) pair S :: nat -> nat Triple :: 'a -> 'b -> 'c -> ('a,'b,'c) triple cond_div_mod_n_m :: (nat,nat) pair -> nat -> (nat,nat,nat) triple cond_div_mod_n_m_2 :: (nat,nat,nat) triple -> nat -> (nat,nat,nat) triple cond_eval_e_1 :: (nat,nat,nat) triple -> nat div_mod#2 :: nat -> nat -> (nat,nat,nat) triple eval#1 :: exp -> nat main :: exp -> nat minus'#2 :: nat -> nat -> nat mult#2 :: nat -> nat -> nat plus#2 :: nat -> nat -> nat + Applied Processor: ToTctProblem + Details: none * Step 21: Failure MAYBE + Considered Problem: - Strict TRS: cond_div_mod_n_m(Pair(0(),x2),x1) -> Triple(0(),x1,x2) cond_div_mod_n_m(Pair(S(x3),x2),x1) -> cond_div_mod_n_m_2(div_mod#2(S(x3),x2),x2) cond_div_mod_n_m_2(Triple(x4,x3,x2),x1) -> Triple(plus#2(S(0()),x4),x3,x1) cond_eval_e_1(Triple(x9,x10,x11)) -> x9 div_mod#2(x8,x4) -> cond_div_mod_n_m(Pair(minus'#2(x8,x4),x4),x8) eval#1(Eadd(x2,x1)) -> plus#2(eval#1(x2),eval#1(x1)) eval#1(Econst(x1)) -> x1 eval#1(Ediv(x2,x1)) -> cond_eval_e_1(div_mod#2(eval#1(x2),eval#1(x1))) eval#1(Emult(x2,x1)) -> mult#2(eval#1(x2),eval#1(x1)) main(x20) -> eval#1(x20) minus'#2(0(),x16) -> 0() minus'#2(S(x20),0()) -> S(x20) minus'#2(S(x4),S(x2)) -> minus'#2(x4,x2) mult#2(0(),x2) -> 0() mult#2(S(x4),x2) -> S(plus#2(mult#2(x4,x2),x2)) plus#2(x4,S(x2)) -> S(plus#2(x4,x2)) plus#2(x8,0()) -> x8 - Signature: {cond_div_mod_n_m/2,cond_div_mod_n_m_2/2,cond_eval_e_1/1,div_mod#2/2,eval#1/1,main/1,minus'#2/2,mult#2/2 ,plus#2/2} / {0/0,Eadd/2,Econst/1,Ediv/2,Emult/2,Pair/2,S/1,Triple/3} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,Eadd,Econst,Ediv,Emult,Pair,S ,Triple} + Applied Processor: EmptyProcessor + Details: The problem is still open. MAYBE