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

** Step 1.b:1: WeightGap WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            if(false(),x,y) -> y
            if(true(),x,y) -> x
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            minus(x,0()) -> x
            minus(x,s(y)) -> if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {if/3,le/2,minus/2,p/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {if,le,minus,p} and constructors {0,false,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        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(if) = {1,3},
            uargs(minus) = {2},
            uargs(p) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(0) = [0]                           
            p(false) = [0]                           
               p(if) = [1] x1 + [2] x2 + [1] x3 + [0]
               p(le) = [0]                           
            p(minus) = [6] x1 + [1] x2 + [0]         
                p(p) = [1] x1 + [5]                  
                p(s) = [1] x1 + [0]                  
             p(true) = [0]                           
          
          Following rules are strictly oriented:
           p(0()) = [5]        
                  > [0]        
                  = 0()        
          
          p(s(x)) = [1] x + [5]
                  > [1] x + [0]
                  = x          
          
          
          Following rules are (at-least) weakly oriented:
          if(false(),x,y) =  [2] x + [1] y + [0]                   
                          >= [1] y + [0]                           
                          =  y                                     
          
           if(true(),x,y) =  [2] x + [1] y + [0]                   
                          >= [1] x + [0]                           
                          =  x                                     
          
                le(0(),y) =  [0]                                   
                          >= [0]                                   
                          =  true()                                
          
             le(s(x),0()) =  [0]                                   
                          >= [0]                                   
                          =  false()                               
          
            le(s(x),s(y)) =  [0]                                   
                          >= [0]                                   
                          =  le(x,y)                               
          
             minus(x,0()) =  [6] x + [0]                           
                          >= [1] x + [0]                           
                          =  x                                     
          
            minus(x,s(y)) =  [6] x + [1] y + [0]                   
                          >= [6] x + [1] y + [10]                  
                          =  if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:2: WeightGap WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            if(false(),x,y) -> y
            if(true(),x,y) -> x
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            minus(x,0()) -> x
            minus(x,s(y)) -> if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
        - Weak TRS:
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {if/3,le/2,minus/2,p/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {if,le,minus,p} and constructors {0,false,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        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(if) = {1,3},
            uargs(minus) = {2},
            uargs(p) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(0) = [0]                           
            p(false) = [0]                           
               p(if) = [1] x1 + [2] x2 + [1] x3 + [0]
               p(le) = [4]                           
            p(minus) = [1] x1 + [1] x2 + [0]         
                p(p) = [1] x1 + [0]                  
                p(s) = [1] x1 + [0]                  
             p(true) = [0]                           
          
          Following rules are strictly oriented:
             le(0(),y) = [4]    
                       > [0]    
                       = true() 
          
          le(s(x),0()) = [4]    
                       > [0]    
                       = false()
          
          
          Following rules are (at-least) weakly oriented:
          if(false(),x,y) =  [2] x + [1] y + [0]                   
                          >= [1] y + [0]                           
                          =  y                                     
          
           if(true(),x,y) =  [2] x + [1] y + [0]                   
                          >= [1] x + [0]                           
                          =  x                                     
          
            le(s(x),s(y)) =  [4]                                   
                          >= [4]                                   
                          =  le(x,y)                               
          
             minus(x,0()) =  [1] x + [0]                           
                          >= [1] x + [0]                           
                          =  x                                     
          
            minus(x,s(y)) =  [1] x + [1] y + [0]                   
                          >= [1] x + [1] y + [4]                   
                          =  if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
          
                   p(0()) =  [0]                                   
                          >= [0]                                   
                          =  0()                                   
          
                  p(s(x)) =  [1] x + [0]                           
                          >= [1] x + [0]                           
                          =  x                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:3: WeightGap WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            if(false(),x,y) -> y
            if(true(),x,y) -> x
            le(s(x),s(y)) -> le(x,y)
            minus(x,0()) -> x
            minus(x,s(y)) -> if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
        - Weak TRS:
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {if/3,le/2,minus/2,p/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {if,le,minus,p} and constructors {0,false,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        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(if) = {1,3},
            uargs(minus) = {2},
            uargs(p) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(0) = [0]                           
            p(false) = [0]                           
               p(if) = [1] x1 + [8] x2 + [1] x3 + [0]
               p(le) = [0]                           
            p(minus) = [8] x1 + [1] x2 + [1]         
                p(p) = [1] x1 + [0]                  
                p(s) = [1] x1 + [0]                  
             p(true) = [0]                           
          
          Following rules are strictly oriented:
          minus(x,0()) = [8] x + [1]
                       > [1] x + [0]
                       = x          
          
          
          Following rules are (at-least) weakly oriented:
          if(false(),x,y) =  [8] x + [1] y + [0]                   
                          >= [1] y + [0]                           
                          =  y                                     
          
           if(true(),x,y) =  [8] x + [1] y + [0]                   
                          >= [1] x + [0]                           
                          =  x                                     
          
                le(0(),y) =  [0]                                   
                          >= [0]                                   
                          =  true()                                
          
             le(s(x),0()) =  [0]                                   
                          >= [0]                                   
                          =  false()                               
          
            le(s(x),s(y)) =  [0]                                   
                          >= [0]                                   
                          =  le(x,y)                               
          
            minus(x,s(y)) =  [8] x + [1] y + [1]                   
                          >= [8] x + [1] y + [1]                   
                          =  if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
          
                   p(0()) =  [0]                                   
                          >= [0]                                   
                          =  0()                                   
          
                  p(s(x)) =  [1] x + [0]                           
                          >= [1] x + [0]                           
                          =  x                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:4: WeightGap WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            if(false(),x,y) -> y
            if(true(),x,y) -> x
            le(s(x),s(y)) -> le(x,y)
            minus(x,s(y)) -> if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
        - Weak TRS:
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            minus(x,0()) -> x
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {if/3,le/2,minus/2,p/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {if,le,minus,p} and constructors {0,false,s,true}
    + Applied Processor:
        WeightGap {wgDimension = 1, wgDegree = 1, wgKind = Algebraic, wgUArgs = UArgs, wgOn = WgOnAny}
    + Details:
        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(if) = {1,3},
            uargs(minus) = {2},
            uargs(p) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(0) = [0]                           
            p(false) = [1]                           
               p(if) = [1] x1 + [1] x2 + [1] x3 + [0]
               p(le) = [1]                           
            p(minus) = [8] x1 + [1] x2 + [0]         
                p(p) = [1] x1 + [8]                  
                p(s) = [1] x1 + [8]                  
             p(true) = [1]                           
          
          Following rules are strictly oriented:
          if(false(),x,y) = [1] x + [1] y + [1]
                          > [1] y + [0]        
                          = y                  
          
           if(true(),x,y) = [1] x + [1] y + [1]
                          > [1] x + [0]        
                          = x                  
          
          
          Following rules are (at-least) weakly oriented:
              le(0(),y) =  [1]                                   
                        >= [1]                                   
                        =  true()                                
          
           le(s(x),0()) =  [1]                                   
                        >= [1]                                   
                        =  false()                               
          
          le(s(x),s(y)) =  [1]                                   
                        >= [1]                                   
                        =  le(x,y)                               
          
           minus(x,0()) =  [8] x + [0]                           
                        >= [1] x + [0]                           
                        =  x                                     
          
          minus(x,s(y)) =  [8] x + [1] y + [8]                   
                        >= [8] x + [1] y + [25]                  
                        =  if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
          
                 p(0()) =  [8]                                   
                        >= [0]                                   
                        =  0()                                   
          
                p(s(x)) =  [1] x + [16]                          
                        >= [1] x + [0]                           
                        =  x                                     
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
** Step 1.b:5: MI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            le(s(x),s(y)) -> le(x,y)
            minus(x,s(y)) -> if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
        - Weak TRS:
            if(false(),x,y) -> y
            if(true(),x,y) -> x
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            minus(x,0()) -> x
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {if/3,le/2,minus/2,p/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {if,le,minus,p} and constructors {0,false,s,true}
    + Applied Processor:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity (Just 2))), miDimension = 3, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity (Just 2))):
        
        The following argument positions are considered usable:
          uargs(if) = {1,3},
          uargs(minus) = {2},
          uargs(p) = {1}
        
        Following symbols are considered usable:
          {if,le,minus,p}
        TcT has computed the following interpretation:
              p(0) = [0]                                          
                     [0]                                          
                     [0]                                          
          p(false) = [0]                                          
                     [1]                                          
                     [1]                                          
             p(if) = [2 0 0]       [2 0 0]       [1 0 0]       [0]
                     [1 1 0] x_1 + [0 1 0] x_2 + [0 1 0] x_3 + [0]
                     [0 0 1]       [1 0 2]       [0 0 1]       [0]
             p(le) = [0 0 0]       [0]                            
                     [0 0 0] x_1 + [1]                            
                     [2 2 0]       [1]                            
          p(minus) = [1 0 0]       [2 0 1]       [0]              
                     [1 1 0] x_1 + [2 1 0] x_2 + [1]              
                     [3 3 1]       [3 0 0]       [3]              
              p(p) = [1 0 0]       [0]                            
                     [1 0 0] x_1 + [0]                            
                     [0 1 0]       [0]                            
              p(s) = [1 1 0]       [0]                            
                     [0 0 1] x_1 + [0]                            
                     [0 0 1]       [1]                            
           p(true) = [0]                                          
                     [0]                                          
                     [1]                                          
        
        Following rules are strictly oriented:
        minus(x,s(y)) = [1 0 0]     [2 2 1]     [1]           
                        [1 1 0] x + [2 2 1] y + [1]           
                        [3 3 1]     [3 3 0]     [3]           
                      > [1 0 0]     [2 2 1]     [0]           
                        [1 0 0] x + [2 2 1] y + [1]           
                        [3 3 0]     [3 3 0]     [2]           
                      = if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
        
        
        Following rules are (at-least) weakly oriented:
        if(false(),x,y) =  [2 0 0]     [1 0 0]     [0]
                           [0 1 0] x + [0 1 0] y + [1]
                           [1 0 2]     [0 0 1]     [1]
                        >= [1 0 0]     [0]            
                           [0 1 0] y + [0]            
                           [0 0 1]     [0]            
                        =  y                          
        
         if(true(),x,y) =  [2 0 0]     [1 0 0]     [0]
                           [0 1 0] x + [0 1 0] y + [0]
                           [1 0 2]     [0 0 1]     [1]
                        >= [1 0 0]     [0]            
                           [0 1 0] x + [0]            
                           [0 0 1]     [0]            
                        =  x                          
        
              le(0(),y) =  [0]                        
                           [1]                        
                           [1]                        
                        >= [0]                        
                           [0]                        
                           [1]                        
                        =  true()                     
        
           le(s(x),0()) =  [0 0 0]     [0]            
                           [0 0 0] x + [1]            
                           [2 2 2]     [1]            
                        >= [0]                        
                           [1]                        
                           [1]                        
                        =  false()                    
        
          le(s(x),s(y)) =  [0 0 0]     [0]            
                           [0 0 0] x + [1]            
                           [2 2 2]     [1]            
                        >= [0 0 0]     [0]            
                           [0 0 0] x + [1]            
                           [2 2 0]     [1]            
                        =  le(x,y)                    
        
           minus(x,0()) =  [1 0 0]     [0]            
                           [1 1 0] x + [1]            
                           [3 3 1]     [3]            
                        >= [1 0 0]     [0]            
                           [0 1 0] x + [0]            
                           [0 0 1]     [0]            
                        =  x                          
        
                 p(0()) =  [0]                        
                           [0]                        
                           [0]                        
                        >= [0]                        
                           [0]                        
                           [0]                        
                        =  0()                        
        
                p(s(x)) =  [1 1 0]     [0]            
                           [1 1 0] x + [0]            
                           [0 0 1]     [0]            
                        >= [1 0 0]     [0]            
                           [0 1 0] x + [0]            
                           [0 0 1]     [0]            
                        =  x                          
        
** Step 1.b:6: MI WORST_CASE(?,O(n^3))
    + Considered Problem:
        - Strict TRS:
            le(s(x),s(y)) -> le(x,y)
        - Weak TRS:
            if(false(),x,y) -> y
            if(true(),x,y) -> x
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            minus(x,0()) -> x
            minus(x,s(y)) -> if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {if/3,le/2,minus/2,p/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {if,le,minus,p} and constructors {0,false,s,true}
    + Applied Processor:
        MI {miKind = MaximalMatrix (UpperTriangular (Multiplicity (Just 3))), miDimension = 4, miUArgs = UArgs, miURules = URules, miSelector = Just any strict-rules}
    + Details:
        We apply a matrix interpretation of kind MaximalMatrix (UpperTriangular (Multiplicity (Just 3))):
        
        The following argument positions are considered usable:
          uargs(if) = {1,3},
          uargs(minus) = {2},
          uargs(p) = {1}
        
        Following symbols are considered usable:
          {if,le,minus,p}
        TcT has computed the following interpretation:
              p(0) = [0]                                                
                     [1]                                                
                     [1]                                                
                     [0]                                                
          p(false) = [0]                                                
                     [0]                                                
                     [0]                                                
                     [0]                                                
             p(if) = [1 0 0 0]       [1 0 0 0]       [1 0 0 0]       [0]
                     [0 0 0 0] x_1 + [0 1 0 0] x_2 + [0 1 0 0] x_3 + [0]
                     [0 0 0 0]       [0 1 1 0]       [0 0 1 0]       [0]
                     [0 0 0 0]       [0 0 0 1]       [0 0 0 1]       [0]
             p(le) = [0 0 0 0]       [0 0 0 1]       [0]                
                     [0 0 0 0] x_1 + [0 0 0 1] x_2 + [0]                
                     [0 0 1 0]       [0 0 1 0]       [0]                
                     [0 0 0 0]       [0 0 1 0]       [0]                
          p(minus) = [1 0 0 0]       [1 0 1 0]       [0]                
                     [1 1 0 0] x_1 + [1 0 1 0] x_2 + [1]                
                     [1 1 1 0]       [1 0 1 1]       [1]                
                     [0 0 0 1]       [0 0 1 0]       [0]                
              p(p) = [1 0 0 0]       [0]                                
                     [1 0 0 0] x_1 + [1]                                
                     [0 1 0 0]       [0]                                
                     [0 0 0 1]       [1]                                
              p(s) = [1 1 1 0]       [0]                                
                     [0 0 1 0] x_1 + [0]                                
                     [0 0 1 1]       [1]                                
                     [0 0 0 1]       [1]                                
           p(true) = [0]                                                
                     [0]                                                
                     [0]                                                
                     [0]                                                
        
        Following rules are strictly oriented:
        le(s(x),s(y)) = [0 0 0 0]     [0 0 0 1]     [1]
                        [0 0 0 0] x + [0 0 0 1] y + [1]
                        [0 0 1 1]     [0 0 1 1]     [2]
                        [0 0 0 0]     [0 0 1 1]     [1]
                      > [0 0 0 0]     [0 0 0 1]     [0]
                        [0 0 0 0] x + [0 0 0 1] y + [0]
                        [0 0 1 0]     [0 0 1 0]     [0]
                        [0 0 0 0]     [0 0 1 0]     [0]
                      = le(x,y)                        
        
        
        Following rules are (at-least) weakly oriented:
        if(false(),x,y) =  [1 0 0 0]     [1 0 0 0]     [0]       
                           [0 1 0 0] x + [0 1 0 0] y + [0]       
                           [0 1 1 0]     [0 0 1 0]     [0]       
                           [0 0 0 1]     [0 0 0 1]     [0]       
                        >= [1 0 0 0]     [0]                     
                           [0 1 0 0] y + [0]                     
                           [0 0 1 0]     [0]                     
                           [0 0 0 1]     [0]                     
                        =  y                                     
        
         if(true(),x,y) =  [1 0 0 0]     [1 0 0 0]     [0]       
                           [0 1 0 0] x + [0 1 0 0] y + [0]       
                           [0 1 1 0]     [0 0 1 0]     [0]       
                           [0 0 0 1]     [0 0 0 1]     [0]       
                        >= [1 0 0 0]     [0]                     
                           [0 1 0 0] x + [0]                     
                           [0 0 1 0]     [0]                     
                           [0 0 0 1]     [0]                     
                        =  x                                     
        
              le(0(),y) =  [0 0 0 1]     [0]                     
                           [0 0 0 1] y + [0]                     
                           [0 0 1 0]     [1]                     
                           [0 0 1 0]     [0]                     
                        >= [0]                                   
                           [0]                                   
                           [0]                                   
                           [0]                                   
                        =  true()                                
        
           le(s(x),0()) =  [0 0 0 0]     [0]                     
                           [0 0 0 0] x + [0]                     
                           [0 0 1 1]     [2]                     
                           [0 0 0 0]     [1]                     
                        >= [0]                                   
                           [0]                                   
                           [0]                                   
                           [0]                                   
                        =  false()                               
        
           minus(x,0()) =  [1 0 0 0]     [1]                     
                           [1 1 0 0] x + [2]                     
                           [1 1 1 0]     [2]                     
                           [0 0 0 1]     [1]                     
                        >= [1 0 0 0]     [0]                     
                           [0 1 0 0] x + [0]                     
                           [0 0 1 0]     [0]                     
                           [0 0 0 1]     [0]                     
                        =  x                                     
        
          minus(x,s(y)) =  [1 0 0 0]     [1 1 2 1]     [1]       
                           [1 1 0 0] x + [1 1 2 1] y + [2]       
                           [1 1 1 0]     [1 1 2 2]     [3]       
                           [0 0 0 1]     [0 0 1 1]     [1]       
                        >= [1 0 0 0]     [1 1 2 1]     [1]       
                           [1 0 0 0] x + [1 1 2 0] y + [2]       
                           [1 1 0 0]     [1 1 2 0]     [3]       
                           [0 0 0 1]     [0 0 1 0]     [1]       
                        =  if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
        
                 p(0()) =  [0]                                   
                           [1]                                   
                           [1]                                   
                           [1]                                   
                        >= [0]                                   
                           [1]                                   
                           [1]                                   
                           [0]                                   
                        =  0()                                   
        
                p(s(x)) =  [1 1 1 0]     [0]                     
                           [1 1 1 0] x + [1]                     
                           [0 0 1 0]     [0]                     
                           [0 0 0 1]     [2]                     
                        >= [1 0 0 0]     [0]                     
                           [0 1 0 0] x + [0]                     
                           [0 0 1 0]     [0]                     
                           [0 0 0 1]     [0]                     
                        =  x                                     
        
** Step 1.b:7: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            if(false(),x,y) -> y
            if(true(),x,y) -> x
            le(0(),y) -> true()
            le(s(x),0()) -> false()
            le(s(x),s(y)) -> le(x,y)
            minus(x,0()) -> x
            minus(x,s(y)) -> if(le(x,s(y)),0(),p(minus(x,p(s(y)))))
            p(0()) -> 0()
            p(s(x)) -> x
        - Signature:
            {if/3,le/2,minus/2,p/1} / {0/0,false/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {if,le,minus,p} and constructors {0,false,s,true}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

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