WORST_CASE(?,O(n^1))
* Step 1: Desugar WORST_CASE(?,O(n^1))
    + Considered Problem:
        
        type u = E | Z of u | O of u;;
        
        let rec flip x =
          match x with
          | E -> E
          | Z(x') -> O(flip x')
          | O(x') -> Z(flip x')
        ;;
        
        let main w = flip w;;
        
        
    + Applied Processor:
        Desugar {analysedFunction = Nothing}
    + Details:
        none
* Step 2: Defunctionalization WORST_CASE(?,O(n^1))
    + Considered Problem:
        λw : u.
          (λflip : u -> u. (λmain : u -> u. main w) (λw : u. flip w))
            (μflip : u -> u. λx : u. case x of  | E -> E | Z -> λx' : u. O(flip x') | O -> λx' : u. Z(flip x')) : u -> u
        where
          E :: u
          O :: u -> u
          Z :: u -> u
    + Applied Processor:
        Defunctionalization
    + Details:
        none
* Step 3: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: main_3(x1) x2 -> x1 x2
        3: main_1(x0) x1 -> main_2(x0) main_3(x1)
        4: cond_flip_x(E()) -> E()
        5: cond_flip_x(Z(x2)) -> O(flip() x2)
        6: cond_flip_x(O(x2)) -> Z(flip() x2)
        7: flip_1() x1 -> cond_flip_x(x1)
        8: flip() x0 -> flip_1() x0
        9: main(x0) -> main_1(x0) flip()
        where
          E           :: u
          O           :: u -> u
          Z           :: u -> u
          flip_1      :: u -> u
          main_1      :: u -> (u -> u) -> u
          main_2      :: u -> (u -> u) -> u
          main_3      :: (u -> u) -> u -> u
          cond_flip_x :: u -> u
          flip        :: u -> u
          main        :: u -> u
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 4: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: main_3(x1) x2 -> x1 x2
        3: main_1(x0) x3 -> main_3(x3) x0
        4: cond_flip_x(E()) -> E()
        5: cond_flip_x(Z(x2)) -> O(flip() x2)
        6: cond_flip_x(O(x2)) -> Z(flip() x2)
        7: flip_1() x1 -> cond_flip_x(x1)
        8: flip() x2 -> cond_flip_x(x2)
        9: main(x0) -> main_2(x0) main_3(flip())
        where
          E           :: u
          O           :: u -> u
          Z           :: u -> u
          flip_1      :: u -> u
          main_1      :: u -> (u -> u) -> u
          main_2      :: u -> (u -> u) -> u
          main_3      :: (u -> u) -> u -> u
          cond_flip_x :: u -> u
          flip        :: u -> u
          main        :: u -> u
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 5: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: main_3(x1) x2 -> x1 x2
        3: main_1(x4) x2 -> x2 x4
        4: cond_flip_x(E()) -> E()
        5: cond_flip_x(Z(x2)) -> O(flip() x2)
        6: cond_flip_x(O(x2)) -> Z(flip() x2)
        7: flip_1() x1 -> cond_flip_x(x1)
        8: flip() x2 -> cond_flip_x(x2)
        9: main(x0) -> main_3(flip()) x0
        where
          E           :: u
          O           :: u -> u
          Z           :: u -> u
          flip_1      :: u -> u
          main_1      :: u -> (u -> u) -> u
          main_2      :: u -> (u -> u) -> u
          main_3      :: (u -> u) -> u -> u
          cond_flip_x :: u -> u
          flip        :: u -> u
          main        :: u -> u
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 6: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: main_3(x1) x2 -> x1 x2
        3: main_1(x4) x2 -> x2 x4
        4: cond_flip_x(E()) -> E()
        5: cond_flip_x(Z(x2)) -> O(flip() x2)
        6: cond_flip_x(O(x2)) -> Z(flip() x2)
        7: flip_1() x1 -> cond_flip_x(x1)
        8: flip() x2 -> cond_flip_x(x2)
        9: main(x4) -> flip() x4
        where
          E           :: u
          O           :: u -> u
          Z           :: u -> u
          flip_1      :: u -> u
          main_1      :: u -> (u -> u) -> u
          main_2      :: u -> (u -> u) -> u
          main_3      :: (u -> u) -> u -> u
          cond_flip_x :: u -> u
          flip        :: u -> u
          main        :: u -> u
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
    + Details:
        none
