*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        sum(0()) -> 0()
        sum(s(x)) -> +(sum(x),s(x))
        sum1(0()) -> 0()
        sum1(s(x)) -> s(+(sum1(x),+(x,x)))
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {sum/1,sum1/1} / {+/2,0/0,s/1}
      Obligation:
        Full
        basic terms: {sum,sum1}/{+,0,s}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(+) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
             p(+) = [1] x1 + [0]
             p(0) = [0]         
             p(s) = [1] x1 + [7]
           p(sum) = [0]         
          p(sum1) = [4] x1 + [1]
        
        Following rules are strictly oriented:
         sum1(0()) = [1]                 
                   > [0]                 
                   = 0()                 
        
        sum1(s(x)) = [4] x + [29]        
                   > [4] x + [8]         
                   = s(+(sum1(x),+(x,x)))
        
        
        Following rules are (at-least) weakly oriented:
         sum(0()) =  [0]           
                  >= [0]           
                  =  0()           
        
        sum(s(x)) =  [0]           
                  >= [0]           
                  =  +(sum(x),s(x))
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        sum(0()) -> 0()
        sum(s(x)) -> +(sum(x),s(x))
      Weak DP Rules:
        
      Weak TRS Rules:
        sum1(0()) -> 0()
        sum1(s(x)) -> s(+(sum1(x),+(x,x)))
      Signature:
        {sum/1,sum1/1} / {+/2,0/0,s/1}
      Obligation:
        Full
        basic terms: {sum,sum1}/{+,0,s}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(+) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
             p(+) = [1] x1 + [4]
             p(0) = [7]         
             p(s) = [1] x1 + [8]
           p(sum) = [9]         
          p(sum1) = [2] x1 + [2]
        
        Following rules are strictly oriented:
        sum(0()) = [9]
                 > [7]
                 = 0()
        
        
        Following rules are (at-least) weakly oriented:
         sum(s(x)) =  [9]                 
                   >= [13]                
                   =  +(sum(x),s(x))      
        
         sum1(0()) =  [16]                
                   >= [7]                 
                   =  0()                 
        
        sum1(s(x)) =  [2] x + [18]        
                   >= [2] x + [14]        
                   =  s(+(sum1(x),+(x,x)))
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        sum(s(x)) -> +(sum(x),s(x))
      Weak DP Rules:
        
      Weak TRS Rules:
        sum(0()) -> 0()
        sum1(0()) -> 0()
        sum1(s(x)) -> s(+(sum1(x),+(x,x)))
      Signature:
        {sum/1,sum1/1} / {+/2,0/0,s/1}
      Obligation:
        Full
        basic terms: {sum,sum1}/{+,0,s}
    Applied Processor:
      WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    Proof:
      The weightgap principle applies using the following nonconstant growth matrix-interpretation:
        We apply a matrix interpretation of kind constructor based matrix interpretation:
        The following argument positions are considered usable:
          uargs(+) = {1},
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
             p(+) = [1] x1 + [1] 
             p(0) = [2]          
             p(s) = [1] x1 + [2] 
           p(sum) = [4] x1 + [4] 
          p(sum1) = [8] x1 + [15]
        
        Following rules are strictly oriented:
        sum(s(x)) = [4] x + [12]  
                  > [4] x + [5]   
                  = +(sum(x),s(x))
        
        
        Following rules are (at-least) weakly oriented:
          sum(0()) =  [12]                
                   >= [2]                 
                   =  0()                 
        
         sum1(0()) =  [31]                
                   >= [2]                 
                   =  0()                 
        
        sum1(s(x)) =  [8] x + [31]        
                   >= [8] x + [18]        
                   =  s(+(sum1(x),+(x,x)))
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        sum(0()) -> 0()
        sum(s(x)) -> +(sum(x),s(x))
        sum1(0()) -> 0()
        sum1(s(x)) -> s(+(sum1(x),+(x,x)))
      Signature:
        {sum/1,sum1/1} / {+/2,0/0,s/1}
      Obligation:
        Full
        basic terms: {sum,sum1}/{+,0,s}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).