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

** Step 1.b:1: DependencyPairs WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(a(),a()) -> f(a(),b())
            f(a(),b()) -> f(s(a()),c())
            f(c(),c()) -> f(a(),a())
            f(s(X),c()) -> f(X,c())
        - Signature:
            {f/2} / {a/0,b/0,c/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f} and constructors {a,b,c,s}
    + Applied Processor:
        DependencyPairs {dpKind_ = DT}
    + Details:
        We add the following dependency tuples:
        
        Strict DPs
          f#(a(),a()) -> c_1(f#(a(),b()))
          f#(a(),b()) -> c_2(f#(s(a()),c()))
          f#(c(),c()) -> c_3(f#(a(),a()))
          f#(s(X),c()) -> c_4(f#(X,c()))
        Weak DPs
          
        
        and mark the set of starting terms.
** Step 1.b:2: UsableRules WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            f#(a(),a()) -> c_1(f#(a(),b()))
            f#(a(),b()) -> c_2(f#(s(a()),c()))
            f#(c(),c()) -> c_3(f#(a(),a()))
            f#(s(X),c()) -> c_4(f#(X,c()))
        - Weak TRS:
            f(a(),a()) -> f(a(),b())
            f(a(),b()) -> f(s(a()),c())
            f(c(),c()) -> f(a(),a())
            f(s(X),c()) -> f(X,c())
        - Signature:
            {f/2,f#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#} and constructors {a,b,c,s}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          f#(a(),a()) -> c_1(f#(a(),b()))
          f#(a(),b()) -> c_2(f#(s(a()),c()))
          f#(c(),c()) -> c_3(f#(a(),a()))
          f#(s(X),c()) -> c_4(f#(X,c()))
** Step 1.b:3: WeightGap WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            f#(a(),a()) -> c_1(f#(a(),b()))
            f#(a(),b()) -> c_2(f#(s(a()),c()))
            f#(c(),c()) -> c_3(f#(a(),a()))
            f#(s(X),c()) -> c_4(f#(X,c()))
        - Signature:
            {f/2,f#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#} and constructors {a,b,c,s}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        The weightgap principle applies using the following constant growth matrix-interpretation:
          We apply a matrix interpretation of kind constructor based matrix interpretation:
          The following argument positions are considered usable:
            uargs(c_1) = {1},
            uargs(c_2) = {1},
            uargs(c_3) = {1},
            uargs(c_4) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
              p(a) = [3]                  
              p(b) = [0]                  
              p(c) = [1]                  
              p(f) = [1] x1 + [1] x2 + [0]
              p(s) = [1] x1 + [2]         
             p(f#) = [5] x1 + [2] x2 + [4]
            p(c_1) = [1] x1 + [0]         
            p(c_2) = [1] x1 + [0]         
            p(c_3) = [1] x1 + [0]         
            p(c_4) = [1] x1 + [0]         
          
          Following rules are strictly oriented:
           f#(a(),a()) = [25]            
                       > [19]            
                       = c_1(f#(a(),b()))
          
          f#(s(X),c()) = [5] X + [16]    
                       > [5] X + [6]     
                       = c_4(f#(X,c()))  
          
          
          Following rules are (at-least) weakly oriented:
          f#(a(),b()) =  [19]               
                      >= [31]               
                      =  c_2(f#(s(a()),c()))
          
          f#(c(),c()) =  [11]               
                      >= [25]               
                      =  c_3(f#(a(),a()))   
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:4: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            f#(a(),b()) -> c_2(f#(s(a()),c()))
            f#(c(),c()) -> c_3(f#(a(),a()))
        - Weak DPs:
            f#(a(),a()) -> c_1(f#(a(),b()))
            f#(s(X),c()) -> c_4(f#(X,c()))
        - Signature:
            {f/2,f#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#} and constructors {a,b,c,s}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_2) = {1},
          uargs(c_3) = {1},
          uargs(c_4) = {1}
        
        Following symbols are considered usable:
          {f#}
        TcT has computed the following interpretation:
            p(a) = [0]         
            p(b) = [1]         
            p(c) = [1]         
            p(f) = [4] x2 + [0]
            p(s) = [1] x1 + [0]
           p(f#) = [8] x1 + [0]
          p(c_1) = [2] x1 + [0]
          p(c_2) = [4] x1 + [0]
          p(c_3) = [4] x1 + [6]
          p(c_4) = [1] x1 + [0]
        
        Following rules are strictly oriented:
        f#(c(),c()) = [8]             
                    > [6]             
                    = c_3(f#(a(),a()))
        
        
        Following rules are (at-least) weakly oriented:
         f#(a(),a()) =  [0]                
                     >= [0]                
                     =  c_1(f#(a(),b()))   
        
         f#(a(),b()) =  [0]                
                     >= [0]                
                     =  c_2(f#(s(a()),c()))
        
        f#(s(X),c()) =  [8] X + [0]        
                     >= [8] X + [0]        
                     =  c_4(f#(X,c()))     
        
** Step 1.b:5: MI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            f#(a(),b()) -> c_2(f#(s(a()),c()))
        - Weak DPs:
            f#(a(),a()) -> c_1(f#(a(),b()))
            f#(c(),c()) -> c_3(f#(a(),a()))
            f#(s(X),c()) -> c_4(f#(X,c()))
        - Signature:
            {f/2,f#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#} and constructors {a,b,c,s}
    + Applied Processor:
        MI {miKind = Automaton Nothing, miDimension = 2, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind Automaton Nothing:
        
        The following argument positions are considered usable:
          uargs(c_1) = {1},
          uargs(c_2) = {1},
          uargs(c_3) = {1},
          uargs(c_4) = {1}
        
        Following symbols are considered usable:
          {f#}
        TcT has computed the following interpretation:
            p(a) = [0]                        
                   [4]                        
            p(b) = [0]                        
                   [1]                        
            p(c) = [2]                        
                   [0]                        
            p(f) = [1 1] x_2 + [0]            
                   [2 0]       [1]            
            p(s) = [1 0] x_1 + [0]            
                   [0 1]       [11]           
           p(f#) = [8 0] x_1 + [0 2] x_2 + [0]
                   [8 0]       [0 0]       [3]
          p(c_1) = [4 0] x_1 + [0]            
                   [0 0]       [3]            
          p(c_2) = [8 0] x_1 + [1]            
                   [0 0]       [0]            
          p(c_3) = [2 0] x_1 + [0]            
                   [2 0]       [3]            
          p(c_4) = [1 0] x_1 + [0]            
                   [0 1]       [0]            
        
        Following rules are strictly oriented:
        f#(a(),b()) = [2]                
                      [3]                
                    > [1]                
                      [0]                
                    = c_2(f#(s(a()),c()))
        
        
        Following rules are (at-least) weakly oriented:
         f#(a(),a()) =  [8]             
                        [3]             
                     >= [8]             
                        [3]             
                     =  c_1(f#(a(),b()))
        
         f#(c(),c()) =  [16]            
                        [19]            
                     >= [16]            
                        [19]            
                     =  c_3(f#(a(),a()))
        
        f#(s(X),c()) =  [8 0] X + [0]   
                        [8 0]     [3]   
                     >= [8 0] X + [0]   
                        [8 0]     [3]   
                     =  c_4(f#(X,c()))  
        
** Step 1.b:6: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            f#(a(),a()) -> c_1(f#(a(),b()))
            f#(a(),b()) -> c_2(f#(s(a()),c()))
            f#(c(),c()) -> c_3(f#(a(),a()))
            f#(s(X),c()) -> c_4(f#(X,c()))
        - Signature:
            {f/2,f#/2} / {a/0,b/0,c/0,s/1,c_1/1,c_2/1,c_3/1,c_4/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f#} and constructors {a,b,c,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

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