WORST_CASE(?,O(n^1)) * Step 1: Desugar WORST_CASE(?,O(n^1)) + Considered Problem: type nat = 0 | S of nat;; type bool = True | False ;; let rec even x = match x with | 0 -> True | S(x') -> odd x' and odd x = match x with | 0 -> False | S(x') -> even x' ;; let main x = even x ;; + Applied Processor: Desugar {analysedFunction = Nothing} + Details: none * Step 2: Defunctionalization WORST_CASE(?,O(n^1)) + Considered Problem: λx : nat. (λeven : nat -> bool. λodd : nat -> bool. (λmain : nat -> bool. main x) (λx : nat. even x)) (μ0 [λeven : nat -> bool. λodd : nat -> bool. λx : nat. case x of | 0 -> True | S -> λx' : nat. odd x' ,λeven : nat -> bool. λodd : nat -> bool. λx : nat. case x of | 0 -> False | S -> λx' : nat. even x']) (μ1 [λeven : nat -> bool. λodd : nat -> bool. λx : nat. case x of | 0 -> True | S -> λx' : nat. odd x' ,λeven : nat -> bool. λodd : nat -> bool. λx : nat. case x of | 0 -> False | S -> λx' : nat. even x']) : nat -> bool where 0 :: nat False :: bool S :: nat -> nat True :: bool + Applied Processor: Defunctionalization + Details: none * Step 3: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: main_4(x1) x3 -> x1 x3 3: main_2(x0, x1) x2 -> main_3(x0) main_4(x1) 4: main_1(x0) x1 -> main_2(x0, x1) 5: cond_odd_x(0()) -> False() 6: cond_odd_x(S(x4)) -> even() x4 7: odd_2() x3 -> cond_odd_x(x3) 8: odd() x0 -> odd_2() x0 9: cond_even_x(0()) -> True() 10: cond_even_x(S(x2)) -> odd() x2 11: even_2() x1 -> cond_even_x(x1) 12: even() x0 -> even_2() x0 13: cond_even_x_1(0()) -> True() 14: cond_even_x_1(S(x4)) -> odd_3() x4 15: even_5() x3 -> cond_even_x_1(x3) 16: even_3() x0 -> even_5() x0 17: cond_odd_x_1(0()) -> False() 18: cond_odd_x_1(S(x2)) -> even_3() x2 19: odd_5() x1 -> cond_odd_x_1(x1) 20: odd_3() x0 -> odd_5() x0 21: main(x0) -> main_1(x0) even() odd_3() where 0 :: nat False :: bool S :: nat -> nat True :: bool main_1 :: nat -> (nat -> bool) -> (nat -> bool) -> bool even_2 :: nat -> bool main_2 :: nat -> (nat -> bool) -> (nat -> bool) -> bool odd_2 :: nat -> bool main_3 :: nat -> (nat -> bool) -> bool main_4 :: (nat -> bool) -> nat -> bool even_5 :: nat -> bool odd_5 :: nat -> bool cond_even_x :: nat -> bool cond_odd_x :: nat -> bool cond_even_x_1 :: nat -> bool cond_odd_x_1 :: nat -> bool even :: nat -> bool odd :: nat -> bool even_3 :: nat -> bool odd_3 :: nat -> bool main :: nat -> bool + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 4: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: main_4(x1) x3 -> x1 x3 3: main_2(x0, x3) x5 -> main_4(x3) x0 4: main_1(x0) x1 -> main_2(x0, x1) 5: cond_odd_x(0()) -> False() 6: cond_odd_x(S(x4)) -> even() x4 7: odd_2() x3 -> cond_odd_x(x3) 8: odd() x6 -> cond_odd_x(x6) 9: cond_even_x(0()) -> True() 10: cond_even_x(S(x2)) -> odd() x2 11: even_2() x1 -> cond_even_x(x1) 12: even() x2 -> cond_even_x(x2) 13: cond_even_x_1(0()) -> True() 14: cond_even_x_1(S(x4)) -> odd_3() x4 15: even_5() x3 -> cond_even_x_1(x3) 16: even_3() x6 -> cond_even_x_1(x6) 17: cond_odd_x_1(0()) -> False() 18: cond_odd_x_1(S(x2)) -> even_3() x2 19: odd_5() x1 -> cond_odd_x_1(x1) 20: odd_3() x2 -> cond_odd_x_1(x2) 21: main(x0) -> main_2(x0, even()) odd_3() where 0 :: nat False :: bool S :: nat -> nat True :: bool main_1 :: nat -> (nat -> bool) -> (nat -> bool) -> bool even_2 :: nat -> bool main_2 :: nat -> (nat -> bool) -> (nat -> bool) -> bool odd_2 :: nat -> bool main_3 :: nat -> (nat -> bool) -> bool main_4 :: (nat -> bool) -> nat -> bool even_5 :: nat -> bool odd_5 :: nat -> bool cond_even_x :: nat -> bool cond_odd_x :: nat -> bool cond_even_x_1 :: nat -> bool cond_odd_x_1 :: nat -> bool even :: nat -> bool odd :: nat -> bool even_3 :: nat -> bool odd_3 :: nat -> bool main :: nat -> bool + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 5: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: main_4(x1) x3 -> x1 x3 3: main_2(x6, x2) x11 -> x2 x6 4: main_1(x0) x1 -> main_2(x0, x1) 5: cond_odd_x(0()) -> False() 6: cond_odd_x(S(x4)) -> even() x4 7: odd_2() x3 -> cond_odd_x(x3) 8: odd() x6 -> cond_odd_x(x6) 9: cond_even_x(0()) -> True() 10: cond_even_x(S(x2)) -> odd() x2 11: even_2() x1 -> cond_even_x(x1) 12: even() x2 -> cond_even_x(x2) 13: cond_even_x_1(0()) -> True() 14: cond_even_x_1(S(x4)) -> odd_3() x4 15: even_5() x3 -> cond_even_x_1(x3) 16: even_3() x6 -> cond_even_x_1(x6) 17: cond_odd_x_1(0()) -> False() 18: cond_odd_x_1(S(x2)) -> even_3() x2 19: odd_5() x1 -> cond_odd_x_1(x1) 20: odd_3() x2 -> cond_odd_x_1(x2) 21: main(x0) -> main_4(even()) x0 where 0 :: nat False :: bool S :: nat -> nat True :: bool main_1 :: nat -> (nat -> bool) -> (nat -> bool) -> bool even_2 :: nat -> bool main_2 :: nat -> (nat -> bool) -> (nat -> bool) -> bool odd_2 :: nat -> bool main_3 :: nat -> (nat -> bool) -> bool main_4 :: (nat -> bool) -> nat -> bool even_5 :: nat -> bool odd_5 :: nat -> bool cond_even_x :: nat -> bool cond_odd_x :: nat -> bool cond_even_x_1 :: nat -> bool cond_odd_x_1 :: nat -> bool even :: nat -> bool odd :: nat -> bool even_3 :: nat -> bool odd_3 :: nat -> bool main :: nat -> bool + Applied Processor: Inline {inlineType = InlineRewrite, inlineSelect = } + Details: none * Step 6: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: main_4(x1) x3 -> x1 x3 3: main_2(x6, x2) x11 -> x2 x6 4: main_1(x0) x1 -> main_2(x0, x1) 5: cond_odd_x(0()) -> False() 6: cond_odd_x(S(x4)) -> even() x4 7: odd_2() x3 -> cond_odd_x(x3) 8: odd() x6 -> cond_odd_x(x6) 9: cond_even_x(0()) -> True() 10: cond_even_x(S(x2)) -> odd() x2 11: even_2() x1 -> cond_even_x(x1) 12: even() x2 -> cond_even_x(x2) 13: cond_even_x_1(0()) -> True() 14: cond_even_x_1(S(x4)) -> odd_3() x4 15: even_5() x3 -> cond_even_x_1(x3) 16: even_3() x6 -> cond_even_x_1(x6) 17: cond_odd_x_1(0()) -> False() 18: cond_odd_x_1(S(x2)) -> even_3() x2 19: odd_5() x1 -> cond_odd_x_1(x1) 20: odd_3() x2 -> cond_odd_x_1(x2) 21: main(x6) -> even() x6 where 0 :: nat False :: bool S :: nat -> nat True :: bool main_1 :: nat -> (nat -> bool) -> (nat -> bool) -> bool even_2 :: nat -> bool main_2 :: nat -> (nat -> bool) -> (nat -> bool) -> bool odd_2 :: nat -> bool main_3 :: nat -> (nat -> bool) -> bool main_4 :: (nat -> bool) -> nat -> bool even_5 :: nat -> bool odd_5 :: nat -> bool cond_even_x :: nat -> bool cond_odd_x :: nat -> bool cond_even_x_1 :: nat -> bool cond_odd_x_1 :: nat -> bool even :: nat -> bool odd :: nat -> bool even_3 :: nat -> bool odd_3 :: nat -> bool main :: nat -> bool + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 7: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: main_3(x0) x3 -> x3 x0 2: main_4(x1) x3 -> x1 x3 3: main_2(x6, x2) x11 -> x2 x6 4: main_1(x0) x1 -> main_2(x0, x1) 5: cond_odd_x(0()) -> False() 6: cond_odd_x(S(x4)) -> even() x4 7: odd_2() 0() -> False() 8: odd_2() S(x8) -> even() x8 9: odd() 0() -> False() 10: odd() S(x8) -> even() x8 11: cond_even_x(0()) -> True() 12: cond_even_x(S(x2)) -> odd() x2 13: even_2() 0() -> True() 14: even_2() S(x4) -> odd() x4 15: even() 0() -> True() 16: even() S(x4) -> odd() x4 17: cond_even_x_1(0()) -> True() 18: cond_even_x_1(S(x4)) -> odd_3() x4 19: even_5() 0() -> True() 20: even_5() S(x8) -> odd_3() x8 21: even_3() 0() -> True() 22: even_3() S(x8) -> odd_3() x8 23: cond_odd_x_1(0()) -> False() 24: cond_odd_x_1(S(x2)) -> even_3() x2 25: odd_5() 0() -> False() 26: odd_5() S(x4) -> even_3() x4 27: odd_3() 0() -> False() 28: odd_3() S(x4) -> even_3() x4 29: main(x6) -> even() x6 where 0 :: nat False :: bool S :: nat -> nat True :: bool main_1 :: nat -> (nat -> bool) -> (nat -> bool) -> bool even_2 :: nat -> bool main_2 :: nat -> (nat -> bool) -> (nat -> bool) -> bool odd_2 :: nat -> bool main_3 :: nat -> (nat -> bool) -> bool main_4 :: (nat -> bool) -> nat -> bool even_5 :: nat -> bool odd_5 :: nat -> bool cond_even_x :: nat -> bool cond_odd_x :: nat -> bool cond_even_x_1 :: nat -> bool cond_odd_x_1 :: nat -> bool even :: nat -> bool odd :: nat -> bool even_3 :: nat -> bool odd_3 :: nat -> bool main :: nat -> bool + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 8: UncurryATRS WORST_CASE(?,O(n^1)) + Considered Problem: 9: odd() 0() -> False() 10: odd() S(x8) -> even() x8 15: even() 0() -> True() 16: even() S(x4) -> odd() x4 29: main(x6) -> even() x6 where 0 :: nat False :: bool S :: nat -> nat True :: bool even :: nat -> bool odd :: nat -> bool main :: nat -> bool + Applied Processor: UncurryATRS + Details: none * Step 9: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: odd#1(0()) -> False() 2: odd#1(S(x8)) -> even#1(x8) 3: even#1(0()) -> True() 4: even#1(S(x4)) -> odd#1(x4) 5: main(x6) -> even#1(x6) where 0 :: nat False :: bool S :: nat -> nat True :: bool even#1 :: nat -> bool main :: nat -> bool odd#1 :: nat -> bool + Applied Processor: UsableRules {urType = DFA} + Details: none * Step 10: Inline WORST_CASE(?,O(n^1)) + Considered Problem: 1: odd#1(0()) -> False() 2: odd#1(S(x8)) -> even#1(x8) 3: even#1(0()) -> True() 4: even#1(S(x4)) -> odd#1(x4) 5: main(x6) -> even#1(x6) where 0 :: nat False :: bool S :: nat -> nat True :: bool even#1 :: nat -> bool main :: nat -> bool odd#1 :: nat -> bool + Applied Processor: Inline {inlineType = InlineFull, inlineSelect = } + Details: none * Step 11: UsableRules WORST_CASE(?,O(n^1)) + Considered Problem: 1: odd#1(0()) -> False() 2: odd#1(S(x8)) -> even#1(x8) 3: even#1(0()) -> True() 4: even#1(S(0())) -> False() 5: even#1(S(S(x16))) -> even#1(x16) 6: main(x6) -> even#1(x6) where 0 :: nat False :: bool S :: nat -> nat True :: bool even#1 :: nat -> bool main :: nat -> bool odd#1 :: nat -> bool + Applied Processor: UsableRules {urType = Syntactic} + Details: none * Step 12: Compression WORST_CASE(?,O(n^1)) + Considered Problem: 3: even#1(0()) -> True() 4: even#1(S(0())) -> False() 5: even#1(S(S(x16))) -> even#1(x16) 6: main(x6) -> even#1(x6) where 0 :: nat False :: bool S :: nat -> nat True :: bool even#1 :: nat -> bool main :: nat -> bool + Applied Processor: Compression + Details: none * Step 13: ToTctProblem WORST_CASE(?,O(n^1)) + Considered Problem: 1: even#1(0()) -> True() 2: even#1(S(0())) -> False() 3: even#1(S(S(x16))) -> even#1(x16) 4: main(x6) -> even#1(x6) where 0 :: nat False :: bool S :: nat -> nat True :: bool even#1 :: nat -> bool main :: nat -> bool + Applied Processor: ToTctProblem + Details: none * Step 14: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even#1(0()) -> True() even#1(S(0())) -> False() even#1(S(S(x16))) -> even#1(x16) main(x6) -> even#1(x6) - Signature: {even#1/1,main/1} / {0/0,False/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,False,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: none Following symbols are considered usable: {even#1,main} TcT has computed the following interpretation: p(0) = 1 p(False) = 13 p(S) = x1 p(True) = 0 p(even#1) = 13*x1 p(main) = 13*x1 Following rules are strictly oriented: even#1(0()) = 13 > 0 = True() Following rules are (at-least) weakly oriented: even#1(S(0())) = 13 >= 13 = False() even#1(S(S(x16))) = 13*x16 >= 13*x16 = even#1(x16) main(x6) = 13*x6 >= 13*x6 = even#1(x6) * Step 15: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even#1(S(0())) -> False() even#1(S(S(x16))) -> even#1(x16) main(x6) -> even#1(x6) - Weak TRS: even#1(0()) -> True() - Signature: {even#1/1,main/1} / {0/0,False/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,False,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: none Following symbols are considered usable: {even#1,main} TcT has computed the following interpretation: p(0) = 8 p(False) = 0 p(S) = 2 p(True) = 0 p(even#1) = 0 p(main) = 1 Following rules are strictly oriented: main(x6) = 1 > 0 = even#1(x6) Following rules are (at-least) weakly oriented: even#1(0()) = 0 >= 0 = True() even#1(S(0())) = 0 >= 0 = False() even#1(S(S(x16))) = 0 >= 0 = even#1(x16) * Step 16: NaturalMI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even#1(S(0())) -> False() even#1(S(S(x16))) -> even#1(x16) - Weak TRS: even#1(0()) -> True() main(x6) -> even#1(x6) - Signature: {even#1/1,main/1} / {0/0,False/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,False,S,True} + Applied Processor: NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a matrix interpretation of kind constructor based matrix interpretation: The following argument positions are considered usable: none Following symbols are considered usable: {even#1,main} TcT has computed the following interpretation: p(0) = [0] p(False) = [0] p(S) = [15] p(True) = [8] p(even#1) = [8] p(main) = [8] Following rules are strictly oriented: even#1(S(0())) = [8] > [0] = False() Following rules are (at-least) weakly oriented: even#1(0()) = [8] >= [8] = True() even#1(S(S(x16))) = [8] >= [8] = even#1(x16) main(x6) = [8] >= [8] = even#1(x6) * Step 17: NaturalPI WORST_CASE(?,O(n^1)) + Considered Problem: - Strict TRS: even#1(S(S(x16))) -> even#1(x16) - Weak TRS: even#1(0()) -> True() even#1(S(0())) -> False() main(x6) -> even#1(x6) - Signature: {even#1/1,main/1} / {0/0,False/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,False,S,True} + Applied Processor: NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules} + Details: We apply a polynomial interpretation of kind constructor-based(linear): The following argument positions are considered usable: none Following symbols are considered usable: {even#1,main} TcT has computed the following interpretation: p(0) = 6 p(False) = 11 p(S) = 3 + x1 p(True) = 0 p(even#1) = 2*x1 p(main) = 2*x1 Following rules are strictly oriented: even#1(S(S(x16))) = 12 + 2*x16 > 2*x16 = even#1(x16) Following rules are (at-least) weakly oriented: even#1(0()) = 12 >= 0 = True() even#1(S(0())) = 18 >= 11 = False() main(x6) = 2*x6 >= 2*x6 = even#1(x6) * Step 18: EmptyProcessor WORST_CASE(?,O(1)) + Considered Problem: - Weak TRS: even#1(0()) -> True() even#1(S(0())) -> False() even#1(S(S(x16))) -> even#1(x16) main(x6) -> even#1(x6) - Signature: {even#1/1,main/1} / {0/0,False/0,S/1,True/0} - Obligation: innermost runtime complexity wrt. defined symbols {main} and constructors {0,False,S,True} + Applied Processor: EmptyProcessor + Details: The problem is already closed. The intended complexity is O(1). WORST_CASE(?,O(n^1))