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: NaturalPI 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:
        NaturalPI {shape = Mixed 2, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(mixed(2)):
        The following argument positions are considered usable:
          uargs(O) = {1},
          uargs(Z) = {1}
        
        Following symbols are considered usable:
          {flip#1,main}
        TcT has computed the following interpretation:
               p(E) = 2       
               p(O) = 2 + x1  
               p(Z) = 2 + x1  
          p(flip#1) = 4*x1    
            p(main) = 3 + 8*x1
        
        Following rules are strictly oriented:
          flip#1(E()) = 8            
                      > 2            
                      = E()          
        
        flip#1(O(x4)) = 8 + 4*x4     
                      > 2 + 4*x4     
                      = Z(flip#1(x4))
        
        flip#1(Z(x4)) = 8 + 4*x4     
                      > 2 + 4*x4     
                      = O(flip#1(x4))
        
             main(x4) = 3 + 8*x4     
                      > 4*x4         
                      = flip#1(x4)   
        
        
        Following rules are (at-least) weakly oriented:
        
* Step 13: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak 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:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^1))