* Step 7: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_2(x0) x2 -> x2 x0
        2: main_3(x1) x2 -> x1 x2
        3: main_1(x4) x2 -> x2 x4
        4: cond_flip_x(E()) -> E()
        5: cond_flip_x(Z(x2)) -> O(flip() x2)
        6: cond_flip_x(O(x2)) -> Z(flip() x2)
        7: flip_1() E() -> E()
        8: flip_1() Z(x4) -> O(flip() x4)
        9: flip_1() O(x4) -> Z(flip() x4)
        10: flip() E() -> E()
        11: flip() Z(x4) -> O(flip() x4)
        12: flip() O(x4) -> Z(flip() x4)
        13: main(x4) -> flip() x4
        where
          E           :: u
          O           :: u -> u
          Z           :: u -> u
          flip_1      :: u -> u
          main_1      :: u -> (u -> u) -> u
          main_2      :: u -> (u -> u) -> u
          main_3      :: (u -> u) -> u -> u
          cond_flip_x :: u -> u
          flip        :: u -> u
          main        :: u -> u
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 8: UncurryATRS WORST_CASE(?,O(n^1))
    + Considered Problem:
        10: flip() E() -> E()
        11: flip() Z(x4) -> O(flip() x4)
        12: flip() O(x4) -> Z(flip() x4)
        13: main(x4) -> flip() x4
        where
          E    :: u
          O    :: u -> u
          Z    :: u -> u
          flip :: u -> u
          main :: u -> u
    + Applied Processor:
        UncurryATRS
    + Details:
        none
* Step 9: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: flip#1(E()) -> E()
        2: flip#1(Z(x4)) -> O(flip#1(x4))
        3: flip#1(O(x4)) -> Z(flip#1(x4))
        4: main(x4) -> flip#1(x4)
        where
          E      :: u
          O      :: u -> u
          Z      :: u -> u
          flip#1 :: u -> u
          main   :: u -> u
    + Applied Processor:
        UsableRules {urType = DFA}
    + Details:
        none
* Step 10: Compression WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: flip#1(E()) -> E()
        2: flip#1(Z(x4)) -> O(flip#1(x4))
        3: flip#1(O(x4)) -> Z(flip#1(x4))
        4: main(x4) -> flip#1(x4)
        where
          E      :: u
          O      :: u -> u
          Z      :: u -> u
          flip#1 :: u -> u
          main   :: u -> u
    + Applied Processor:
        Compression
    + Details:
        none
* Step 11: ToTctProblem WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: flip#1(E()) -> E()
        2: flip#1(Z(x4)) -> O(flip#1(x4))
        3: flip#1(O(x4)) -> Z(flip#1(x4))
        4: main(x4) -> flip#1(x4)
        where
          E      :: u
          O      :: u -> u
          Z      :: u -> u
          flip#1 :: u -> u
          main   :: u -> u
    + Applied Processor:
        ToTctProblem
    + Details:
        none
* Step 12: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            flip#1(E()) -> E()
            flip#1(O(x4)) -> Z(flip#1(x4))
            flip#1(Z(x4)) -> O(flip#1(x4))
            main(x4) -> flip#1(x4)
        - Signature:
            {flip#1/1,main/1} / {E/0,O/1,Z/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {main} and constructors {E,O,Z}
    + Applied Processor:
        Ara {minDegree = 1, maxDegree = 2, araTimeout = 3, araRuleShifting = Nothing}
    + Details:
        Signatures used:
        ----------------
          F (TrsFun "E") :: [] -(0)-> "A"(1)
          F (TrsFun "E") :: [] -(0)-> "A"(0)
          F (TrsFun "O") :: ["A"(1)] -(1)-> "A"(1)
          F (TrsFun "O") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "Z") :: ["A"(1)] -(1)-> "A"(1)
          F (TrsFun "Z") :: ["A"(0)] -(0)-> "A"(0)
          F (TrsFun "flip#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))