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

** Step 1.b:1: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            -(x,0()) -> x
            -(s(x),s(y)) -> -(x,y)
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            half(0()) -> 0()
            half(double(x)) -> x
            half(s(0())) -> 0()
            half(s(s(x))) -> s(half(x))
            if(0(),y,z) -> y
            if(s(x),y,z) -> z
        - Signature:
            {-/2,double/1,half/1,if/3} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,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(s) = {1}
        
        Following symbols are considered usable:
          {-,double,half,if}
        TcT has computed the following interpretation:
               p(-) = [2] x1 + [8]         
               p(0) = [0]                  
          p(double) = [8] x1 + [0]         
            p(half) = [2] x1 + [0]         
              p(if) = [2] x2 + [2] x3 + [0]
               p(s) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
        -(x,0()) = [2] x + [8]
                 > [1] x + [0]
                 = x          
        
        
        Following rules are (at-least) weakly oriented:
           -(s(x),s(y)) =  [2] x + [8]        
                        >= [2] x + [8]        
                        =  -(x,y)             
        
            double(0()) =  [0]                
                        >= [0]                
                        =  0()                
        
           double(s(x)) =  [8] x + [0]        
                        >= [8] x + [0]        
                        =  s(s(double(x)))    
        
              half(0()) =  [0]                
                        >= [0]                
                        =  0()                
        
        half(double(x)) =  [16] x + [0]       
                        >= [1] x + [0]        
                        =  x                  
        
           half(s(0())) =  [0]                
                        >= [0]                
                        =  0()                
        
          half(s(s(x))) =  [2] x + [0]        
                        >= [2] x + [0]        
                        =  s(half(x))         
        
            if(0(),y,z) =  [2] y + [2] z + [0]
                        >= [1] y + [0]        
                        =  y                  
        
           if(s(x),y,z) =  [2] y + [2] z + [0]
                        >= [1] z + [0]        
                        =  z                  
        
** Step 1.b:2: NaturalMI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            -(s(x),s(y)) -> -(x,y)
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            half(0()) -> 0()
            half(double(x)) -> x
            half(s(0())) -> 0()
            half(s(s(x))) -> s(half(x))
            if(0(),y,z) -> y
            if(s(x),y,z) -> z
        - Weak TRS:
            -(x,0()) -> x
        - Signature:
            {-/2,double/1,half/1,if/3} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,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(s) = {1}
        
        Following symbols are considered usable:
          {-,double,half,if}
        TcT has computed the following interpretation:
               p(-) = [1] x1 + [14]        
               p(0) = [2]                  
          p(double) = [1] x1 + [0]         
            p(half) = [4] x1 + [0]         
              p(if) = [2] x2 + [2] x3 + [0]
               p(s) = [1] x1 + [0]         
        
        Following rules are strictly oriented:
           half(0()) = [8]
                     > [2]
                     = 0()
        
        half(s(0())) = [8]
                     > [2]
                     = 0()
        
        
        Following rules are (at-least) weakly oriented:
               -(x,0()) =  [1] x + [14]       
                        >= [1] x + [0]        
                        =  x                  
        
           -(s(x),s(y)) =  [1] x + [14]       
                        >= [1] x + [14]       
                        =  -(x,y)             
        
            double(0()) =  [2]                
                        >= [2]                
                        =  0()                
        
           double(s(x)) =  [1] x + [0]        
                        >= [1] x + [0]        
                        =  s(s(double(x)))    
        
        half(double(x)) =  [4] x + [0]        
                        >= [1] x + [0]        
                        =  x                  
        
          half(s(s(x))) =  [4] x + [0]        
                        >= [4] x + [0]        
                        =  s(half(x))         
        
            if(0(),y,z) =  [2] y + [2] z + [0]
                        >= [1] y + [0]        
                        =  y                  
        
           if(s(x),y,z) =  [2] y + [2] z + [0]
                        >= [1] z + [0]        
                        =  z                  
        
