WORST_CASE(?,O(n^1))
* Step 1: Desugar WORST_CASE(?,O(n^1))
    + Considered Problem:
        type bstring =
            E | Z of bstring | O of bstring
        ;;
        
        let rec flip x =
          match x with
          | E -> E
          | Z(x') -> O(flip x')
          | O(x') -> Z(flip x')
        ;;
        
    + Applied Processor:
        Desugar {analysedFunction = Nothing}
    + Details:
        none
* Step 2: Defunctionalization WORST_CASE(?,O(n^1))
    + Considered Problem:
        λx : bstring.
          (λflip : bstring -> bstring. flip x)
            (μflip : bstring -> bstring.
               λx : bstring.
                 case x of  | E -> E | Z -> λx' : bstring. O(flip x') | O -> λx' : bstring. Z(flip x')) : bstring
                                                                                                           -> bstring
        where
          E :: bstring
          O :: bstring -> bstring
          Z :: bstring -> bstring
    + Applied Processor:
        Defunctionalization
    + Details:
        none
* Step 3: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_1(x0) x1 -> x1 x0
        2: cond_flip_x(E()) -> E()
        3: cond_flip_x(Z(x2)) -> O(flip() x2)
        4: cond_flip_x(O(x2)) -> Z(flip() x2)
        5: flip_1() x1 -> cond_flip_x(x1)
        6: flip() x0 -> flip_1() x0
        7: main(x0) -> main_1(x0) flip()
        where
          E           :: bstring
          O           :: bstring -> bstring
          Z           :: bstring -> bstring
          flip_1      :: bstring -> bstring
          main_1      :: bstring -> (bstring -> bstring) -> bstring
          cond_flip_x :: bstring -> bstring
          flip        :: bstring -> bstring
          main        :: bstring -> bstring
    + Applied Processor:
        Inline {inlineType = InlineRewrite, inlineSelect = <inline non-recursive>}
    + Details:
        none
* Step 4: Inline WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_1(x0) x1 -> x1 x0
        2: cond_flip_x(E()) -> E()
        3: cond_flip_x(Z(x2)) -> O(flip() x2)
        4: cond_flip_x(O(x2)) -> Z(flip() x2)
        5: flip_1() x1 -> cond_flip_x(x1)
        6: flip() x2 -> cond_flip_x(x2)
        7: main(x0) -> flip() x0
        where
          E           :: bstring
          O           :: bstring -> bstring
          Z           :: bstring -> bstring
          flip_1      :: bstring -> bstring
          main_1      :: bstring -> (bstring -> bstring) -> bstring
          cond_flip_x :: bstring -> bstring
          flip        :: bstring -> bstring
          main        :: bstring -> bstring
    + Applied Processor:
        Inline {inlineType = InlineFull, inlineSelect = <inline case-expression>}
    + Details:
        none
* Step 5: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        1: main_1(x0) x1 -> x1 x0
        2: cond_flip_x(E()) -> E()
        3: cond_flip_x(Z(x2)) -> O(flip() x2)
        4: cond_flip_x(O(x2)) -> Z(flip() x2)
        5: flip_1() E() -> E()
        6: flip_1() Z(x4) -> O(flip() x4)
        7: flip_1() O(x4) -> Z(flip() x4)
        8: flip() E() -> E()
        9: flip() Z(x4) -> O(flip() x4)
        10: flip() O(x4) -> Z(flip() x4)
        11: main(x0) -> flip() x0
        where
          E           :: bstring
          O           :: bstring -> bstring
          Z           :: bstring -> bstring
          flip_1      :: bstring -> bstring
          main_1      :: bstring -> (bstring -> bstring) -> bstring
          cond_flip_x :: bstring -> bstring
          flip        :: bstring -> bstring
          main        :: bstring -> bstring
    + Applied Processor:
        UsableRules {urType = Syntactic}
    + Details:
        none
* Step 6: UncurryATRS WORST_CASE(?,O(n^1))
    + Considered Problem:
        8: flip() E() -> E()
        9: flip() Z(x4) -> O(flip() x4)
        10: flip() O(x4) -> Z(flip() x4)
        11: main(x0) -> flip() x0
        where
          E    :: bstring
          O    :: bstring -> bstring
          Z    :: bstring -> bstring
          flip :: bstring -> bstring
          main :: bstring -> bstring
    + Applied Processor:
        UncurryATRS
    + Details:
        none
* Step 7: 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(x0) -> flip#1(x0)
        where
          E      :: bstring
          O      :: bstring -> bstring
          Z      :: bstring -> bstring
          flip#1 :: bstring -> bstring
          main   :: bstring -> bstring
    + Applied Processor:
        UsableRules {urType = DFA}
    + Details:
        none
* Step 8: 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(x0) -> flip#1(x0)
        where
          E      :: bstring
          O      :: bstring -> bstring
          Z      :: bstring -> bstring
          flip#1 :: bstring -> bstring
          main   :: bstring -> bstring
    + Applied Processor:
        Compression
    + Details:
        none
* Step 9: 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(x0) -> flip#1(x0)
        where
          E      :: bstring
          O      :: bstring -> bstring
          Z      :: bstring -> bstring
          flip#1 :: bstring -> bstring
          main   :: bstring -> bstring
    + Applied Processor:
        ToTctProblem
    + Details:
        none
* Step 10: 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(x0) -> flip#1(x0)
        - 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(x0) = 3 + 8*x0     
                      > 4*x0         
                      = flip#1(x0)   
        
        
        Following rules are (at-least) weakly oriented:
        
* Step 11: 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(x0) -> flip#1(x0)
        - 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))