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: Ara 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: Ara {minDegree = 1, maxDegree = 2, araTimeout = 5, araRuleShifting = Nothing} + Details: Signatures used: ---------------- F (TrsFun "0") :: [] -(0)-> "A"(1) F (TrsFun "False") :: [] -(0)-> "A"(0) F (TrsFun "S") :: ["A"(1)] -(1)-> "A"(1) F (TrsFun "True") :: [] -(0)-> "A"(0) F (TrsFun "even#1") :: ["A"(1)] -(1)-> "A"(0) F (TrsFun "main") :: ["A"(1)] -(2)-> "A"(0) Cost-free Signatures used: -------------------------- Base Constructor Signatures used: --------------------------------- WORST_CASE(?,O(n^1))