*** 1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        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
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {if/3,le/2,minus/2,p/1} / {0/0,false/0,s/1,true/0}
      Obligation:
        Innermost
        basic terms: {if,le,minus,p}/{0,false,s,true}
    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(if) = {1,3},
          uargs(minus) = {2},
          uargs(p) = {1}
        
        Following symbols are considered usable:
          {}
        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.
*** 1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        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 DP Rules:
        
      Weak TRS Rules:
        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
        basic terms: {if,le,minus,p}/{0,false,s,true}
    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(if) = {1,3},
          uargs(minus) = {2},
          uargs(p) = {1}
        
        Following symbols are considered usable:
          {}
        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.
*** 1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        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 DP Rules:
        
      Weak TRS Rules:
        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
        basic terms: {if,le,minus,p}/{0,false,s,true}
    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(if) = {1,3},
          uargs(minus) = {2},
          uargs(p) = {1}
        
        Following symbols are considered usable:
          {}
        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.
*** 1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        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 DP Rules:
        
      Weak TRS Rules:
        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
        basic terms: {if,le,minus,p}/{0,false,s,true}
    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(if) = {1,3},
          uargs(minus) = {2},
          uargs(p) = {1}
        
        Following symbols are considered usable:
          {}
        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.
*** 1.1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        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 DP Rules:
        
      Weak TRS Rules:
        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
        basic terms: {if,le,minus,p}/{0,false,s,true}
    Applied Processor:
      NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 2 non-zero interpretation-entries in the diagonal of the component-wise maxima):
      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]                           
                   [0]                           
                   [0]                           
           p(if) = [1 0 0]      [1 0 0]      [1 0
                   0]      [0]                   
                   [0 0 0] x1 + [0 1 0] x2 + [0 1
                   0] x3 + [0]                   
                   [0 0 0]      [0 0 1]      [0 0
                   1]      [1]                   
           p(le) = [0 0 0]      [0]              
                   [1 0 0] x1 + [0]              
                   [0 0 0]      [0]              
        p(minus) = [1 0 0]      [1 0 1]      [0] 
                   [1 1 0] x1 + [1 0 1] x2 + [0] 
                   [1 1 1]      [1 0 1]      [0] 
            p(p) = [1 0 0]      [0]              
                   [1 0 0] x1 + [1]              
                   [0 1 0]      [0]              
            p(s) = [1 1 0]      [1]              
                   [0 0 1] x1 + [0]              
                   [0 0 1]      [1]              
         p(true) = [0]                           
                   [0]                           
                   [0]                           
      
      Following rules are strictly oriented:
      minus(x,s(y)) = [1 0 0]     [1 1 1]     [2]
                      [1 1 0] x + [1 1 1] y + [2]
                      [1 1 1]     [1 1 1]     [2]
                    > [1 0 0]     [1 1 1]     [1]
                      [1 0 0] x + [1 1 1] y + [2]
                      [1 1 0]     [1 1 1]     [2]
                    = if(le(x,s(y))              
                        ,0()                     
                        ,p(minus(x,p(s(y)))))    
      
      
      Following rules are (at-least) weakly oriented:
      if(false(),x,y) =  [1 0 0]     [1 0 0]     [0]
                         [0 1 0] x + [0 1 0] y + [0]
                         [0 0 1]     [0 0 1]     [1]
                      >= [1 0 0]     [0]            
                         [0 1 0] y + [0]            
                         [0 0 1]     [0]            
                      =  y                          
      
       if(true(),x,y) =  [1 0 0]     [1 0 0]     [0]
                         [0 1 0] x + [0 1 0] y + [0]
                         [0 0 1]     [0 0 1]     [1]
                      >= [1 0 0]     [0]            
                         [0 1 0] x + [0]            
                         [0 0 1]     [0]            
                      =  x                          
      
            le(0(),y) =  [0]                        
                         [0]                        
                         [0]                        
                      >= [0]                        
                         [0]                        
                         [0]                        
                      =  true()                     
      
         le(s(x),0()) =  [0 0 0]     [0]            
                         [1 1 0] x + [1]            
                         [0 0 0]     [0]            
                      >= [0]                        
                         [0]                        
                         [0]                        
                      =  false()                    
      
        le(s(x),s(y)) =  [0 0 0]     [0]            
                         [1 1 0] x + [1]            
                         [0 0 0]     [0]            
                      >= [0 0 0]     [0]            
                         [1 0 0] x + [0]            
                         [0 0 0]     [0]            
                      =  le(x,y)                    
      
         minus(x,0()) =  [1 0 0]     [0]            
                         [1 1 0] x + [0]            
                         [1 1 1]     [0]            
                      >= [1 0 0]     [0]            
                         [0 1 0] x + [0]            
                         [0 0 1]     [0]            
                      =  x                          
      
               p(0()) =  [0]                        
                         [1]                        
                         [0]                        
                      >= [0]                        
                         [0]                        
                         [0]                        
                      =  0()                        
      
              p(s(x)) =  [1 1 0]     [1]            
                         [1 1 0] x + [2]            
                         [0 0 1]     [0]            
                      >= [1 0 0]     [0]            
                         [0 1 0] x + [0]            
                         [0 0 1]     [0]            
                      =  x                          
      
