WORST_CASE(Omega(n^1),O(n^1))
* Step 1: Sum WORST_CASE(Omega(n^1),O(n^1))
    + Considered Problem:
        - Strict TRS:
            h(f(x,y)) -> f(y,f(h(h(x)),a()))
        - Signature:
            {h/1} / {a/0,f/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {h} and constructors {a,f}
    + Applied Processor:
        Sum {left = someStrategy, right = someStrategy}
    + Details:
        ()
** Step 1.a:1: DecreasingLoops WORST_CASE(Omega(n^1),?)
    + Considered Problem:
        - Strict TRS:
            h(f(x,y)) -> f(y,f(h(h(x)),a()))
        - Signature:
            {h/1} / {a/0,f/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {h} and constructors {a,f}
    + Applied Processor:
        DecreasingLoops {bound = AnyLoop, narrow = 10}
    + Details:
        The system has following decreasing Loops:
          h(x){x -> f(x,y)} =
            h(f(x,y)) ->^+ f(y,f(h(h(x)),a()))
              = C[h(x) = h(x){}]

** Step 1.b:1: MI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            h(f(x,y)) -> f(y,f(h(h(x)),a()))
        - Signature:
            {h/1} / {a/0,f/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {h} and constructors {a,f}
    + Applied Processor:
        MI {miKind = Automaton (Just 1), miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind Automaton (Just 1):
        
        
        Following symbols are considered usable:
          {h}
        TcT has computed the following interpretation:
          p(a) = [2]                            
                 [0]                            
                 [4]                            
          p(f) = [1 0 0]       [1 0 0]       [0]
                 [0 1 1] x_1 + [0 0 0] x_2 + [2]
                 [0 0 0]       [0 1 1]       [2]
          p(h) = [1 2 0]       [1]              
                 [0 0 1] x_1 + [0]              
                 [0 5 0]       [0]              
        
        Following rules are strictly oriented:
        h(f(x,y)) = [1 2 2]     [1 0 0]     [5] 
                    [0 0 0] x + [0 1 1] y + [2] 
                    [0 5 5]     [0 0 0]     [10]
                  > [1 2 2]     [1 0 0]     [4] 
                    [0 0 0] x + [0 1 1] y + [2] 
                    [0 5 5]     [0 0 0]     [10]
                  = f(y,f(h(h(x)),a()))         
        
        
        Following rules are (at-least) weakly oriented:
        
** Step 1.b:2: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            h(f(x,y)) -> f(y,f(h(h(x)),a()))
        - Signature:
            {h/1} / {a/0,f/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {h} and constructors {a,f}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(Omega(n^1),O(n^1))