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

** Step 1.b:1: DependencyPairs.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            SQR(z0) -> c4()
            SUM(0()) -> c()
            SUM(s(z0)) -> c1(SQR(s(z0)))
            SUM(s(z0)) -> c2(SUM(z0))
            SUM(s(z0)) -> c3(SUM(z0))
        - Weak TRS:
            sqr(z0) -> *(z0,z0)
            sum(0()) -> 0()
            sum(s(z0)) -> +(*(s(z0),s(z0)),sum(z0))
            sum(s(z0)) -> +(sqr(s(z0)),sum(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR,SUM,sqr,sum} and constructors {*,+,0,c,c1,c2,c3,c4,s}
    + Applied Processor:
        DependencyPairs {dpKind_ = WIDP}
    + Details:
        We add the following weak innermost dependency pairs:
        
        Strict DPs
          SQR#(z0) -> c_1()
          SUM#(0()) -> c_2()
          SUM#(s(z0)) -> c_3(SQR#(s(z0)))
          SUM#(s(z0)) -> c_4(SUM#(z0))
          SUM#(s(z0)) -> c_5(SUM#(z0))
        Weak DPs
          sqr#(z0) -> c_6()
          sum#(0()) -> c_7()
          sum#(s(z0)) -> c_8(sum#(z0))
          sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
        
        and mark the set of starting terms.
** Step 1.b:2: UsableRules.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            SQR#(z0) -> c_1()
            SUM#(0()) -> c_2()
            SUM#(s(z0)) -> c_3(SQR#(s(z0)))
            SUM#(s(z0)) -> c_4(SUM#(z0))
            SUM#(s(z0)) -> c_5(SUM#(z0))
        - Strict TRS:
            SQR(z0) -> c4()
            SUM(0()) -> c()
            SUM(s(z0)) -> c1(SQR(s(z0)))
            SUM(s(z0)) -> c2(SUM(z0))
            SUM(s(z0)) -> c3(SUM(z0))
        - Weak DPs:
            sqr#(z0) -> c_6()
            sum#(0()) -> c_7()
            sum#(s(z0)) -> c_8(sum#(z0))
            sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
        - Weak TRS:
            sqr(z0) -> *(z0,z0)
            sum(0()) -> 0()
            sum(s(z0)) -> +(*(s(z0),s(z0)),sum(z0))
            sum(s(z0)) -> +(sqr(s(z0)),sum(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        UsableRules
    + Details:
        We replace rewrite rules by usable rules:
          SQR#(z0) -> c_1()
          SUM#(0()) -> c_2()
          SUM#(s(z0)) -> c_3(SQR#(s(z0)))
          SUM#(s(z0)) -> c_4(SUM#(z0))
          SUM#(s(z0)) -> c_5(SUM#(z0))
          sqr#(z0) -> c_6()
          sum#(0()) -> c_7()
          sum#(s(z0)) -> c_8(sum#(z0))
          sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
** Step 1.b:3: PredecessorEstimation.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            SQR#(z0) -> c_1()
            SUM#(0()) -> c_2()
            SUM#(s(z0)) -> c_3(SQR#(s(z0)))
            SUM#(s(z0)) -> c_4(SUM#(z0))
            SUM#(s(z0)) -> c_5(SUM#(z0))
        - Weak DPs:
            sqr#(z0) -> c_6()
            sum#(0()) -> c_7()
            sum#(s(z0)) -> c_8(sum#(z0))
            sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1,2}
        by application of
          Pre({1,2}) = {3,4,5}.
        Here rules are labelled as follows:
          1: SQR#(z0) -> c_1()
          2: SUM#(0()) -> c_2()
          3: SUM#(s(z0)) -> c_3(SQR#(s(z0)))
          4: SUM#(s(z0)) -> c_4(SUM#(z0))
          5: SUM#(s(z0)) -> c_5(SUM#(z0))
          6: sqr#(z0) -> c_6()
          7: sum#(0()) -> c_7()
          8: sum#(s(z0)) -> c_8(sum#(z0))
          9: sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
** Step 1.b:4: PredecessorEstimation.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            SUM#(s(z0)) -> c_3(SQR#(s(z0)))
            SUM#(s(z0)) -> c_4(SUM#(z0))
            SUM#(s(z0)) -> c_5(SUM#(z0))
        - Weak DPs:
            SQR#(z0) -> c_1()
            SUM#(0()) -> c_2()
            sqr#(z0) -> c_6()
            sum#(0()) -> c_7()
            sum#(s(z0)) -> c_8(sum#(z0))
            sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        PredecessorEstimation {onSelection = all simple predecessor estimation selector}
    + Details:
        We estimate the number of application of
          {1}
        by application of
          Pre({1}) = {2,3}.
        Here rules are labelled as follows:
          1: SUM#(s(z0)) -> c_3(SQR#(s(z0)))
          2: SUM#(s(z0)) -> c_4(SUM#(z0))
          3: SUM#(s(z0)) -> c_5(SUM#(z0))
          4: SQR#(z0) -> c_1()
          5: SUM#(0()) -> c_2()
          6: sqr#(z0) -> c_6()
          7: sum#(0()) -> c_7()
          8: sum#(s(z0)) -> c_8(sum#(z0))
          9: sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
** Step 1.b:5: RemoveWeakSuffixes.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            SUM#(s(z0)) -> c_4(SUM#(z0))
            SUM#(s(z0)) -> c_5(SUM#(z0))
        - Weak DPs:
            SQR#(z0) -> c_1()
            SUM#(0()) -> c_2()
            SUM#(s(z0)) -> c_3(SQR#(s(z0)))
            sqr#(z0) -> c_6()
            sum#(0()) -> c_7()
            sum#(s(z0)) -> c_8(sum#(z0))
            sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:S:SUM#(s(z0)) -> c_4(SUM#(z0))
             -->_1 SUM#(s(z0)) -> c_3(SQR#(s(z0))):5
             -->_1 SUM#(s(z0)) -> c_5(SUM#(z0)):2
             -->_1 SUM#(0()) -> c_2():4
             -->_1 SUM#(s(z0)) -> c_4(SUM#(z0)):1
          
          2:S:SUM#(s(z0)) -> c_5(SUM#(z0))
             -->_1 SUM#(s(z0)) -> c_3(SQR#(s(z0))):5
             -->_1 SUM#(0()) -> c_2():4
             -->_1 SUM#(s(z0)) -> c_5(SUM#(z0)):2
             -->_1 SUM#(s(z0)) -> c_4(SUM#(z0)):1
          
          3:W:SQR#(z0) -> c_1()
             
          
          4:W:SUM#(0()) -> c_2()
             
          
          5:W:SUM#(s(z0)) -> c_3(SQR#(s(z0)))
             -->_1 SQR#(z0) -> c_1():3
          
          6:W:sqr#(z0) -> c_6()
             
          
          7:W:sum#(0()) -> c_7()
             
          
          8:W:sum#(s(z0)) -> c_8(sum#(z0))
             -->_1 sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0)):9
             -->_1 sum#(s(z0)) -> c_8(sum#(z0)):8
             -->_1 sum#(0()) -> c_7():7
          
          9:W:sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
             -->_2 sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0)):9
             -->_2 sum#(s(z0)) -> c_8(sum#(z0)):8
             -->_2 sum#(0()) -> c_7():7
             -->_1 sqr#(z0) -> c_6():6
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          8: sum#(s(z0)) -> c_8(sum#(z0))
          9: sum#(s(z0)) -> c_9(sqr#(s(z0)),sum#(z0))
          7: sum#(0()) -> c_7()
          6: sqr#(z0) -> c_6()
          4: SUM#(0()) -> c_2()
          5: SUM#(s(z0)) -> c_3(SQR#(s(z0)))
          3: SQR#(z0) -> c_1()