*** 1.1.1.1.1.1 Progress [(O(1),O(n^3))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        le(s(x),s(y)) -> le(x,y)
      Weak DP Rules:
        
      Weak TRS Rules:
        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
        basic terms: {if,le,minus,p}/{0,false,s,true}
    Applied Processor:
      NaturalMI {miDimension = 4, miDegree = 3, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules, greedy = NoGreedy}
    Proof:
      We apply a matrix interpretation of kind constructor based matrix interpretation (containing no more than 3 non-zero interpretation-entries in the diagonal of the component-wise maxima):
      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]                             
                   [0]                             
        p(false) = [0]                             
                   [1]                             
                   [0]                             
                   [0]                             
           p(if) = [1 0 0 0]      [1 0 0 0]      [1
                   0 0 0]      [0]                 
                   [0 0 0 0] x1 + [0 1 0 0] x2 + [0
                   1 0 0] x3 + [0]                 
                   [0 0 0 0]      [0 0 1 0]      [0
                   0 1 0]      [1]                 
                   [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] x1 + [0 0 0           
                   1] x2 + [1]                     
                   [0 0 0 1]      [0 0 0           
                   0]      [0]                     
                   [0 0 0 0]      [0 0 0           
                   0]      [1]                     
        p(minus) = [1 0 0 0]      [1 0 1           
                   0]      [0]                     
                   [1 1 0 1] x1 + [1 0 1           
                   1] x2 + [0]                     
                   [1 1 1 1]      [1 1 1           
                   0]      [1]                     
                   [0 0 0 1]      [0 0 0           
                   0]      [0]                     
            p(p) = [1 0 0 0]      [0]              
                   [1 0 0 1] x1 + [0]              
                   [0 1 0 0]      [0]              
                   [0 0 0 1]      [0]              
            p(s) = [1 1 0 0]      [0]              
                   [0 0 1 0] x1 + [0]              
                   [0 0 1 1]      [1]              
                   [0 0 0 1]      [1]              
         p(true) = [0]                             
                   [0]                             
                   [0]                             
                   [1]                             
      
      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 + [2]
                      [0 0 0 1]     [0 0 0 0]     [1]
                      [0 0 0 0]     [0 0 0 0]     [1]
                    > [0 0 0 0]     [0 0 0 1]     [0]
                      [0 0 0 0] x + [0 0 0 1] y + [1]
                      [0 0 0 1]     [0 0 0 0]     [0]
                      [0 0 0 0]     [0 0 0 0]     [1]
                    = 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 0 1 0]     [0 0 1 0]     [1]
                         [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 0 1 0]     [0 0 1 0]     [1]
                         [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 + [1]              
                         [0 0 0 0]     [0]              
                         [0 0 0 0]     [1]              
                      >= [0]                            
                         [0]                            
                         [0]                            
                         [1]                            
                      =  true()                         
      
         le(s(x),0()) =  [0 0 0 0]     [0]              
                         [0 0 0 0] x + [1]              
                         [0 0 0 1]     [1]              
                         [0 0 0 0]     [1]              
                      >= [0]                            
                         [1]                            
                         [0]                            
                         [0]                            
                      =  false()                        
      
         minus(x,0()) =  [1 0 0 0]     [0]              
                         [1 1 0 1] x + [0]              
                         [1 1 1 1]     [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                              
      
        minus(x,s(y)) =  [1 0 0 0]     [1 1 1 1]     [1]
                         [1 1 0 1] x + [1 1 1 2] y + [2]
                         [1 1 1 1]     [1 1 2 1]     [2]
                         [0 0 0 1]     [0 0 0 0]     [0]
                      >= [1 0 0 0]     [1 1 1 1]     [1]
                         [1 0 0 1] x + [1 1 1 0] y + [0]
                         [1 1 0 1]     [1 1 1 1]     [2]
                         [0 0 0 1]     [0 0 0 0]     [0]
                      =  if(le(x,s(y))                  
                           ,0()                         
                           ,p(minus(x,p(s(y)))))        
      
               p(0()) =  [0]                            
                         [0]                            
                         [0]                            
                         [0]                            
                      >= [0]                            
                         [0]                            
                         [0]                            
                         [0]                            
                      =  0()                            
      
              p(s(x)) =  [1 1 0 0]     [0]              
                         [1 1 0 1] x + [1]              
                         [0 0 1 0]     [0]              
                         [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                              
      
*** 1.1.1.1.1.1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        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
        basic terms: {if,le,minus,p}/{0,false,s,true}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).