MAYBE * Step 1: Desugar MAYBE + Considered Problem: type 'a list = Nil | Cons of 'a * 'a list ;; type int = 0 | S of int | M of int ;; (* max : nat -> nat -> nat *) let rec max x y = match x with | 0 -> y | S(x') -> match y with | 0 -> x | S(y') -> S(max x' y') ;; (* plus : nat -> nat -> nat *) let rec plus x y = match x with | 0 -> y | S(x') -> S(plus x' y) ;; (* minus : nat -> nat -> nat *) let rec minus x y = match x with | 0 -> 0 | S(x') -> match y with | 0 -> x | S(y') -> minus x' y' ;; (* foldl: (nat -> nat -> nat) -> nat -> nat list -> nat *) let rec foldl f z xs = match xs with | Nil -> z | Cons(x,xs') -> foldl f (f z x) xs' ;; (* maxlist : int list -> int *) let maxlist = foldl max 0 ;; (* scanr: (nat -> nat -> nat) -> nat -> nat list -> nat list *) let rec scanr f z xs = match xs with | Nil -> Cons(z,Nil) | Cons(x,xs') -> match scanr f z xs' with | Nil -> error | Cons(y,ys) -> Cons(f x y, Cons(y,ys)) ;; let mms l = (* f x y == max 0 (plus x y) *) let rec f x y = match x with | 0 -> (match y with | 0 -> 0 | M(y') -> 0 | S(y') -> y) | M(x') -> (match y with | 0 -> 0 | M(y') -> 0 | S(y') -> minus y x') | S(x') -> (match y with | 0 -> x | M(y') -> minus x y' | S(y') -> plus x y) in maxlist (scanr f 0 l) ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization MAYBE + Considered Problem: λl : int list. (λmax : int -> int -> int. (λplus : int -> int -> int. (λminus : int -> int -> int. (λfoldl : (int -> int -> int) -> int -> int list -> int. (λmaxlist : int list -> int. (λscanr : (int -> int -> int) -> int -> int list -> int list. (λmms : int list -> int. mms l) (λl : int list. (λf : int -> int -> int. maxlist (scanr f 0 l)) (μf : int -> int -> int. λx : int. λy : int. case x of | 0 -> case y of | 0 -> 0 | M -> λy' : int. 0 | S -> λy' : int. y | M -> λx' : int. case y of | 0 -> 0 | M -> λy' : int. 0 | S -> λy' : int. minus y x' | S -> λx' : int. case y of | 0 -> x | M -> λy' : int. minus x y' | S -> λy' : int. plus x y))) (μscanr : (int -> int -> int) -> int -> int list -> int list. λf : int -> int -> int. λz : int. λxs : int list. case xs of | Nil -> Cons(z,Nil) | Cons -> λx : int. λxs' : int list. case scanr f z xs' of | Nil -> ⟘  | Cons -> λy : int. λys : int list. Cons(f x y,Cons(y,ys)))) (foldl max 0)) (μfoldl : (int -> int -> int) -> int -> int list -> int. λf : int -> int -> int. λz : int. λxs : int list. case xs of | Nil -> z | Cons -> λx : int. λxs' : int list. foldl f (f z x) xs')) (μminus : int -> int -> int. λx : int. λy : int. case x of | 0 -> 0 | S -> λx' : int. case y of | 0 -> x | S -> λy' : int. minus x' y')) (μplus : int -> int -> int. λx : int. λy : int. case x of | 0 -> y | S -> λx' : int. S(plus x' y))) (μmax : int -> int -> int. λx : int. λy : int. case x of | 0 -> y | S -> λx' : int. case y of | 0 -> x | S -> λy' : int. S(max x' y')) : int list -> int where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int + Applied Processor: Defunctionalization + Details: none * Step 3: Inline MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 3: cond_f_x_y_1(0(), x9) -> 0() 4: cond_f_x_y_1(M(x10), x9) -> 0() 5: cond_f_x_y_1(S(x10), x9) -> x9 6: cond_f_x_y_2(0(), x3, x9, x10) -> 0() 7: cond_f_x_y_2(M(x11), x3, x9, x10) -> 0() 8: cond_f_x_y_2(S(x11), x3, x9, x10) -> x3 x9 x10 9: cond_f_x_y_3(0(), x2, x3, x8, x9) -> x8 10: cond_f_x_y_3(M(x11), x2, x3, x8, x9) -> x3 x8 x11 11: cond_f_x_y_3(S(x11), x2, x3, x8, x9) -> x2 x8 x9 12: cond_f_x_y(0(), x2, x3, x8, x9) -> cond_f_x_y_1(x9, x9) 13: cond_f_x_y(M(x10), x2, x3, x8, x9) -> cond_f_x_y_2(x9, x3, x9, x10) 14: cond_f_x_y(S(x10), x2, x3, x8, x9) -> cond_f_x_y_3(x9, x2, x3, x8, x9) 15: f_x(x2, x3, x8) x9 -> cond_f_x_y(x8, x2, x3, x8, x9) 16: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 17: f(x2, x3) x4 -> f_1(x2, x3) x4 18: mms(x2, x3, x5, x6) x7 -> mms_l(x5, x6, x7) f(x2, x3) 19: main_6(x0, x2, x3, x5) x6 -> main_7(x0) mms(x2, x3, x5, x6) 20: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 21: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 22: cond_scanr_f_z_xs(Nil(), x6, x7) -> Cons(x7, Nil()) 23: cond_scanr_f_z_xs(Cons(x9, x10), x6, x7) -> cond_scanr_f_z_xs_1(scanr() x6 x7 x10, x6, x9) 24: scanr_f_z(x6, x7) x8 -> cond_scanr_f_z_xs(x8, x6, x7) 25: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 26: scanr_1() x6 -> scanr_f(x6) 27: scanr() x0 -> scanr_1() x0 28: main_5(x0, x2, x3) x5 -> main_6(x0, x2, x3, x5) scanr() 29: main_4(x0, x1, x2, x3) x4 -> main_5(x0, x2, x3) (x4 x1 0()) 30: cond_foldl_f_z_xs(Nil(), x4, x5) -> x5 31: cond_foldl_f_z_xs(Cons(x7, x8), x4, x5) -> foldl() x4 (x4 x5 x7) x8 32: foldl_f_z(x4, x5) x6 -> cond_foldl_f_z_xs(x6, x4, x5) 33: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 34: foldl_1() x4 -> foldl_f(x4) 35: foldl() x0 -> foldl_1() x0 36: main_3(x0, x1, x2) x3 -> main_4(x0, x1, x2, x3) foldl() 37: cond_minus_x_y_1(0(), x3, x5) -> x3 38: cond_minus_x_y_1(S(x6), x3, x5) -> minus() x5 x6 39: cond_minus_x_y(0(), x3, x4) -> 0() 40: cond_minus_x_y(S(x5), x3, x4) -> cond_minus_x_y_1(x4, x3, x5) 41: minus_x(x3) x4 -> cond_minus_x_y(x3, x3, x4) 42: minus_1() x3 -> minus_x(x3) 43: minus() x0 -> minus_1() x0 44: main_2(x0, x1) x2 -> main_3(x0, x1, x2) minus() 45: cond_plus_x_y(0(), x3) -> x3 46: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 47: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 48: plus_1() x2 -> plus_x(x2) 49: plus() x0 -> plus_1() x0 50: main_1(x0) x1 -> main_2(x0, x1) plus() 51: cond_max_x_y_1(0(), x1, x3) -> x1 52: cond_max_x_y_1(S(x4), x1, x3) -> S(max() x3 x4) 53: cond_max_x_y(0(), x1, x2) -> x2 54: cond_max_x_y(S(x3), x1, x2) -> cond_max_x_y_1(x2, x1, x3) 55: max_x(x1) x2 -> cond_max_x_y(x1, x1, x2) 56: max_1() x1 -> max_x(x1) 57: max() x0 -> max_1() x0 58: main(x0) -> main_1(x0) max() where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_foldl_f_z_xs :: int list -> (int -> int -> int) -> int -> int cond_scanr_f_z_xs :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int cond_max_x_y :: int -> int -> int -> int cond_minus_x_y :: int -> int -> int -> int cond_plus_x_y :: int -> int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y_1 :: int -> int -> int cond_max_x_y_1 :: int -> int -> int -> int cond_minus_x_y_1 :: int -> int -> int -> int cond_f_x_y_2 :: int -> (int -> int -> int) -> int -> int -> int cond_f_x_y_3 :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 3: cond_f_x_y_1(0(), x9) -> 0() 4: cond_f_x_y_1(M(x10), x9) -> 0() 5: cond_f_x_y_1(S(x10), x9) -> x9 6: cond_f_x_y_2(0(), x3, x9, x10) -> 0() 7: cond_f_x_y_2(M(x11), x3, x9, x10) -> 0() 8: cond_f_x_y_2(S(x11), x3, x9, x10) -> x3 x9 x10 9: cond_f_x_y_3(0(), x2, x3, x8, x9) -> x8 10: cond_f_x_y_3(M(x11), x2, x3, x8, x9) -> x3 x8 x11 11: cond_f_x_y_3(S(x11), x2, x3, x8, x9) -> x2 x8 x9 12: cond_f_x_y(0(), x2, x3, x8, x9) -> cond_f_x_y_1(x9, x9) 13: cond_f_x_y(M(x10), x2, x3, x8, x9) -> cond_f_x_y_2(x9, x3, x9, x10) 14: cond_f_x_y(S(x10), x2, x3, x8, x9) -> cond_f_x_y_3(x9, x2, x3, x8, x9) 15: f_x(x2, x3, x8) x9 -> cond_f_x_y(x8, x2, x3, x8, x9) 16: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 17: f(x4, x6) x16 -> f_x(x4, x6, x16) 18: mms(x5, x7, x10, x12) x14 -> x10 (x12 f(x5, x7) 0() x14) 19: main_6(x0, x5, x7, x11) x13 -> mms(x5, x7, x11, x13) x0 20: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 21: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 22: cond_scanr_f_z_xs(Nil(), x6, x7) -> Cons(x7, Nil()) 23: cond_scanr_f_z_xs(Cons(x9, x10), x6, x7) -> cond_scanr_f_z_xs_1(scanr() x6 x7 x10, x6, x9) 24: scanr_f_z(x6, x7) x8 -> cond_scanr_f_z_xs(x8, x6, x7) 25: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 26: scanr_1() x6 -> scanr_f(x6) 27: scanr() x12 -> scanr_f(x12) 28: main_5(x0, x4, x6) x10 -> main_7(x0) mms(x4, x6, x10, scanr()) 29: main_4(x0, x3, x4, x6) x9 -> main_6(x0, x4, x6, x9 x3 0()) scanr() 30: cond_foldl_f_z_xs(Nil(), x4, x5) -> x5 31: cond_foldl_f_z_xs(Cons(x7, x8), x4, x5) -> foldl() x4 (x4 x5 x7) x8 32: foldl_f_z(x4, x5) x6 -> cond_foldl_f_z_xs(x6, x4, x5) 33: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 34: foldl_1() x4 -> foldl_f(x4) 35: foldl() x8 -> foldl_f(x8) 36: main_3(x0, x2, x4) x6 -> main_5(x0, x4, x6) (foldl() x2 0()) 37: cond_minus_x_y_1(0(), x3, x5) -> x3 38: cond_minus_x_y_1(S(x6), x3, x5) -> minus() x5 x6 39: cond_minus_x_y(0(), x3, x4) -> 0() 40: cond_minus_x_y(S(x5), x3, x4) -> cond_minus_x_y_1(x4, x3, x5) 41: minus_x(x3) x4 -> cond_minus_x_y(x3, x3, x4) 42: minus_1() x3 -> minus_x(x3) 43: minus() x6 -> minus_x(x6) 44: main_2(x0, x2) x4 -> main_4(x0, x2, x4, minus()) foldl() 45: cond_plus_x_y(0(), x3) -> x3 46: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 47: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 48: plus_1() x2 -> plus_x(x2) 49: plus() x4 -> plus_x(x4) 50: main_1(x0) x2 -> main_3(x0, x2, plus()) minus() 51: cond_max_x_y_1(0(), x1, x3) -> x1 52: cond_max_x_y_1(S(x4), x1, x3) -> S(max() x3 x4) 53: cond_max_x_y(0(), x1, x2) -> x2 54: cond_max_x_y(S(x3), x1, x2) -> cond_max_x_y_1(x2, x1, x3) 55: max_x(x1) x2 -> cond_max_x_y(x1, x1, x2) 56: max_1() x1 -> max_x(x1) 57: max() x2 -> max_x(x2) 58: main(x0) -> main_2(x0, max()) plus() where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_foldl_f_z_xs :: int list -> (int -> int -> int) -> int -> int cond_scanr_f_z_xs :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int cond_max_x_y :: int -> int -> int -> int cond_minus_x_y :: int -> int -> int -> int cond_plus_x_y :: int -> int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y_1 :: int -> int -> int cond_max_x_y_1 :: int -> int -> int -> int cond_minus_x_y_1 :: int -> int -> int -> int cond_f_x_y_2 :: int -> (int -> int -> int) -> int -> int -> int cond_f_x_y_3 :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 3: cond_f_x_y_1(0(), x9) -> 0() 4: cond_f_x_y_1(M(x10), x9) -> 0() 5: cond_f_x_y_1(S(x10), x9) -> x9 6: cond_f_x_y_2(0(), x3, x9, x10) -> 0() 7: cond_f_x_y_2(M(x11), x3, x9, x10) -> 0() 8: cond_f_x_y_2(S(x11), x3, x9, x10) -> x3 x9 x10 9: cond_f_x_y_3(0(), x2, x3, x8, x9) -> x8 10: cond_f_x_y_3(M(x11), x2, x3, x8, x9) -> x3 x8 x11 11: cond_f_x_y_3(S(x11), x2, x3, x8, x9) -> x2 x8 x9 12: cond_f_x_y(0(), x2, x3, x8, x9) -> cond_f_x_y_1(x9, x9) 13: cond_f_x_y(M(x10), x2, x3, x8, x9) -> cond_f_x_y_2(x9, x3, x9, x10) 14: cond_f_x_y(S(x10), x2, x3, x8, x9) -> cond_f_x_y_3(x9, x2, x3, x8, x9) 15: f_x(x2, x3, x8) x9 -> cond_f_x_y(x8, x2, x3, x8, x9) 16: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 17: f(x4, x6) x16 -> f_x(x4, x6, x16) 18: mms(x5, x7, x10, x12) x14 -> x10 (x12 f(x5, x7) 0() x14) 19: main_6(x28, x10, x14, x20) x24 -> x20 (x24 f(x10, x14) 0() x28) 20: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 21: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 22: cond_scanr_f_z_xs(Nil(), x6, x7) -> Cons(x7, Nil()) 23: cond_scanr_f_z_xs(Cons(x9, x10), x6, x7) -> cond_scanr_f_z_xs_1(scanr() x6 x7 x10, x6, x9) 24: scanr_f_z(x6, x7) x8 -> cond_scanr_f_z_xs(x8, x6, x7) 25: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 26: scanr_1() x6 -> scanr_f(x6) 27: scanr() x12 -> scanr_f(x12) 28: main_5(x0, x9, x13) x21 -> mms(x9, x13, x21, scanr()) x0 29: main_4(x0, x7, x10, x14) x19 -> mms(x10, x14, x19 x7 0(), scanr()) x0 30: cond_foldl_f_z_xs(Nil(), x4, x5) -> x5 31: cond_foldl_f_z_xs(Cons(x7, x8), x4, x5) -> foldl() x4 (x4 x5 x7) x8 32: foldl_f_z(x4, x5) x6 -> cond_foldl_f_z_xs(x6, x4, x5) 33: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 34: foldl_1() x4 -> foldl_f(x4) 35: foldl() x8 -> foldl_f(x8) 36: main_3(x0, x5, x8) x12 -> main_7(x0) mms(x8, x12, foldl() x5 0(), scanr()) 37: cond_minus_x_y_1(0(), x3, x5) -> x3 38: cond_minus_x_y_1(S(x6), x3, x5) -> minus() x5 x6 39: cond_minus_x_y(0(), x3, x4) -> 0() 40: cond_minus_x_y(S(x5), x3, x4) -> cond_minus_x_y_1(x4, x3, x5) 41: minus_x(x3) x4 -> cond_minus_x_y(x3, x3, x4) 42: minus_1() x3 -> minus_x(x3) 43: minus() x6 -> minus_x(x6) 44: main_2(x0, x6) x8 -> main_6(x0, x8, minus(), foldl() x6 0()) scanr() 45: cond_plus_x_y(0(), x3) -> x3 46: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 47: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 48: plus_1() x2 -> plus_x(x2) 49: plus() x4 -> plus_x(x4) 50: main_1(x0) x4 -> main_5(x0, plus(), minus()) (foldl() x4 0()) 51: cond_max_x_y_1(0(), x1, x3) -> x1 52: cond_max_x_y_1(S(x4), x1, x3) -> S(max() x3 x4) 53: cond_max_x_y(0(), x1, x2) -> x2 54: cond_max_x_y(S(x3), x1, x2) -> cond_max_x_y_1(x2, x1, x3) 55: max_x(x1) x2 -> cond_max_x_y(x1, x1, x2) 56: max_1() x1 -> max_x(x1) 57: max() x2 -> max_x(x2) 58: main(x0) -> main_4(x0, max(), plus(), minus()) foldl() where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_foldl_f_z_xs :: int list -> (int -> int -> int) -> int -> int cond_scanr_f_z_xs :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int cond_max_x_y :: int -> int -> int -> int cond_minus_x_y :: int -> int -> int -> int cond_plus_x_y :: int -> int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y_1 :: int -> int -> int cond_max_x_y_1 :: int -> int -> int -> int cond_minus_x_y_1 :: int -> int -> int -> int cond_f_x_y_2 :: int -> (int -> int -> int) -> int -> int -> int cond_f_x_y_3 :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 3: cond_f_x_y_1(0(), x9) -> 0() 4: cond_f_x_y_1(M(x10), x9) -> 0() 5: cond_f_x_y_1(S(x10), x9) -> x9 6: cond_f_x_y_2(0(), x3, x9, x10) -> 0() 7: cond_f_x_y_2(M(x11), x3, x9, x10) -> 0() 8: cond_f_x_y_2(S(x11), x3, x9, x10) -> x3 x9 x10 9: cond_f_x_y_3(0(), x2, x3, x8, x9) -> x8 10: cond_f_x_y_3(M(x11), x2, x3, x8, x9) -> x3 x8 x11 11: cond_f_x_y_3(S(x11), x2, x3, x8, x9) -> x2 x8 x9 12: cond_f_x_y(0(), x2, x3, x8, x9) -> cond_f_x_y_1(x9, x9) 13: cond_f_x_y(M(x10), x2, x3, x8, x9) -> cond_f_x_y_2(x9, x3, x9, x10) 14: cond_f_x_y(S(x10), x2, x3, x8, x9) -> cond_f_x_y_3(x9, x2, x3, x8, x9) 15: f_x(x2, x3, x8) x9 -> cond_f_x_y(x8, x2, x3, x8, x9) 16: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 17: f(x4, x6) x16 -> f_x(x4, x6, x16) 18: mms(x5, x7, x10, x12) x14 -> x10 (x12 f(x5, x7) 0() x14) 19: main_6(x28, x10, x14, x20) x24 -> x20 (x24 f(x10, x14) 0() x28) 20: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 21: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 22: cond_scanr_f_z_xs(Nil(), x6, x7) -> Cons(x7, Nil()) 23: cond_scanr_f_z_xs(Cons(x9, x10), x6, x7) -> cond_scanr_f_z_xs_1(scanr() x6 x7 x10, x6, x9) 24: scanr_f_z(x6, x7) x8 -> cond_scanr_f_z_xs(x8, x6, x7) 25: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 26: scanr_1() x6 -> scanr_f(x6) 27: scanr() x12 -> scanr_f(x12) 28: main_5(x28, x10, x14) x20 -> x20 (scanr() f(x10, x14) 0() x28) 29: main_4(x28, x15, x10, x14) x39 -> x39 x15 0() (scanr() f(x10, x14) 0() x28) 30: cond_foldl_f_z_xs(Nil(), x4, x5) -> x5 31: cond_foldl_f_z_xs(Cons(x7, x8), x4, x5) -> foldl() x4 (x4 x5 x7) x8 32: foldl_f_z(x4, x5) x6 -> cond_foldl_f_z_xs(x6, x4, x5) 33: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 34: foldl_1() x4 -> foldl_f(x4) 35: foldl() x8 -> foldl_f(x8) 36: main_3(x0, x11, x17) x25 -> mms(x17, x25, foldl() x11 0(), scanr()) x0 37: cond_minus_x_y_1(0(), x3, x5) -> x3 38: cond_minus_x_y_1(S(x6), x3, x5) -> minus() x5 x6 39: cond_minus_x_y(0(), x3, x4) -> 0() 40: cond_minus_x_y(S(x5), x3, x4) -> cond_minus_x_y_1(x4, x3, x5) 41: minus_x(x3) x4 -> cond_minus_x_y(x3, x3, x4) 42: minus_1() x3 -> minus_x(x3) 43: minus() x6 -> minus_x(x6) 44: main_2(x56, x13) x20 -> foldl() x13 0() (scanr() f(x20, minus()) 0() x56) 45: cond_plus_x_y(0(), x3) -> x3 46: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 47: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 48: plus_1() x2 -> plus_x(x2) 49: plus() x4 -> plus_x(x4) 50: main_1(x0) x9 -> mms(plus(), minus(), foldl() x9 0(), scanr()) x0 51: cond_max_x_y_1(0(), x1, x3) -> x1 52: cond_max_x_y_1(S(x4), x1, x3) -> S(max() x3 x4) 53: cond_max_x_y(0(), x1, x2) -> x2 54: cond_max_x_y(S(x3), x1, x2) -> cond_max_x_y_1(x2, x1, x3) 55: max_x(x1) x2 -> cond_max_x_y(x1, x1, x2) 56: max_1() x1 -> max_x(x1) 57: max() x2 -> max_x(x2) 58: main(x0) -> mms(plus(), minus(), foldl() max() 0(), scanr()) x0 where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_foldl_f_z_xs :: int list -> (int -> int -> int) -> int -> int cond_scanr_f_z_xs :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int cond_max_x_y :: int -> int -> int -> int cond_minus_x_y :: int -> int -> int -> int cond_plus_x_y :: int -> int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y_1 :: int -> int -> int cond_max_x_y_1 :: int -> int -> int -> int cond_minus_x_y_1 :: int -> int -> int -> int cond_f_x_y_2 :: int -> (int -> int -> int) -> int -> int -> int cond_f_x_y_3 :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 7: Inline MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 3: cond_f_x_y_1(0(), x9) -> 0() 4: cond_f_x_y_1(M(x10), x9) -> 0() 5: cond_f_x_y_1(S(x10), x9) -> x9 6: cond_f_x_y_2(0(), x3, x9, x10) -> 0() 7: cond_f_x_y_2(M(x11), x3, x9, x10) -> 0() 8: cond_f_x_y_2(S(x11), x3, x9, x10) -> x3 x9 x10 9: cond_f_x_y_3(0(), x2, x3, x8, x9) -> x8 10: cond_f_x_y_3(M(x11), x2, x3, x8, x9) -> x3 x8 x11 11: cond_f_x_y_3(S(x11), x2, x3, x8, x9) -> x2 x8 x9 12: cond_f_x_y(0(), x2, x3, x8, x9) -> cond_f_x_y_1(x9, x9) 13: cond_f_x_y(M(x10), x2, x3, x8, x9) -> cond_f_x_y_2(x9, x3, x9, x10) 14: cond_f_x_y(S(x10), x2, x3, x8, x9) -> cond_f_x_y_3(x9, x2, x3, x8, x9) 15: f_x(x2, x3, x8) x9 -> cond_f_x_y(x8, x2, x3, x8, x9) 16: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 17: f(x4, x6) x16 -> f_x(x4, x6, x16) 18: mms(x5, x7, x10, x12) x14 -> x10 (x12 f(x5, x7) 0() x14) 19: main_6(x28, x10, x14, x20) x24 -> x20 (x24 f(x10, x14) 0() x28) 20: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 21: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 22: cond_scanr_f_z_xs(Nil(), x6, x7) -> Cons(x7, Nil()) 23: cond_scanr_f_z_xs(Cons(x9, x10), x6, x7) -> cond_scanr_f_z_xs_1(scanr() x6 x7 x10, x6, x9) 24: scanr_f_z(x6, x7) x8 -> cond_scanr_f_z_xs(x8, x6, x7) 25: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 26: scanr_1() x6 -> scanr_f(x6) 27: scanr() x12 -> scanr_f(x12) 28: main_5(x28, x10, x14) x20 -> x20 (scanr() f(x10, x14) 0() x28) 29: main_4(x28, x15, x10, x14) x39 -> x39 x15 0() (scanr() f(x10, x14) 0() x28) 30: cond_foldl_f_z_xs(Nil(), x4, x5) -> x5 31: cond_foldl_f_z_xs(Cons(x7, x8), x4, x5) -> foldl() x4 (x4 x5 x7) x8 32: foldl_f_z(x4, x5) x6 -> cond_foldl_f_z_xs(x6, x4, x5) 33: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 34: foldl_1() x4 -> foldl_f(x4) 35: foldl() x8 -> foldl_f(x8) 36: main_3(x28, x23, x10) x14 -> foldl() x23 0() (scanr() f(x10, x14) 0() x28) 37: cond_minus_x_y_1(0(), x3, x5) -> x3 38: cond_minus_x_y_1(S(x6), x3, x5) -> minus() x5 x6 39: cond_minus_x_y(0(), x3, x4) -> 0() 40: cond_minus_x_y(S(x5), x3, x4) -> cond_minus_x_y_1(x4, x3, x5) 41: minus_x(x3) x4 -> cond_minus_x_y(x3, x3, x4) 42: minus_1() x3 -> minus_x(x3) 43: minus() x6 -> minus_x(x6) 44: main_2(x56, x13) x20 -> foldl() x13 0() (scanr() f(x20, minus()) 0() x56) 45: cond_plus_x_y(0(), x3) -> x3 46: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 47: plus_x(x2) x3 -> cond_plus_x_y(x2, x3) 48: plus_1() x2 -> plus_x(x2) 49: plus() x4 -> plus_x(x4) 50: main_1(x28) x19 -> foldl() x19 0() (scanr() f(plus(), minus()) 0() x28) 51: cond_max_x_y_1(0(), x1, x3) -> x1 52: cond_max_x_y_1(S(x4), x1, x3) -> S(max() x3 x4) 53: cond_max_x_y(0(), x1, x2) -> x2 54: cond_max_x_y(S(x3), x1, x2) -> cond_max_x_y_1(x2, x1, x3) 55: max_x(x1) x2 -> cond_max_x_y(x1, x1, x2) 56: max_1() x1 -> max_x(x1) 57: max() x2 -> max_x(x2) 58: main(x28) -> foldl() max() 0() (scanr() f(plus(), minus()) 0() x28) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_foldl_f_z_xs :: int list -> (int -> int -> int) -> int -> int cond_scanr_f_z_xs :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int cond_max_x_y :: int -> int -> int -> int cond_minus_x_y :: int -> int -> int -> int cond_plus_x_y :: int -> int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y_1 :: int -> int -> int cond_max_x_y_1 :: int -> int -> int -> int cond_minus_x_y_1 :: int -> int -> int -> int cond_f_x_y_2 :: int -> (int -> int -> int) -> int -> int -> int cond_f_x_y_3 :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 8: Inline MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 3: cond_f_x_y_1(0(), x9) -> 0() 4: cond_f_x_y_1(M(x10), x9) -> 0() 5: cond_f_x_y_1(S(x10), x9) -> x9 6: cond_f_x_y_2(0(), x3, x9, x10) -> 0() 7: cond_f_x_y_2(M(x11), x3, x9, x10) -> 0() 8: cond_f_x_y_2(S(x11), x3, x9, x10) -> x3 x9 x10 9: cond_f_x_y_3(0(), x2, x3, x8, x9) -> x8 10: cond_f_x_y_3(M(x11), x2, x3, x8, x9) -> x3 x8 x11 11: cond_f_x_y_3(S(x11), x2, x3, x8, x9) -> x2 x8 x9 12: cond_f_x_y(0(), x5, x7, x17, 0()) -> 0() 13: cond_f_x_y(0(), x5, x7, x17, M(x20)) -> 0() 14: cond_f_x_y(0(), x5, x7, x17, S(x20)) -> S(x20) 15: cond_f_x_y(M(x20), x5, x6, x17, 0()) -> 0() 16: cond_f_x_y(M(x20), x5, x6, x17, M(x22)) -> 0() 17: cond_f_x_y(M(x20), x5, x6, x17, S(x22)) -> x6 S(x22) x20 18: cond_f_x_y(S(x21), x4, x6, x16, 0()) -> x16 19: cond_f_x_y(S(x21), x4, x6, x16, M(x22)) -> x6 x16 x22 20: cond_f_x_y(S(x21), x4, x6, x16, S(x22)) -> x4 x16 S(x22) 21: f_x(x4, x6, 0()) x18 -> cond_f_x_y_1(x18, x18) 22: f_x(x4, x6, M(x20)) x18 -> cond_f_x_y_2(x18, x6, x18, x20) 23: f_x(x4, x6, S(x20)) x18 -> cond_f_x_y_3(x18, x4, x6, S(x20), x18) 24: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 25: f(x4, x6) x16 -> f_x(x4, x6, x16) 26: mms(x5, x7, x10, x12) x14 -> x10 (x12 f(x5, x7) 0() x14) 27: main_6(x28, x10, x14, x20) x24 -> x20 (x24 f(x10, x14) 0() x28) 28: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 29: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 30: cond_scanr_f_z_xs(Nil(), x6, x7) -> Cons(x7, Nil()) 31: cond_scanr_f_z_xs(Cons(x9, x10), x6, x7) -> cond_scanr_f_z_xs_1(scanr() x6 x7 x10, x6, x9) 32: scanr_f_z(x12, x14) Nil() -> Cons(x14, Nil()) 33: scanr_f_z(x12, x14) Cons(x18, x20) -> cond_scanr_f_z_xs_1(scanr() x12 x14 x20, x12, x18) 34: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 35: scanr_1() x6 -> scanr_f(x6) 36: scanr() x12 -> scanr_f(x12) 37: main_5(x28, x10, x14) x20 -> x20 (scanr() f(x10, x14) 0() x28) 38: main_4(x28, x15, x10, x14) x39 -> x39 x15 0() (scanr() f(x10, x14) 0() x28) 39: cond_foldl_f_z_xs(Nil(), x4, x5) -> x5 40: cond_foldl_f_z_xs(Cons(x7, x8), x4, x5) -> foldl() x4 (x4 x5 x7) x8 41: foldl_f_z(x8, x10) Nil() -> x10 42: foldl_f_z(x8, x10) Cons(x14, x16) -> foldl() x8 (x8 x10 x14) x16 43: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 44: foldl_1() x4 -> foldl_f(x4) 45: foldl() x8 -> foldl_f(x8) 46: main_3(x28, x23, x10) x14 -> foldl() x23 0() (scanr() f(x10, x14) 0() x28) 47: cond_minus_x_y_1(0(), x3, x5) -> x3 48: cond_minus_x_y_1(S(x6), x3, x5) -> minus() x5 x6 49: cond_minus_x_y(0(), x3, x4) -> 0() 50: cond_minus_x_y(S(x10), x6, 0()) -> x6 51: cond_minus_x_y(S(x10), x6, S(x12)) -> minus() x10 x12 52: minus_x(0()) x8 -> 0() 53: minus_x(S(x10)) x8 -> cond_minus_x_y_1(x8, S(x10), x10) 54: minus_1() x3 -> minus_x(x3) 55: minus() x6 -> minus_x(x6) 56: main_2(x56, x13) x20 -> foldl() x13 0() (scanr() f(x20, minus()) 0() x56) 57: cond_plus_x_y(0(), x3) -> x3 58: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 59: plus_x(0()) x6 -> x6 60: plus_x(S(x8)) x6 -> S(plus() x8 x6) 61: plus_1() x2 -> plus_x(x2) 62: plus() x4 -> plus_x(x4) 63: main_1(x28) x19 -> foldl() x19 0() (scanr() f(plus(), minus()) 0() x28) 64: cond_max_x_y_1(0(), x1, x3) -> x1 65: cond_max_x_y_1(S(x4), x1, x3) -> S(max() x3 x4) 66: cond_max_x_y(0(), x1, x2) -> x2 67: cond_max_x_y(S(x6), x2, 0()) -> x2 68: cond_max_x_y(S(x6), x2, S(x8)) -> S(max() x6 x8) 69: max_x(0()) x4 -> x4 70: max_x(S(x6)) x4 -> cond_max_x_y_1(x4, S(x6), x6) 71: max_1() x1 -> max_x(x1) 72: max() x2 -> max_x(x2) 73: main(x28) -> foldl() max() 0() (scanr() f(plus(), minus()) 0() x28) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_foldl_f_z_xs :: int list -> (int -> int -> int) -> int -> int cond_scanr_f_z_xs :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int cond_max_x_y :: int -> int -> int -> int cond_minus_x_y :: int -> int -> int -> int cond_plus_x_y :: int -> int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y_1 :: int -> int -> int cond_max_x_y_1 :: int -> int -> int -> int cond_minus_x_y_1 :: int -> int -> int -> int cond_f_x_y_2 :: int -> (int -> int -> int) -> int -> int -> int cond_f_x_y_3 :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 9: UsableRules MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 3: cond_f_x_y_1(0(), x9) -> 0() 4: cond_f_x_y_1(M(x10), x9) -> 0() 5: cond_f_x_y_1(S(x10), x9) -> x9 6: cond_f_x_y_2(0(), x3, x9, x10) -> 0() 7: cond_f_x_y_2(M(x11), x3, x9, x10) -> 0() 8: cond_f_x_y_2(S(x11), x3, x9, x10) -> x3 x9 x10 9: cond_f_x_y_3(0(), x2, x3, x8, x9) -> x8 10: cond_f_x_y_3(M(x11), x2, x3, x8, x9) -> x3 x8 x11 11: cond_f_x_y_3(S(x11), x2, x3, x8, x9) -> x2 x8 x9 12: cond_f_x_y(0(), x5, x7, x17, 0()) -> 0() 13: cond_f_x_y(0(), x5, x7, x17, M(x20)) -> 0() 14: cond_f_x_y(0(), x5, x7, x17, S(x20)) -> S(x20) 15: cond_f_x_y(M(x20), x5, x6, x17, 0()) -> 0() 16: cond_f_x_y(M(x20), x5, x6, x17, M(x22)) -> 0() 17: cond_f_x_y(M(x20), x5, x6, x17, S(x22)) -> x6 S(x22) x20 18: cond_f_x_y(S(x21), x4, x6, x16, 0()) -> x16 19: cond_f_x_y(S(x21), x4, x6, x16, M(x22)) -> x6 x16 x22 20: cond_f_x_y(S(x21), x4, x6, x16, S(x22)) -> x4 x16 S(x22) 21: f_x(x9, x13, 0()) 0() -> 0() 22: f_x(x9, x13, 0()) M(x20) -> 0() 23: f_x(x9, x13, 0()) S(x20) -> S(x20) 24: f_x(x9, x6, M(x20)) 0() -> 0() 25: f_x(x9, x6, M(x20)) M(x22) -> 0() 26: f_x(x9, x6, M(x20)) S(x22) -> x6 S(x22) x20 27: f_x(x4, x6, S(x41)) 0() -> S(x41) 28: f_x(x4, x6, S(x41)) M(x22) -> x6 S(x41) x22 29: f_x(x4, x6, S(x41)) S(x22) -> x4 S(x41) S(x22) 30: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 31: f(x4, x6) x16 -> f_x(x4, x6, x16) 32: mms(x5, x7, x10, x12) x14 -> x10 (x12 f(x5, x7) 0() x14) 33: main_6(x28, x10, x14, x20) x24 -> x20 (x24 f(x10, x14) 0() x28) 34: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 35: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 36: cond_scanr_f_z_xs(Nil(), x6, x7) -> Cons(x7, Nil()) 37: cond_scanr_f_z_xs(Cons(x9, x10), x6, x7) -> cond_scanr_f_z_xs_1(scanr() x6 x7 x10, x6, x9) 38: scanr_f_z(x12, x14) Nil() -> Cons(x14, Nil()) 39: scanr_f_z(x12, x14) Cons(x18, x20) -> cond_scanr_f_z_xs_1(scanr() x12 x14 x20, x12, x18) 40: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 41: scanr_1() x6 -> scanr_f(x6) 42: scanr() x12 -> scanr_f(x12) 43: main_5(x28, x10, x14) x20 -> x20 (scanr() f(x10, x14) 0() x28) 44: main_4(x28, x15, x10, x14) x39 -> x39 x15 0() (scanr() f(x10, x14) 0() x28) 45: cond_foldl_f_z_xs(Nil(), x4, x5) -> x5 46: cond_foldl_f_z_xs(Cons(x7, x8), x4, x5) -> foldl() x4 (x4 x5 x7) x8 47: foldl_f_z(x8, x10) Nil() -> x10 48: foldl_f_z(x8, x10) Cons(x14, x16) -> foldl() x8 (x8 x10 x14) x16 49: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 50: foldl_1() x4 -> foldl_f(x4) 51: foldl() x8 -> foldl_f(x8) 52: main_3(x28, x23, x10) x14 -> foldl() x23 0() (scanr() f(x10, x14) 0() x28) 53: cond_minus_x_y_1(0(), x3, x5) -> x3 54: cond_minus_x_y_1(S(x6), x3, x5) -> minus() x5 x6 55: cond_minus_x_y(0(), x3, x4) -> 0() 56: cond_minus_x_y(S(x10), x6, 0()) -> x6 57: cond_minus_x_y(S(x10), x6, S(x12)) -> minus() x10 x12 58: minus_x(0()) x8 -> 0() 59: minus_x(S(x10)) 0() -> S(x10) 60: minus_x(S(x10)) S(x12) -> minus() x10 x12 61: minus_1() x3 -> minus_x(x3) 62: minus() x6 -> minus_x(x6) 63: main_2(x56, x13) x20 -> foldl() x13 0() (scanr() f(x20, minus()) 0() x56) 64: cond_plus_x_y(0(), x3) -> x3 65: cond_plus_x_y(S(x4), x3) -> S(plus() x4 x3) 66: plus_x(0()) x6 -> x6 67: plus_x(S(x8)) x6 -> S(plus() x8 x6) 68: plus_1() x2 -> plus_x(x2) 69: plus() x4 -> plus_x(x4) 70: main_1(x28) x19 -> foldl() x19 0() (scanr() f(plus(), minus()) 0() x28) 71: cond_max_x_y_1(0(), x1, x3) -> x1 72: cond_max_x_y_1(S(x4), x1, x3) -> S(max() x3 x4) 73: cond_max_x_y(0(), x1, x2) -> x2 74: cond_max_x_y(S(x6), x2, 0()) -> x2 75: cond_max_x_y(S(x6), x2, S(x8)) -> S(max() x6 x8) 76: max_x(0()) x4 -> x4 77: max_x(S(x6)) 0() -> S(x6) 78: max_x(S(x6)) S(x8) -> S(max() x6 x8) 79: max_1() x1 -> max_x(x1) 80: max() x2 -> max_x(x2) 81: main(x28) -> foldl() max() 0() (scanr() f(plus(), minus()) 0() x28) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_foldl_f_z_xs :: int list -> (int -> int -> int) -> int -> int cond_scanr_f_z_xs :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int cond_max_x_y :: int -> int -> int -> int cond_minus_x_y :: int -> int -> int -> int cond_plus_x_y :: int -> int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list cond_f_x_y_1 :: int -> int -> int cond_max_x_y_1 :: int -> int -> int -> int cond_minus_x_y_1 :: int -> int -> int -> int cond_f_x_y_2 :: int -> (int -> int -> int) -> int -> int -> int cond_f_x_y_3 :: int -> (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 10: NeededRules MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 21: f_x(x9, x13, 0()) 0() -> 0() 22: f_x(x9, x13, 0()) M(x20) -> 0() 23: f_x(x9, x13, 0()) S(x20) -> S(x20) 24: f_x(x9, x6, M(x20)) 0() -> 0() 25: f_x(x9, x6, M(x20)) M(x22) -> 0() 26: f_x(x9, x6, M(x20)) S(x22) -> x6 S(x22) x20 27: f_x(x4, x6, S(x41)) 0() -> S(x41) 28: f_x(x4, x6, S(x41)) M(x22) -> x6 S(x41) x22 29: f_x(x4, x6, S(x41)) S(x22) -> x4 S(x41) S(x22) 30: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 31: f(x4, x6) x16 -> f_x(x4, x6, x16) 32: mms(x5, x7, x10, x12) x14 -> x10 (x12 f(x5, x7) 0() x14) 33: main_6(x28, x10, x14, x20) x24 -> x20 (x24 f(x10, x14) 0() x28) 34: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 35: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 38: scanr_f_z(x12, x14) Nil() -> Cons(x14, Nil()) 39: scanr_f_z(x12, x14) Cons(x18, x20) -> cond_scanr_f_z_xs_1(scanr() x12 x14 x20, x12, x18) 40: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 41: scanr_1() x6 -> scanr_f(x6) 42: scanr() x12 -> scanr_f(x12) 43: main_5(x28, x10, x14) x20 -> x20 (scanr() f(x10, x14) 0() x28) 44: main_4(x28, x15, x10, x14) x39 -> x39 x15 0() (scanr() f(x10, x14) 0() x28) 47: foldl_f_z(x8, x10) Nil() -> x10 48: foldl_f_z(x8, x10) Cons(x14, x16) -> foldl() x8 (x8 x10 x14) x16 49: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 50: foldl_1() x4 -> foldl_f(x4) 51: foldl() x8 -> foldl_f(x8) 52: main_3(x28, x23, x10) x14 -> foldl() x23 0() (scanr() f(x10, x14) 0() x28) 58: minus_x(0()) x8 -> 0() 59: minus_x(S(x10)) 0() -> S(x10) 60: minus_x(S(x10)) S(x12) -> minus() x10 x12 61: minus_1() x3 -> minus_x(x3) 62: minus() x6 -> minus_x(x6) 63: main_2(x56, x13) x20 -> foldl() x13 0() (scanr() f(x20, minus()) 0() x56) 66: plus_x(0()) x6 -> x6 67: plus_x(S(x8)) x6 -> S(plus() x8 x6) 68: plus_1() x2 -> plus_x(x2) 69: plus() x4 -> plus_x(x4) 70: main_1(x28) x19 -> foldl() x19 0() (scanr() f(plus(), minus()) 0() x28) 76: max_x(0()) x4 -> x4 77: max_x(S(x6)) 0() -> S(x6) 78: max_x(S(x6)) S(x8) -> S(max() x6 x8) 79: max_1() x1 -> max_x(x1) 80: max() x2 -> max_x(x2) 81: main(x28) -> foldl() max() 0() (scanr() f(plus(), minus()) 0() x28) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: NeededRules + Details: none * Step 11: CFA MAYBE + Considered Problem: 1: main_7(x0) x7 -> x7 x0 2: mms_l(x5, x6, x7) x8 -> x5 (x6 x8 0() x7) 3: f_x(x9, x13, 0()) 0() -> 0() 4: f_x(x9, x13, 0()) M(x20) -> 0() 5: f_x(x9, x13, 0()) S(x20) -> S(x20) 6: f_x(x9, x6, M(x20)) 0() -> 0() 7: f_x(x9, x6, M(x20)) M(x22) -> 0() 8: f_x(x9, x6, M(x20)) S(x22) -> x6 S(x22) x20 9: f_x(x4, x6, S(x41)) 0() -> S(x41) 10: f_x(x4, x6, S(x41)) M(x22) -> x6 S(x41) x22 11: f_x(x4, x6, S(x41)) S(x22) -> x4 S(x41) S(x22) 12: f_1(x2, x3) x8 -> f_x(x2, x3, x8) 13: f(x4, x6) x16 -> f_x(x4, x6, x16) 14: mms(x5, x7, x10, x12) x14 -> x10 (x12 f(x5, x7) 0() x14) 15: main_6(x28, x10, x14, x20) x24 -> x20 (x24 f(x10, x14) 0() x28) 16: cond_scanr_f_z_xs_1(Nil(), x6, x9) -> bot[0]() 17: cond_scanr_f_z_xs_1(Cons(x11, x12), x6, x9) -> Cons(x6 x9 x11, Cons(x11, x12)) 18: scanr_f_z(x12, x14) Nil() -> Cons(x14, Nil()) 19: scanr_f_z(x12, x14) Cons(x18, x20) -> cond_scanr_f_z_xs_1(scanr() x12 x14 x20, x12, x18) 20: scanr_f(x6) x7 -> scanr_f_z(x6, x7) 21: scanr_1() x6 -> scanr_f(x6) 22: scanr() x12 -> scanr_f(x12) 23: main_5(x28, x10, x14) x20 -> x20 (scanr() f(x10, x14) 0() x28) 24: main_4(x28, x15, x10, x14) x39 -> x39 x15 0() (scanr() f(x10, x14) 0() x28) 25: foldl_f_z(x8, x10) Nil() -> x10 26: foldl_f_z(x8, x10) Cons(x14, x16) -> foldl() x8 (x8 x10 x14) x16 27: foldl_f(x4) x5 -> foldl_f_z(x4, x5) 28: foldl_1() x4 -> foldl_f(x4) 29: foldl() x8 -> foldl_f(x8) 30: main_3(x28, x23, x10) x14 -> foldl() x23 0() (scanr() f(x10, x14) 0() x28) 31: minus_x(0()) x8 -> 0() 32: minus_x(S(x10)) 0() -> S(x10) 33: minus_x(S(x10)) S(x12) -> minus() x10 x12 34: minus_1() x3 -> minus_x(x3) 35: minus() x6 -> minus_x(x6) 36: main_2(x56, x13) x20 -> foldl() x13 0() (scanr() f(x20, minus()) 0() x56) 37: plus_x(0()) x6 -> x6 38: plus_x(S(x8)) x6 -> S(plus() x8 x6) 39: plus_1() x2 -> plus_x(x2) 40: plus() x4 -> plus_x(x4) 41: main_1(x28) x19 -> foldl() x19 0() (scanr() f(plus(), minus()) 0() x28) 42: max_x(0()) x4 -> x4 43: max_x(S(x6)) 0() -> S(x6) 44: max_x(S(x6)) S(x8) -> S(max() x6 x8) 45: max_1() x1 -> max_x(x1) 46: max() x2 -> max_x(x2) 47: main(x28) -> foldl() max() 0() (scanr() f(plus(), minus()) 0() x28) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list mms_l :: (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> (int -> int -> int) -> int mms :: (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int list -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list f_1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl_1 :: (int -> int -> int) -> int -> int list -> int main_1 :: int list -> (int -> int -> int) -> int max_1 :: int -> int -> int minus_1 :: int -> int -> int plus_1 :: int -> int -> int scanr_1 :: (int -> int -> int) -> int -> int list -> int list main_2 :: int list -> (int -> int -> int) -> (int -> int -> int) -> int main_3 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> int main_4 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int -> int -> int) -> ((int -> int -> int) -> int -> int list -> int) -> int main_5 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> int main_6 :: int list -> (int -> int -> int) -> (int -> int -> int) -> (int list -> int) -> ((int -> int -> int) -> int -> int list -> int list) -> int main_7 :: int list -> (int list -> int) -> int bot[0] :: int list cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: CFA {cfaRefinement = } + Details: {X{*} -> 0() | 0() | S(X{*}) | S(X{*}) | S(X{*}) | S(X{*}) | 0() | S(X{*}) | 0() | 0() | 0() | S(X{*}) | S(X{*}) | 0() | 0() | 0() | S(X{*}) | S(X{*}) | S(X{*}) | 0() | S(X{*}) | 0() | 0() | 0() | 0() | Cons(X{*},X{*}) | Nil() | 0() | 0() | 0() | Cons(X{*},X{*}) | Nil() | Cons(X{*},X{*}) | Nil() | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Cons(X{*},X{*}) | Nil() | 0() | 0() | S(X{*}) | S(X{*}) | S(X{*}) | S(X{*}) | S(X{*}) | M(X{*}) | S(X{*}) | S(X{*}) | 0() | S(X{*}) | S(X{*}) | S(X{*}) | M(X{*}) | 0() | M(X{*}) | M(X{*}) | 0() | 0() | M(X{*}) | S(X{*}) | S(X{*}) | 0() | 0() | M(X{*}) | 0() | 0() | 0() | 0() | 0() ,V{x2_46} -> V{x6_44} | V{x10_26} ,V{x4_9} -> V{x4_13} ,V{x4_11} -> V{x4_13} ,V{x4_13} -> plus() ,V{x4_27} -> V{x8_29} ,V{x4_40} -> V{x8_38} | S(V{x41_11}) ,V{x4_42} -> V{x8_44} | V{x14_26} ,V{x5_27} -> R{44} | R{43} | R{42} | 0() ,V{x6_6} -> V{x6_13} ,V{x6_8} -> V{x6_13} ,V{x6_9} -> V{x6_13} ,V{x6_11} -> V{x6_13} ,V{x6_13} -> minus() ,V{x6_17} -> V{x12_19} ,V{x6_20} -> V{x12_22} ,V{x6_35} -> V{x10_33} | S(V{x22_8}) ,V{x6_37} -> V{x6_38} | S(V{x22_11}) ,V{x6_38} -> V{x6_38} | S(V{x22_11}) ,V{x6_43} -> @(@(max(),V{x6_44}),V{x8_44}) | @(R{46},V{x8_44}) | R{42} | R{43} | R{44} | R{38} | R{37} | V{x22_11} | X{*} | @(R{40},V{x6_38}) | @(@(plus(),V{x8_38}),V{x6_38}) | V{x10_32} | V{x6_43} | V{x20_5} | V{x41_9} ,V{x6_44} -> @(@(max(),V{x6_44}),V{x8_44}) | @(R{46},V{x8_44}) | R{42} | R{43} | R{44} | R{38} | R{37} | V{x22_11} | X{*} | @(R{40},V{x6_38}) | @(@(plus(),V{x8_38}),V{x6_38}) | V{x10_32} | V{x6_43} | V{x20_5} | V{x41_9} ,V{x7_20} -> V{x14_19} | 0() ,V{x8_25} -> V{x4_27} ,V{x8_26} -> V{x4_27} ,V{x8_29} -> V{x8_26} | max() ,V{x8_31} -> V{x12_33} | V{x20_8} ,V{x8_38} -> X{*} | V{x41_11} ,V{x8_44} -> R{38} | R{37} | X{*} | V{x22_11} | @(R{40},V{x6_38}) | @(@(plus(),V{x8_38}),V{x6_38}) | V{x10_32} | V{x20_5} | V{x41_9} ,V{x9_3} -> V{x4_13} ,V{x9_5} -> V{x4_13} ,V{x9_6} -> V{x4_13} ,V{x9_8} -> V{x4_13} ,V{x9_17} -> V{x18_19} ,V{x10_25} -> V{x5_27} ,V{x10_26} -> V{x5_27} ,V{x10_32} -> R{38} | R{37} | X{*} | V{x22_11} | @(@(plus(),V{x8_38}),V{x6_38}) | @(R{40},V{x6_38}) | V{x22_8} ,V{x10_33} -> R{38} | R{37} | X{*} | V{x22_11} | @(@(plus(),V{x8_38}),V{x6_38}) | @(R{40},V{x6_38}) | V{x22_8} ,V{x11_17} -> R{5} | R{8} | R{11} | R{9} | R{6} | R{3} | @(@(V{x6_17},V{x9_17}),V{x11_17}) | @(R{13},V{x11_17}) | V{x14_18} ,V{x12_17} -> Cons(V{x11_17},V{x12_17}) | Nil() ,V{x12_18} -> V{x6_20} ,V{x12_19} -> V{x6_20} ,V{x12_22} -> V{x12_19} | f(plus(),minus()) ,V{x12_33} -> X{*} ,V{x13_3} -> V{x6_13} ,V{x13_5} -> V{x6_13} ,V{x14_18} -> V{x7_20} ,V{x14_19} -> V{x7_20} ,V{x14_26} -> V{x11_17} | R{11} | R{9} | R{8} | R{6} | R{5} | R{3} | @(R{13},V{x11_17}) | @(@(V{x6_17},V{x9_17}),V{x11_17}) | V{x14_18} ,V{x16_13} -> V{x9_17} ,V{x16_26} -> V{x12_17} | Cons(V{x11_17},V{x12_17}) | Nil() ,V{x18_19} -> X{*} ,V{x20_5} -> R{38} | R{37} | V{x22_11} | @(R{40},V{x6_38}) | @(@(plus(),V{x8_38}),V{x6_38}) | V{x10_32} | V{x20_5} | V{x41_9} ,V{x20_6} -> X{*} ,V{x20_8} -> X{*} ,V{x20_19} -> X{*} ,V{x22_8} -> R{38} | R{37} | V{x22_11} | @(R{40},V{x6_38}) | @(@(plus(),V{x8_38}),V{x6_38}) | V{x10_32} | V{x20_5} | V{x41_9} ,V{x22_11} -> R{38} | R{37} | V{x22_11} | @(R{40},V{x6_38}) | @(@(plus(),V{x8_38}),V{x6_38}) | V{x10_32} | V{x20_5} | V{x41_9} ,V{x28_47} -> X{*} ,V{x41_9} -> X{*} ,V{x41_11} -> X{*} ,R{0} -> R{47} | main(X{*}) ,R{3} -> 0() ,R{5} -> S(V{x20_5}) ,R{6} -> 0() ,R{8} -> R{31} | R{33} | R{32} | @(R{35},V{x20_8}) | @(@(V{x6_8},S(V{x22_8})),V{x20_8}) ,R{9} -> S(V{x41_9}) ,R{11} -> R{37} | R{38} | @(R{40},S(V{x22_11})) | @(@(V{x4_11},S(V{x41_11})),S(V{x22_11})) ,R{13} -> f_x(V{x4_13},V{x6_13},V{x16_13}) ,R{17} -> Cons(R{11},Cons(V{x11_17},V{x12_17})) | Cons(R{9},Cons(V{x11_17},V{x12_17})) | Cons(R{8},Cons(V{x11_17},V{x12_17})) | Cons(R{6},Cons(V{x11_17},V{x12_17})) | Cons(R{5},Cons(V{x11_17},V{x12_17})) | Cons(R{3},Cons(V{x11_17},V{x12_17})) | Cons(@(R{13},V{x11_17}),Cons(V{x11_17},V{x12_17})) | Cons(@(@(V{x6_17},V{x9_17}),V{x11_17}),Cons(V{x11_17},V{x12_17})) ,R{18} -> Cons(V{x14_18},Nil()) ,R{19} -> R{17} | cond_scanr_f_z_xs_1(R{19},V{x12_19},V{x18_19}) | cond_scanr_f_z_xs_1(R{18},V{x12_19},V{x18_19}) | cond_scanr_f_z_xs_1(@(R{20},V{x20_19}),V{x12_19},V{x18_19}) | cond_scanr_f_z_xs_1(@(@(R{22},V{x14_19}),V{x20_19}),V{x12_19},V{x18_19}) | cond_scanr_f_z_xs_1(@(@(@(scanr(),V{x12_19}),V{x14_19}),V{x20_19}),V{x12_19},V{x18_19}) ,R{20} -> scanr_f_z(V{x6_20},V{x7_20}) ,R{22} -> scanr_f(V{x12_22}) ,R{25} -> V{x10_25} ,R{26} -> R{26} | R{25} | @(@(@(foldl(),V{x8_26}),R{44}),V{x16_26}) | @(@(@(foldl(),V{x8_26}),R{43}),V{x16_26}) | @(@(R{29},R{44}),V{x16_26}) | @(@(R{29},R{43}),V{x16_26}) | @(R{27},V{x16_26}) | @(@(R{29},R{42}),V{x16_26}) | @(@(@(foldl(),V{x8_26}),R{42}),V{x16_26}) | @(@(R{29},@(R{46},V{x14_26})),V{x16_26}) | @(@(@(foldl(),V{x8_26}),@(R{46},V{x14_26})),V{x16_26}) | @(@(R{29},@(@(V{x8_26},V{x10_26}),V{x14_26})),V{x16_26}) | @(@(@(foldl(),V{x8_26}),@(@(V{x8_26},V{x10_26}),V{x14_26})),V{x16_26}) ,R{27} -> foldl_f_z(V{x4_27},V{x5_27}) ,R{29} -> foldl_f(V{x8_29}) ,R{31} -> 0() ,R{32} -> S(V{x10_32}) ,R{33} -> R{33} | R{32} | R{31} | @(R{35},V{x12_33}) | @(@(minus(),V{x10_33}),V{x12_33}) ,R{35} -> minus_x(V{x6_35}) ,R{37} -> V{x6_37} ,R{38} -> S(R{38}) | S(R{37}) | S(@(R{40},V{x6_38})) | S(@(@(plus(),V{x8_38}),V{x6_38})) ,R{40} -> plus_x(V{x4_40}) ,R{42} -> V{x4_42} ,R{43} -> S(V{x6_43}) ,R{44} -> S(R{44}) | S(R{43}) | S(R{42}) | S(@(R{46},V{x8_44})) | S(@(@(max(),V{x6_44}),V{x8_44})) ,R{46} -> max_x(V{x2_46}) ,R{47} -> R{26} | @(R{27},R{19}) | @(R{27},R{18}) | @(R{27},@(R{20},V{x28_47})) | @(@(R{29},0()),R{18}) | @(@(R{29},0()),R{19}) | @(@(@(foldl(),max()),0()),R{19}) | @(@(@(foldl(),max()),0()),R{18}) | @(@(R{29},0()),@(R{20},V{x28_47})) | @(R{27},@(@(R{22},0()),V{x28_47})) | @(R{27},@(@(@(scanr(),f(plus(),minus())),0()),V{x28_47})) | @(@(@(foldl(),max()),0()),@(R{20},V{x28_47})) | @(@(R{29},0()),@(@(R{22},0()),V{x28_47})) | @(@(@(foldl(),max()),0()),@(@(R{22},0()),V{x28_47})) | @(@(R{29},0()),@(@(@(scanr(),f(plus(),minus())),0()),V{x28_47})) | @(@(@(foldl(),max()),0()),@(@(@(scanr(),f(plus(),minus())),0()),V{x28_47}))} * Step 12: UncurryATRS MAYBE + Considered Problem: 3: f_x(plus(), minus(), 0()) 0() -> 0() 5: f_x(plus(), minus(), 0()) S(x1) -> S(x1) 6: f_x(plus(), minus(), M(x1)) 0() -> 0() 8: f_x(plus(), minus(), M(x2)) S(x1) -> minus() S(x1) x2 9: f_x(plus(), minus(), S(x1)) 0() -> S(x1) 11: f_x(plus(), minus(), S(x2)) S(x1) -> plus() S(x2) S(x1) 13: f(plus(), minus()) x1 -> f_x(plus(), minus(), x1) 17: cond_scanr_f_z_xs_1(Cons(x3, x2), f(plus(), minus()), x1) -> Cons(f(plus(), minus()) x1 x3, Cons(x3 , x2)) 18: scanr_f_z(f(plus(), minus()), 0()) Nil() -> Cons(0(), Nil()) 19: scanr_f_z(f(plus(), minus()), 0()) Cons(x2, x1) -> cond_scanr_f_z_xs_1(scanr() f(plus(), minus()) 0() x1 , f(plus(), minus()), x2) 20: scanr_f(f(plus(), minus())) 0() -> scanr_f_z(f(plus(), minus()), 0()) 22: scanr() f(plus(), minus()) -> scanr_f(f(plus(), minus())) 25: foldl_f_z(max(), x1) Nil() -> x1 26: foldl_f_z(max(), x3) Cons(x2, x1) -> foldl() max() (max() x3 x2) x1 27: foldl_f(max()) x1 -> foldl_f_z(max(), x1) 29: foldl() max() -> foldl_f(max()) 31: minus_x(0()) x8 -> 0() 32: minus_x(S(x10)) 0() -> S(x10) 33: minus_x(S(x2)) S(x1) -> minus() x2 x1 35: minus() x6 -> minus_x(x6) 37: plus_x(0()) S(x1) -> S(x1) 38: plus_x(S(x2)) S(x1) -> S(plus() x2 S(x1)) 40: plus() x4 -> plus_x(x4) 42: max_x(0()) x4 -> x4 43: max_x(S(x6)) 0() -> S(x6) 44: max_x(S(x2)) S(x1) -> S(max() x2 x1) 46: max() x2 -> max_x(x2) 47: main(x1) -> foldl() max() 0() (scanr() f(plus(), minus()) 0() x1) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int foldl_f :: (int -> int -> int) -> int -> int list -> int scanr_f :: (int -> int -> int) -> int -> int list -> int list f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int max_x :: int -> int -> int minus_x :: int -> int -> int plus_x :: int -> int -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int scanr_f_z :: (int -> int -> int) -> int -> int list -> int list cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl :: (int -> int -> int) -> int -> int list -> int max :: int -> int -> int minus :: int -> int -> int plus :: int -> int -> int scanr :: (int -> int -> int) -> int -> int list -> int list main :: int list -> int + Applied Processor: UncurryATRS + Details: none * Step 13: UsableRules MAYBE + Considered Problem: 1: f_x#1(plus(), minus(), 0(), 0()) -> 0() 2: f_x#1(plus(), minus(), 0(), S(x1)) -> S(x1) 3: f_x#1(plus(), minus(), M(x1), 0()) -> 0() 4: f_x#1(plus(), minus(), M(x2), S(x1)) -> minus#2(S(x1), x2) 5: f_x#1(plus(), minus(), S(x1), 0()) -> S(x1) 6: f_x#1(plus(), minus(), S(x2), S(x1)) -> plus#2(S(x2), S(x1)) 7: f#1(plus(), minus(), x1) -> f_x(plus(), minus(), x1) 8: f#2(plus(), minus(), x1, x2) -> f_x#1(plus(), minus(), x1, x2) 9: cond_scanr_f_z_xs_1(Cons(x3, x2), f(plus(), minus()), x1) -> Cons(f#2(plus(), minus(), x1, x3), Cons(x3 , x2)) 10: scanr_f_z#1(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 11: scanr_f_z#1(f(plus(), minus()), 0(), Cons(x2, x1)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()) , 0(), x1), f(plus() , minus()) , x2) 12: scanr_f#1(f(plus(), minus()), 0()) -> scanr_f_z(f(plus(), minus()), 0()) 13: scanr_f#2(f(plus(), minus()), 0(), x0) -> scanr_f_z#1(f(plus(), minus()), 0(), x0) 14: scanr#1(f(plus(), minus())) -> scanr_f(f(plus(), minus())) 15: scanr#2(f(plus(), minus()), x0) -> scanr_f#1(f(plus(), minus()), x0) 16: scanr#3(f(plus(), minus()), x0, x1) -> scanr_f#2(f(plus(), minus()), x0, x1) 17: foldl_f_z#1(max(), x1, Nil()) -> x1 18: foldl_f_z#1(max(), x3, Cons(x2, x1)) -> foldl#3(max(), max#2(x3, x2), x1) 19: foldl_f#1(max(), x1) -> foldl_f_z(max(), x1) 20: foldl_f#2(max(), x1, x2) -> foldl_f_z#1(max(), x1, x2) 21: foldl#1(max()) -> foldl_f(max()) 22: foldl#2(max(), x0) -> foldl_f#1(max(), x0) 23: foldl#3(max(), x0, x1) -> foldl_f#2(max(), x0, x1) 24: minus_x#1(0(), x8) -> 0() 25: minus_x#1(S(x10), 0()) -> S(x10) 26: minus_x#1(S(x2), S(x1)) -> minus#2(x2, x1) 27: minus#1(x6) -> minus_x(x6) 28: minus#2(x6, x7) -> minus_x#1(x6, x7) 29: plus_x#1(0(), S(x1)) -> S(x1) 30: plus_x#1(S(x2), S(x1)) -> S(plus#2(x2, S(x1))) 31: plus#1(x4) -> plus_x(x4) 32: plus#2(x4, x5) -> plus_x#1(x4, x5) 33: max_x#1(0(), x4) -> x4 34: max_x#1(S(x6), 0()) -> S(x6) 35: max_x#1(S(x2), S(x1)) -> S(max#2(x2, x1)) 36: max#1(x2) -> max_x(x2) 37: max#2(x2, x3) -> max_x#1(x2, x3) 38: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f#1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f#2 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f_x :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f_x#1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#1 :: (int -> int -> int) -> int -> int list -> int foldl#2 :: (int -> int -> int) -> int -> int list -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int foldl_f :: (int -> int -> int) -> int -> int list -> int foldl_f#1 :: (int -> int -> int) -> int -> int list -> int foldl_f#2 :: (int -> int -> int) -> int -> int list -> int foldl_f_z :: (int -> int -> int) -> int -> int list -> int foldl_f_z#1 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#1 :: int -> int -> int max#2 :: int -> int -> int max_x :: int -> int -> int max_x#1 :: int -> int -> int minus :: int -> int -> int minus#1 :: int -> int -> int minus#2 :: int -> int -> int minus_x :: int -> int -> int minus_x#1 :: int -> int -> int plus :: int -> int -> int plus#1 :: int -> int -> int plus#2 :: int -> int -> int plus_x :: int -> int -> int plus_x#1 :: int -> int -> int scanr#1 :: (int -> int -> int) -> int -> int list -> int list scanr#2 :: (int -> int -> int) -> int -> int list -> int list scanr#3 :: (int -> int -> int) -> int -> int list -> int list scanr_f :: (int -> int -> int) -> int -> int list -> int list scanr_f#1 :: (int -> int -> int) -> int -> int list -> int list scanr_f#2 :: (int -> int -> int) -> int -> int list -> int list scanr_f_z :: (int -> int -> int) -> int -> int list -> int list scanr_f_z#1 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 14: Inline MAYBE + Considered Problem: 1: f_x#1(plus(), minus(), 0(), 0()) -> 0() 2: f_x#1(plus(), minus(), 0(), S(x1)) -> S(x1) 3: f_x#1(plus(), minus(), M(x1), 0()) -> 0() 4: f_x#1(plus(), minus(), M(x2), S(x1)) -> minus#2(S(x1), x2) 5: f_x#1(plus(), minus(), S(x1), 0()) -> S(x1) 6: f_x#1(plus(), minus(), S(x2), S(x1)) -> plus#2(S(x2), S(x1)) 8: f#2(plus(), minus(), x1, x2) -> f_x#1(plus(), minus(), x1, x2) 9: cond_scanr_f_z_xs_1(Cons(x3, x2), f(plus(), minus()), x1) -> Cons(f#2(plus(), minus(), x1, x3), Cons(x3 , x2)) 10: scanr_f_z#1(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 11: scanr_f_z#1(f(plus(), minus()), 0(), Cons(x2, x1)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()) , 0(), x1), f(plus() , minus()) , x2) 13: scanr_f#2(f(plus(), minus()), 0(), x0) -> scanr_f_z#1(f(plus(), minus()), 0(), x0) 16: scanr#3(f(plus(), minus()), x0, x1) -> scanr_f#2(f(plus(), minus()), x0, x1) 17: foldl_f_z#1(max(), x1, Nil()) -> x1 18: foldl_f_z#1(max(), x3, Cons(x2, x1)) -> foldl#3(max(), max#2(x3, x2), x1) 20: foldl_f#2(max(), x1, x2) -> foldl_f_z#1(max(), x1, x2) 23: foldl#3(max(), x0, x1) -> foldl_f#2(max(), x0, x1) 24: minus_x#1(0(), x8) -> 0() 25: minus_x#1(S(x10), 0()) -> S(x10) 26: minus_x#1(S(x2), S(x1)) -> minus#2(x2, x1) 28: minus#2(x6, x7) -> minus_x#1(x6, x7) 29: plus_x#1(0(), S(x1)) -> S(x1) 30: plus_x#1(S(x2), S(x1)) -> S(plus#2(x2, S(x1))) 32: plus#2(x4, x5) -> plus_x#1(x4, x5) 33: max_x#1(0(), x4) -> x4 34: max_x#1(S(x6), 0()) -> S(x6) 35: max_x#1(S(x2), S(x1)) -> S(max#2(x2, x1)) 37: max#2(x2, x3) -> max_x#1(x2, x3) 38: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f#2 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f_x#1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int foldl_f#2 :: (int -> int -> int) -> int -> int list -> int foldl_f_z#1 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#2 :: int -> int -> int max_x#1 :: int -> int -> int minus :: int -> int -> int minus#2 :: int -> int -> int minus_x#1 :: int -> int -> int plus :: int -> int -> int plus#2 :: int -> int -> int plus_x#1 :: int -> int -> int scanr#3 :: (int -> int -> int) -> int -> int list -> int list scanr_f#2 :: (int -> int -> int) -> int -> int list -> int list scanr_f_z#1 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 15: UsableRules MAYBE + Considered Problem: 1: f_x#1(plus(), minus(), 0(), 0()) -> 0() 2: f_x#1(plus(), minus(), 0(), S(x1)) -> S(x1) 3: f_x#1(plus(), minus(), M(x1), 0()) -> 0() 4: f_x#1(plus(), minus(), M(x2), S(x1)) -> minus#2(S(x1), x2) 5: f_x#1(plus(), minus(), S(x1), 0()) -> S(x1) 6: f_x#1(plus(), minus(), S(x2), S(x1)) -> plus#2(S(x2), S(x1)) 7: f#2(plus(), minus(), 0(), 0()) -> 0() 8: f#2(plus(), minus(), 0(), S(x2)) -> S(x2) 9: f#2(plus(), minus(), M(x2), 0()) -> 0() 10: f#2(plus(), minus(), M(x4), S(x2)) -> minus#2(S(x2), x4) 11: f#2(plus(), minus(), S(x2), 0()) -> S(x2) 12: f#2(plus(), minus(), S(x4), S(x2)) -> plus#2(S(x4), S(x2)) 13: cond_scanr_f_z_xs_1(Cons(x4, x5), f(plus(), minus()), x2) -> Cons(f_x#1(plus(), minus(), x2, x4) , Cons(x4, x5)) 14: scanr_f_z#1(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 15: scanr_f_z#1(f(plus(), minus()), 0(), Cons(x2, x1)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()) , 0(), x1), f(plus() , minus()) , x2) 16: scanr_f#2(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 17: scanr_f#2(f(plus(), minus()), 0(), Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()), 0() , x2), f(plus(), minus()) , x4) 18: scanr#3(f(plus(), minus()), 0(), x0) -> scanr_f_z#1(f(plus(), minus()), 0(), x0) 19: foldl_f_z#1(max(), x1, Nil()) -> x1 20: foldl_f_z#1(max(), x3, Cons(x2, x1)) -> foldl#3(max(), max#2(x3, x2), x1) 21: foldl_f#2(max(), x2, Nil()) -> x2 22: foldl_f#2(max(), x6, Cons(x4, x2)) -> foldl#3(max(), max#2(x6, x4), x2) 23: foldl#3(max(), x2, x4) -> foldl_f_z#1(max(), x2, x4) 24: minus_x#1(0(), x8) -> 0() 25: minus_x#1(S(x10), 0()) -> S(x10) 26: minus_x#1(S(x2), S(x1)) -> minus#2(x2, x1) 27: minus#2(0(), x16) -> 0() 28: minus#2(S(x20), 0()) -> S(x20) 29: minus#2(S(x4), S(x2)) -> minus#2(x4, x2) 30: plus_x#1(0(), S(x1)) -> S(x1) 31: plus_x#1(S(x2), S(x1)) -> S(plus#2(x2, S(x1))) 32: plus#2(0(), S(x2)) -> S(x2) 33: plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) 34: max_x#1(0(), x4) -> x4 35: max_x#1(S(x6), 0()) -> S(x6) 36: max_x#1(S(x2), S(x1)) -> S(max#2(x2, x1)) 37: max#2(0(), x8) -> x8 38: max#2(S(x12), 0()) -> S(x12) 39: max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) 40: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f#2 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f_x#1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int foldl_f#2 :: (int -> int -> int) -> int -> int list -> int foldl_f_z#1 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#2 :: int -> int -> int max_x#1 :: int -> int -> int minus :: int -> int -> int minus#2 :: int -> int -> int minus_x#1 :: int -> int -> int plus :: int -> int -> int plus#2 :: int -> int -> int plus_x#1 :: int -> int -> int scanr#3 :: (int -> int -> int) -> int -> int list -> int list scanr_f#2 :: (int -> int -> int) -> int -> int list -> int list scanr_f_z#1 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 16: Inline MAYBE + Considered Problem: 1: f_x#1(plus(), minus(), 0(), 0()) -> 0() 2: f_x#1(plus(), minus(), 0(), S(x1)) -> S(x1) 3: f_x#1(plus(), minus(), M(x1), 0()) -> 0() 4: f_x#1(plus(), minus(), M(x2), S(x1)) -> minus#2(S(x1), x2) 5: f_x#1(plus(), minus(), S(x1), 0()) -> S(x1) 6: f_x#1(plus(), minus(), S(x2), S(x1)) -> plus#2(S(x2), S(x1)) 13: cond_scanr_f_z_xs_1(Cons(x4, x5), f(plus(), minus()), x2) -> Cons(f_x#1(plus(), minus(), x2, x4) , Cons(x4, x5)) 14: scanr_f_z#1(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 15: scanr_f_z#1(f(plus(), minus()), 0(), Cons(x2, x1)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()) , 0(), x1), f(plus() , minus()) , x2) 18: scanr#3(f(plus(), minus()), 0(), x0) -> scanr_f_z#1(f(plus(), minus()), 0(), x0) 19: foldl_f_z#1(max(), x1, Nil()) -> x1 20: foldl_f_z#1(max(), x3, Cons(x2, x1)) -> foldl#3(max(), max#2(x3, x2), x1) 23: foldl#3(max(), x2, x4) -> foldl_f_z#1(max(), x2, x4) 27: minus#2(0(), x16) -> 0() 28: minus#2(S(x20), 0()) -> S(x20) 29: minus#2(S(x4), S(x2)) -> minus#2(x4, x2) 32: plus#2(0(), S(x2)) -> S(x2) 33: plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) 37: max#2(0(), x8) -> x8 38: max#2(S(x12), 0()) -> S(x12) 39: max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) 40: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f_x#1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int foldl_f_z#1 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#2 :: int -> int -> int minus :: int -> int -> int minus#2 :: int -> int -> int plus :: int -> int -> int plus#2 :: int -> int -> int scanr#3 :: (int -> int -> int) -> int -> int list -> int list scanr_f_z#1 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 17: UsableRules MAYBE + Considered Problem: 1: f_x#1(plus(), minus(), 0(), 0()) -> 0() 2: f_x#1(plus(), minus(), 0(), S(x1)) -> S(x1) 3: f_x#1(plus(), minus(), M(x1), 0()) -> 0() 4: f_x#1(plus(), minus(), M(0()), S(x40)) -> S(x40) 5: f_x#1(plus(), minus(), M(S(x4)), S(x8)) -> minus#2(x8, x4) 6: f_x#1(plus(), minus(), S(x1), 0()) -> S(x1) 7: f_x#1(plus(), minus(), S(x2), S(x1)) -> plus#2(S(x2), S(x1)) 8: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), 0()) -> Cons(0(), Cons(0(), x11)) 9: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), 0()) -> Cons(S(x2), Cons(S(x2), x11)) 10: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), M(x2)) -> Cons(0(), Cons(0(), x11)) 11: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), M(x4)) -> Cons(minus#2(S(x2), x4), Cons(S(x2) , x11)) 12: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), S(x2)) -> Cons(S(x2), Cons(0(), x11)) 13: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), S(x4)) -> Cons(plus#2(S(x4), S(x2)) , Cons(S(x2), x11)) 14: scanr_f_z#1(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 15: scanr_f_z#1(f(plus(), minus()), 0(), Cons(x2, x1)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()) , 0(), x1), f(plus() , minus()) , x2) 16: scanr#3(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 17: scanr#3(f(plus(), minus()), 0(), Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()), 0() , x2), f(plus(), minus()), x4) 18: foldl_f_z#1(max(), x1, Nil()) -> x1 19: foldl_f_z#1(max(), x3, Cons(x2, x1)) -> foldl#3(max(), max#2(x3, x2), x1) 20: foldl#3(max(), x2, Nil()) -> x2 21: foldl#3(max(), x6, Cons(x4, x2)) -> foldl#3(max(), max#2(x6, 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) 25: plus#2(0(), S(x2)) -> S(x2) 26: plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) 27: max#2(0(), x8) -> x8 28: max#2(S(x12), 0()) -> S(x12) 29: max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) 30: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int f_x#1 :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int foldl_f_z#1 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#2 :: int -> int -> int minus :: int -> int -> int minus#2 :: int -> int -> int plus :: int -> int -> int plus#2 :: int -> int -> int scanr#3 :: (int -> int -> int) -> int -> int list -> int list scanr_f_z#1 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 18: Inline MAYBE + Considered Problem: 8: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), 0()) -> Cons(0(), Cons(0(), x11)) 9: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), 0()) -> Cons(S(x2), Cons(S(x2), x11)) 10: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), M(x2)) -> Cons(0(), Cons(0(), x11)) 11: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), M(x4)) -> Cons(minus#2(S(x2), x4), Cons(S(x2) , x11)) 12: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), S(x2)) -> Cons(S(x2), Cons(0(), x11)) 13: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), S(x4)) -> Cons(plus#2(S(x4), S(x2)) , Cons(S(x2), x11)) 16: scanr#3(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 17: scanr#3(f(plus(), minus()), 0(), Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()), 0() , x2), f(plus(), minus()), x4) 20: foldl#3(max(), x2, Nil()) -> x2 21: foldl#3(max(), x6, Cons(x4, x2)) -> foldl#3(max(), max#2(x6, 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) 25: plus#2(0(), S(x2)) -> S(x2) 26: plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) 27: max#2(0(), x8) -> x8 28: max#2(S(x12), 0()) -> S(x12) 29: max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) 30: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#2 :: int -> int -> int minus :: int -> int -> int minus#2 :: int -> int -> int plus :: int -> int -> int plus#2 :: int -> int -> int scanr#3 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 19: UsableRules MAYBE + Considered Problem: 1: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), 0()) -> Cons(0(), Cons(0(), x11)) 2: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), 0()) -> Cons(S(x2), Cons(S(x2), x11)) 3: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), M(x2)) -> Cons(0(), Cons(0(), x11)) 4: cond_scanr_f_z_xs_1(Cons(S(x40), x23), f(plus(), minus()), M(0())) -> Cons(S(x40), Cons(S(x40), x23)) 5: cond_scanr_f_z_xs_1(Cons(S(x8), x23), f(plus(), minus()), M(S(x4))) -> Cons(minus#2(x8, x4), Cons(S(x8) , x23)) 6: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), S(x2)) -> Cons(S(x2), Cons(0(), x11)) 7: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), S(x4)) -> Cons(plus#2(S(x4), S(x2)), Cons(S(x2) , x11)) 8: scanr#3(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 9: scanr#3(f(plus(), minus()), 0(), Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()), 0() , x2), f(plus(), minus()), x4) 10: foldl#3(max(), x2, Nil()) -> x2 11: foldl#3(max(), x6, Cons(x4, x2)) -> foldl#3(max(), max#2(x6, x4), x2) 12: minus#2(0(), x16) -> 0() 13: minus#2(S(x20), 0()) -> S(x20) 14: minus#2(S(x4), S(x2)) -> minus#2(x4, x2) 15: plus#2(0(), S(x2)) -> S(x2) 16: plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) 17: max#2(0(), x8) -> x8 18: max#2(S(x12), 0()) -> S(x12) 19: max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) 20: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#2 :: int -> int -> int minus :: int -> int -> int minus#2 :: int -> int -> int plus :: int -> int -> int plus#2 :: int -> int -> int scanr#3 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 20: UsableRules MAYBE + Considered Problem: 1: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), 0()) -> Cons(0(), Cons(0(), x11)) 2: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), 0()) -> Cons(S(x2), Cons(S(x2), x11)) 3: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), M(x2)) -> Cons(0(), Cons(0(), x11)) 4: cond_scanr_f_z_xs_1(Cons(S(x40), x23), f(plus(), minus()), M(0())) -> Cons(S(x40), Cons(S(x40), x23)) 5: cond_scanr_f_z_xs_1(Cons(S(x8), x23), f(plus(), minus()), M(S(x4))) -> Cons(minus#2(x8, x4), Cons(S(x8) , x23)) 6: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), S(x2)) -> Cons(S(x2), Cons(0(), x11)) 7: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), S(x4)) -> Cons(plus#2(S(x4), S(x2)), Cons(S(x2) , x11)) 8: scanr#3(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 9: scanr#3(f(plus(), minus()), 0(), Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()), 0() , x2), f(plus(), minus()), x4) 10: foldl#3(max(), x2, Nil()) -> x2 11: foldl#3(max(), x6, Cons(x4, x2)) -> foldl#3(max(), max#2(x6, x4), x2) 12: minus#2(0(), x16) -> 0() 13: minus#2(S(x20), 0()) -> S(x20) 14: minus#2(S(x4), S(x2)) -> minus#2(x4, x2) 15: plus#2(0(), S(x2)) -> S(x2) 16: plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) 17: max#2(0(), x8) -> x8 18: max#2(S(x12), 0()) -> S(x12) 19: max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) 20: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#2 :: int -> int -> int minus :: int -> int -> int minus#2 :: int -> int -> int plus :: int -> int -> int plus#2 :: int -> int -> int scanr#3 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 21: Compression MAYBE + Considered Problem: 1: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), 0()) -> Cons(0(), Cons(0(), x11)) 2: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), 0()) -> Cons(S(x2), Cons(S(x2), x11)) 3: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), M(x2)) -> Cons(0(), Cons(0(), x11)) 4: cond_scanr_f_z_xs_1(Cons(S(x40), x23), f(plus(), minus()), M(0())) -> Cons(S(x40), Cons(S(x40), x23)) 5: cond_scanr_f_z_xs_1(Cons(S(x8), x23), f(plus(), minus()), M(S(x4))) -> Cons(minus#2(x8, x4), Cons(S(x8) , x23)) 6: cond_scanr_f_z_xs_1(Cons(0(), x11), f(plus(), minus()), S(x2)) -> Cons(S(x2), Cons(0(), x11)) 7: cond_scanr_f_z_xs_1(Cons(S(x2), x11), f(plus(), minus()), S(x4)) -> Cons(plus#2(S(x4), S(x2)), Cons(S(x2) , x11)) 8: scanr#3(f(plus(), minus()), 0(), Nil()) -> Cons(0(), Nil()) 9: scanr#3(f(plus(), minus()), 0(), Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(f(plus(), minus()), 0() , x2), f(plus(), minus()), x4) 10: foldl#3(max(), x2, Nil()) -> x2 11: foldl#3(max(), x6, Cons(x4, x2)) -> foldl#3(max(), max#2(x6, x4), x2) 12: minus#2(0(), x16) -> 0() 13: minus#2(S(x20), 0()) -> S(x20) 14: minus#2(S(x4), S(x2)) -> minus#2(x4, x2) 15: plus#2(0(), S(x2)) -> S(x2) 16: plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) 17: max#2(0(), x8) -> x8 18: max#2(S(x12), 0()) -> S(x12) 19: max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) 20: main(x1) -> foldl#3(max(), 0(), scanr#3(f(plus(), minus()), 0(), x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> (int -> int -> int) -> int -> int list f :: (int -> int -> int) -> (int -> int -> int) -> int -> int -> int foldl#3 :: (int -> int -> int) -> int -> int list -> int main :: int list -> int max :: int -> int -> int max#2 :: int -> int -> int minus :: int -> int -> int minus#2 :: int -> int -> int plus :: int -> int -> int plus#2 :: int -> int -> int scanr#3 :: (int -> int -> int) -> int -> int list -> int list + Applied Processor: Compression + Details: none * Step 22: ToTctProblem MAYBE + Considered Problem: 1: cond_scanr_f_z_xs_1(Cons(0(), x11), 0()) -> Cons(0(), Cons(0(), x11)) 2: cond_scanr_f_z_xs_1(Cons(S(x2), x11), 0()) -> Cons(S(x2), Cons(S(x2), x11)) 3: cond_scanr_f_z_xs_1(Cons(0(), x11), M(x2)) -> Cons(0(), Cons(0(), x11)) 4: cond_scanr_f_z_xs_1(Cons(S(x40), x23), M(0())) -> Cons(S(x40), Cons(S(x40), x23)) 5: cond_scanr_f_z_xs_1(Cons(S(x8), x23), M(S(x4))) -> Cons(minus#2(x8, x4), Cons(S(x8), x23)) 6: cond_scanr_f_z_xs_1(Cons(0(), x11), S(x2)) -> Cons(S(x2), Cons(0(), x11)) 7: cond_scanr_f_z_xs_1(Cons(S(x2), x11), S(x4)) -> Cons(plus#2(S(x4), S(x2)), Cons(S(x2), x11)) 8: scanr#3(Nil()) -> Cons(0(), Nil()) 9: scanr#3(Cons(x4, x2)) -> cond_scanr_f_z_xs_1(scanr#3(x2), x4) 10: foldl#3(x2, Nil()) -> x2 11: foldl#3(x6, Cons(x4, x2)) -> foldl#3(max#2(x6, x4), x2) 12: minus#2(0(), x16) -> 0() 13: minus#2(S(x20), 0()) -> S(x20) 14: minus#2(S(x4), S(x2)) -> minus#2(x4, x2) 15: plus#2(0(), S(x2)) -> S(x2) 16: plus#2(S(x4), S(x2)) -> S(plus#2(x4, S(x2))) 17: max#2(0(), x8) -> x8 18: max#2(S(x12), 0()) -> S(x12) 19: max#2(S(x4), S(x2)) -> S(max#2(x4, x2)) 20: main(x1) -> foldl#3(0(), scanr#3(x1)) where 0 :: int Cons :: 'a -> 'a list -> 'a list M :: int -> int Nil :: 'a list S :: int -> int cond_scanr_f_z_xs_1 :: int list -> int -> int list foldl#3 :: int -> int list -> int main :: int list -> int max#2 :: int -> int -> int minus#2 :: int -> int -> int plus#2 :: int -> int -> int scanr#3 :: int list -> int list + Applied Processor: ToTctProblem + Details: none * Step 23: Failure MAYBE timed out MAYBE