** Step 1.b:6: PredecessorEstimationCP.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            SUM#(s(z0)) -> c_4(SUM#(z0))
            SUM#(s(z0)) -> c_5(SUM#(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        PredecessorEstimationCP {onSelectionCP = any intersect of rules of CDG leaf and strict-rules, withComplexityPair = NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing}}
    + Details:
        We first use the processor NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Nothing} to orient following rules strictly:
          1: SUM#(s(z0)) -> c_4(SUM#(z0))
          2: SUM#(s(z0)) -> c_5(SUM#(z0))
          
        The strictly oriented rules are moved into the weak component.
*** Step 1.b:6.a:1: NaturalMI.  WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict DPs:
            SUM#(s(z0)) -> c_4(SUM#(z0))
            SUM#(s(z0)) -> c_5(SUM#(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        NaturalMI {miDimension = 1, miDegree = 1, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just first alternative for predecessorEstimation on any intersect of rules of CDG leaf and strict-rules}
    + Details:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(c_4) = {1},
          uargs(c_5) = {1}
        
        Following symbols are considered usable:
          {SQR#,SUM#,sqr#,sum#}
        TcT has computed the following interpretation:
             p(*) = [1] x1 + [2]         
             p(+) = [1] x2 + [2]         
             p(0) = [1]                  
           p(SQR) = [8] x1 + [1]         
           p(SUM) = [1] x1 + [1]         
             p(c) = [8]                  
            p(c1) = [4]                  
            p(c2) = [1] x1 + [2]         
            p(c3) = [1] x1 + [0]         
            p(c4) = [0]                  
             p(s) = [1] x1 + [6]         
           p(sqr) = [0]                  
           p(sum) = [4] x1 + [1]         
          p(SQR#) = [1] x1 + [1]         
          p(SUM#) = [4] x1 + [1]         
          p(sqr#) = [0]                  
          p(sum#) = [8] x1 + [1]         
           p(c_1) = [1]                  
           p(c_2) = [1]                  
           p(c_3) = [0]                  
           p(c_4) = [1] x1 + [15]        
           p(c_5) = [1] x1 + [9]         
           p(c_6) = [1]                  
           p(c_7) = [2]                  
           p(c_8) = [1] x1 + [8]         
           p(c_9) = [4] x1 + [1] x2 + [0]
        
        Following rules are strictly oriented:
        SUM#(s(z0)) = [4] z0 + [25]
                    > [4] z0 + [16]
                    = c_4(SUM#(z0))
        
        SUM#(s(z0)) = [4] z0 + [25]
                    > [4] z0 + [10]
                    = c_5(SUM#(z0))
        
        
        Following rules are (at-least) weakly oriented:
        
*** Step 1.b:6.a:2: Assumption.  WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            SUM#(s(z0)) -> c_4(SUM#(z0))
            SUM#(s(z0)) -> c_5(SUM#(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        Assumption {assumed = Certificate {spaceUB = Unknown, spaceLB = Unknown, timeUB = Poly (Just 0), timeLB = Unknown, timeBCUB = Unknown, timeBCLB = Unknown}}
    + Details:
        ()

*** Step 1.b:6.b:1: RemoveWeakSuffixes.  WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak DPs:
            SUM#(s(z0)) -> c_4(SUM#(z0))
            SUM#(s(z0)) -> c_5(SUM#(z0))
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        RemoveWeakSuffixes
    + Details:
        Consider the dependency graph
          1:W:SUM#(s(z0)) -> c_4(SUM#(z0))
             -->_1 SUM#(s(z0)) -> c_5(SUM#(z0)):2
             -->_1 SUM#(s(z0)) -> c_4(SUM#(z0)):1
          
          2:W:SUM#(s(z0)) -> c_5(SUM#(z0))
             -->_1 SUM#(s(z0)) -> c_5(SUM#(z0)):2
             -->_1 SUM#(s(z0)) -> c_4(SUM#(z0)):1
          
        The following weak DPs constitute a sub-graph of the DG that is closed under successors. The DPs are removed.
          1: SUM#(s(z0)) -> c_4(SUM#(z0))
          2: SUM#(s(z0)) -> c_5(SUM#(z0))
*** Step 1.b:6.b:2: EmptyProcessor.  WORST_CASE(?,O(1))
    + Considered Problem:
        
        - Signature:
            {SQR/1,SUM/1,sqr/1,sum/1,SQR#/1,SUM#/1,sqr#/1,sum#/1} / {*/2,+/2,0/0,c/0,c1/1,c2/1,c3/1,c4/0,s/1,c_1/0,c_2/0
            ,c_3/1,c_4/1,c_5/1,c_6/0,c_7/0,c_8/1,c_9/2}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {SQR#,SUM#,sqr#,sum#} and constructors {*,+,0,c,c1,c2,c3
            ,c4,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

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