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

** Step 1.b:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(x) -> x
            f(c(s(x),y)) -> f(c(x,s(y)))
            f(f(x)) -> f(d(f(x)))
            g(c(x,s(y))) -> g(c(s(x),y))
        - Signature:
            {f/1,g/1} / {c/2,d/1,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,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:
          none
        
        Following symbols are considered usable:
          {f,g}
        TcT has computed the following interpretation:
          p(c) = [0]         
          p(d) = [4]         
          p(f) = [2] x1 + [4]
          p(g) = [0]         
          p(s) = [1]         
        
        Following rules are strictly oriented:
        f(x) = [2] x + [4]
             > [1] x + [0]
             = x          
        
        
        Following rules are (at-least) weakly oriented:
        f(c(s(x),y)) =  [4]         
                     >= [4]         
                     =  f(c(x,s(y)))
        
             f(f(x)) =  [4] x + [12]
                     >= [12]        
                     =  f(d(f(x)))  
        
        g(c(x,s(y))) =  [0]         
                     >= [0]         
                     =  g(c(s(x),y))
        
** Step 1.b:2: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(c(s(x),y)) -> f(c(x,s(y)))
            f(f(x)) -> f(d(f(x)))
            g(c(x,s(y))) -> g(c(s(x),y))
        - Weak TRS:
            f(x) -> x
        - Signature:
            {f/1,g/1} / {c/2,d/1,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,s}
    + Applied Processor:
        NaturalPI {shape = Linear, restrict = Restrict, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        We apply a polynomial interpretation of kind constructor-based(linear):
        The following argument positions are considered usable:
          none
        
        Following symbols are considered usable:
          {f,g}
        TcT has computed the following interpretation:
          p(c) = x1    
          p(d) = 0     
          p(f) = 2*x1  
          p(g) = 10    
          p(s) = 8 + x1
        
        Following rules are strictly oriented:
        f(c(s(x),y)) = 16 + 2*x    
                     > 2*x         
                     = f(c(x,s(y)))
        
        
        Following rules are (at-least) weakly oriented:
                f(x) =  2*x         
                     >= x           
                     =  x           
        
             f(f(x)) =  4*x         
                     >= 0           
                     =  f(d(f(x)))  
        
        g(c(x,s(y))) =  10          
                     >= 10          
                     =  g(c(s(x),y))
        
** Step 1.b:3: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            f(f(x)) -> f(d(f(x)))
            g(c(x,s(y))) -> g(c(s(x),y))
        - Weak TRS:
            f(x) -> x
            f(c(s(x),y)) -> f(c(x,s(y)))
        - Signature:
            {f/1,g/1} / {c/2,d/1,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,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:
          none
        
        Following symbols are considered usable:
          {f,g}
        TcT has computed the following interpretation:
          p(c) = [1] x1 + [5]
          p(d) = [2]         
          p(f) = [1] x1 + [6]
          p(g) = [1] x1 + [0]
          p(s) = [1] x1 + [0]
        
        Following rules are strictly oriented:
        f(f(x)) = [1] x + [12]
                > [8]         
                = f(d(f(x)))  
        
        
        Following rules are (at-least) weakly oriented:
                f(x) =  [1] x + [6] 
                     >= [1] x + [0] 
                     =  x           
        
        f(c(s(x),y)) =  [1] x + [11]
                     >= [1] x + [11]
                     =  f(c(x,s(y)))
        
        g(c(x,s(y))) =  [1] x + [5] 
                     >= [1] x + [5] 
                     =  g(c(s(x),y))
        
** Step 1.b:4: Ara WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            g(c(x,s(y))) -> g(c(s(x),y))
        - Weak TRS:
            f(x) -> x
            f(c(s(x),y)) -> f(c(x,s(y)))
            f(f(x)) -> f(d(f(x)))
        - Signature:
            {f/1,g/1} / {c/2,d/1,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {f,g} and constructors {c,d,s}
    + Applied Processor:
        Ara {araHeuristics = NoHeuristics, minDegree = 1, maxDegree = 1, araTimeout = 8, araRuleShifting = Just 1}
    + Details:
        Signatures used:
        ----------------
          c :: ["A"(0) x "A"(3)] -(3)-> "A"(3)
          c :: ["A"(0) x "A"(0)] -(0)-> "A"(0)
          d :: ["A"(0)] -(0)-> "A"(4)
          f :: ["A"(0)] -(3)-> "A"(0)
          g :: ["A"(3)] -(7)-> "A"(14)
          s :: ["A"(3)] -(3)-> "A"(3)
          s :: ["A"(0)] -(0)-> "A"(0)
        
        
        Cost-free Signatures used:
        --------------------------
        
        
        
        Base Constructor Signatures used:
        ---------------------------------
          "c_A" :: ["A"(0) x "A"(1)] -(1)-> "A"(1)
          "d_A" :: ["A"(0)] -(0)-> "A"(1)
          "s_A" :: ["A"(1)] -(1)-> "A"(1)
        
        
        Following Still Strict Rules were Typed as:
        -------------------------------------------
        1. Strict:
          g(c(x,s(y))) -> g(c(s(x),y))
        2. Weak:
          

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