** Step 1.b:3: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            -(s(x),s(y)) -> -(x,y)
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            half(double(x)) -> x
            half(s(s(x))) -> s(half(x))
            if(0(),y,z) -> y
            if(s(x),y,z) -> z
        - Weak TRS:
            -(x,0()) -> x
            half(0()) -> 0()
            half(s(0())) -> 0()
        - Signature:
            {-/2,double/1,half/1,if/3} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,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:
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {-,double,half,if}
        TcT has computed the following interpretation:
               p(-) = 6 + x1 + x2     
               p(0) = 1               
          p(double) = 9 + 2*x1        
            p(half) = 9 + x1          
              p(if) = 2 + 14*x2 + 8*x3
               p(s) = 8 + x1          
        
        Following rules are strictly oriented:
           -(s(x),s(y)) = 22 + x + y    
                        > 6 + x + y     
                        = -(x,y)        
        
            double(0()) = 11            
                        > 1             
                        = 0()           
        
        half(double(x)) = 18 + 2*x      
                        > x             
                        = x             
        
          half(s(s(x))) = 25 + x        
                        > 17 + x        
                        = s(half(x))    
        
            if(0(),y,z) = 2 + 14*y + 8*z
                        > y             
                        = y             
        
           if(s(x),y,z) = 2 + 14*y + 8*z
                        > z             
                        = z             
        
        
        Following rules are (at-least) weakly oriented:
            -(x,0()) =  7 + x          
                     >= x              
                     =  x              
        
        double(s(x)) =  25 + 2*x       
                     >= 25 + 2*x       
                     =  s(s(double(x)))
        
           half(0()) =  10             
                     >= 1              
                     =  0()            
        
        half(s(0())) =  18             
                     >= 1              
                     =  0()            
        
** Step 1.b:4: NaturalPI WORST_CASE(?,O(n^1))
    + Considered Problem:
        - Strict TRS:
            double(s(x)) -> s(s(double(x)))
        - Weak TRS:
            -(x,0()) -> x
            -(s(x),s(y)) -> -(x,y)
            double(0()) -> 0()
            half(0()) -> 0()
            half(double(x)) -> x
            half(s(0())) -> 0()
            half(s(s(x))) -> s(half(x))
            if(0(),y,z) -> y
            if(s(x),y,z) -> z
        - Signature:
            {-/2,double/1,half/1,if/3} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,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:
          uargs(s) = {1}
        
        Following symbols are considered usable:
          {-,double,half,if}
        TcT has computed the following interpretation:
               p(-) = 8*x1 + x2            
               p(0) = 0                    
          p(double) = 6 + 8*x1             
            p(half) = 12 + 2*x1            
              p(if) = 14 + x1 + 3*x2 + 8*x3
               p(s) = 2 + x1               
        
        Following rules are strictly oriented:
        double(s(x)) = 22 + 8*x       
                     > 10 + 8*x       
                     = s(s(double(x)))
        
        
        Following rules are (at-least) weakly oriented:
               -(x,0()) =  8*x               
                        >= x                 
                        =  x                 
        
           -(s(x),s(y)) =  18 + 8*x + y      
                        >= 8*x + y           
                        =  -(x,y)            
        
            double(0()) =  6                 
                        >= 0                 
                        =  0()               
        
              half(0()) =  12                
                        >= 0                 
                        =  0()               
        
        half(double(x)) =  24 + 16*x         
                        >= x                 
                        =  x                 
        
           half(s(0())) =  16                
                        >= 0                 
                        =  0()               
        
          half(s(s(x))) =  20 + 2*x          
                        >= 14 + 2*x          
                        =  s(half(x))        
        
            if(0(),y,z) =  14 + 3*y + 8*z    
                        >= y                 
                        =  y                 
        
           if(s(x),y,z) =  16 + x + 3*y + 8*z
                        >= z                 
                        =  z                 
        
** Step 1.b:5: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            -(x,0()) -> x
            -(s(x),s(y)) -> -(x,y)
            double(0()) -> 0()
            double(s(x)) -> s(s(double(x)))
            half(0()) -> 0()
            half(double(x)) -> x
            half(s(0())) -> 0()
            half(s(s(x))) -> s(half(x))
            if(0(),y,z) -> y
            if(s(x),y,z) -> z
        - Signature:
            {-/2,double/1,half/1,if/3} / {0/0,s/1}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {-,double,half,if} and constructors {0,s}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

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