WORST_CASE(?,O(n^2))
* Step 1: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq(0(),0()) -> true()
            eq(0(),s(X)) -> false()
            eq(s(X),0()) -> false()
            eq(s(X),s(Y)) -> eq(X,Y)
            ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
            ifrm(true(),N,add(M,X)) -> rm(N,X)
            purge(add(N,X)) -> add(N,purge(rm(N,X)))
            purge(nil()) -> nil()
            rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
            rm(N,nil()) -> nil()
        - Signature:
            {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,s
            ,true}
    + 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(add) = {2},
          uargs(ifrm) = {1},
          uargs(purge) = {1}
        
        Following symbols are considered usable:
          {eq,ifrm,purge,rm}
        TcT has computed the following interpretation:
              p(0) = [2]         
            p(add) = [1] x2 + [0]
             p(eq) = [0]         
          p(false) = [0]         
           p(ifrm) = [1] x1 + [0]
            p(nil) = [0]         
          p(purge) = [1] x1 + [1]
             p(rm) = [0]         
              p(s) = [1]         
           p(true) = [0]         
        
        Following rules are strictly oriented:
        purge(nil()) = [1]  
                     > [0]  
                     = nil()
        
        
        Following rules are (at-least) weakly oriented:
                     eq(0(),0()) =  [0]                     
                                 >= [0]                     
                                 =  true()                  
        
                    eq(0(),s(X)) =  [0]                     
                                 >= [0]                     
                                 =  false()                 
        
                    eq(s(X),0()) =  [0]                     
                                 >= [0]                     
                                 =  false()                 
        
                   eq(s(X),s(Y)) =  [0]                     
                                 >= [0]                     
                                 =  eq(X,Y)                 
        
        ifrm(false(),N,add(M,X)) =  [0]                     
                                 >= [0]                     
                                 =  add(M,rm(N,X))          
        
         ifrm(true(),N,add(M,X)) =  [0]                     
                                 >= [0]                     
                                 =  rm(N,X)                 
        
                 purge(add(N,X)) =  [1] X + [1]             
                                 >= [1]                     
                                 =  add(N,purge(rm(N,X)))   
        
                  rm(N,add(M,X)) =  [0]                     
                                 >= [0]                     
                                 =  ifrm(eq(N,M),N,add(M,X))
        
                     rm(N,nil()) =  [0]                     
                                 >= [0]                     
                                 =  nil()                   
        
* Step 2: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq(0(),0()) -> true()
            eq(0(),s(X)) -> false()
            eq(s(X),0()) -> false()
            eq(s(X),s(Y)) -> eq(X,Y)
            ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
            ifrm(true(),N,add(M,X)) -> rm(N,X)
            purge(add(N,X)) -> add(N,purge(rm(N,X)))
            rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
            rm(N,nil()) -> nil()
        - Weak TRS:
            purge(nil()) -> nil()
        - Signature:
            {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,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(add) = {2},
            uargs(ifrm) = {1},
            uargs(purge) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(0) = [0]                  
              p(add) = [1] x1 + [1] x2 + [0]
               p(eq) = [12]                 
            p(false) = [0]                  
             p(ifrm) = [1] x1 + [1] x3 + [0]
              p(nil) = [6]                  
            p(purge) = [1] x1 + [0]         
               p(rm) = [1] x2 + [0]         
                p(s) = [1]                  
             p(true) = [0]                  
          
          Following rules are strictly oriented:
           eq(0(),0()) = [12]   
                       > [0]    
                       = true() 
          
          eq(0(),s(X)) = [12]   
                       > [0]    
                       = false()
          
          eq(s(X),0()) = [12]   
                       > [0]    
                       = false()
          
          
          Following rules are (at-least) weakly oriented:
                     eq(s(X),s(Y)) =  [12]                    
                                   >= [12]                    
                                   =  eq(X,Y)                 
          
          ifrm(false(),N,add(M,X)) =  [1] M + [1] X + [0]     
                                   >= [1] M + [1] X + [0]     
                                   =  add(M,rm(N,X))          
          
           ifrm(true(),N,add(M,X)) =  [1] M + [1] X + [0]     
                                   >= [1] X + [0]             
                                   =  rm(N,X)                 
          
                   purge(add(N,X)) =  [1] N + [1] X + [0]     
                                   >= [1] N + [1] X + [0]     
                                   =  add(N,purge(rm(N,X)))   
          
                      purge(nil()) =  [6]                     
                                   >= [6]                     
                                   =  nil()                   
          
                    rm(N,add(M,X)) =  [1] M + [1] X + [0]     
                                   >= [1] M + [1] X + [12]    
                                   =  ifrm(eq(N,M),N,add(M,X))
          
                       rm(N,nil()) =  [6]                     
                                   >= [6]                     
                                   =  nil()                   
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 3: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq(s(X),s(Y)) -> eq(X,Y)
            ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
            ifrm(true(),N,add(M,X)) -> rm(N,X)
            purge(add(N,X)) -> add(N,purge(rm(N,X)))
            rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
            rm(N,nil()) -> nil()
        - Weak TRS:
            eq(0(),0()) -> true()
            eq(0(),s(X)) -> false()
            eq(s(X),0()) -> false()
            purge(nil()) -> nil()
        - Signature:
            {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,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(add) = {2},
            uargs(ifrm) = {1},
            uargs(purge) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(0) = [4]                   
              p(add) = [1] x1 + [1] x2 + [10]
               p(eq) = [8]                   
            p(false) = [4]                   
             p(ifrm) = [1] x1 + [1] x3 + [0] 
              p(nil) = [1]                   
            p(purge) = [1] x1 + [0]          
               p(rm) = [1] x2 + [5]          
                p(s) = [1] x1 + [8]          
             p(true) = [5]                   
          
          Following rules are strictly oriented:
          ifrm(true(),N,add(M,X)) = [1] M + [1] X + [15]
                                  > [1] X + [5]         
                                  = rm(N,X)             
          
                      rm(N,nil()) = [6]                 
                                  > [1]                 
                                  = nil()               
          
          
          Following rules are (at-least) weakly oriented:
                       eq(0(),0()) =  [8]                     
                                   >= [5]                     
                                   =  true()                  
          
                      eq(0(),s(X)) =  [8]                     
                                   >= [4]                     
                                   =  false()                 
          
                      eq(s(X),0()) =  [8]                     
                                   >= [4]                     
                                   =  false()                 
          
                     eq(s(X),s(Y)) =  [8]                     
                                   >= [8]                     
                                   =  eq(X,Y)                 
          
          ifrm(false(),N,add(M,X)) =  [1] M + [1] X + [14]    
                                   >= [1] M + [1] X + [15]    
                                   =  add(M,rm(N,X))          
          
                   purge(add(N,X)) =  [1] N + [1] X + [10]    
                                   >= [1] N + [1] X + [15]    
                                   =  add(N,purge(rm(N,X)))   
          
                      purge(nil()) =  [1]                     
                                   >= [1]                     
                                   =  nil()                   
          
                    rm(N,add(M,X)) =  [1] M + [1] X + [15]    
                                   >= [1] M + [1] X + [18]    
                                   =  ifrm(eq(N,M),N,add(M,X))
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 4: WeightGap WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq(s(X),s(Y)) -> eq(X,Y)
            ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
            purge(add(N,X)) -> add(N,purge(rm(N,X)))
            rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
        - Weak TRS:
            eq(0(),0()) -> true()
            eq(0(),s(X)) -> false()
            eq(s(X),0()) -> false()
            ifrm(true(),N,add(M,X)) -> rm(N,X)
            purge(nil()) -> nil()
            rm(N,nil()) -> nil()
        - Signature:
            {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,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(add) = {2},
            uargs(ifrm) = {1},
            uargs(purge) = {1}
          
          Following symbols are considered usable:
            all
          TcT has computed the following interpretation:
                p(0) = [0]          
              p(add) = [1] x2 + [8] 
               p(eq) = [4]          
            p(false) = [2]          
             p(ifrm) = [1] x1 + [12]
              p(nil) = [0]          
            p(purge) = [1] x1 + [2] 
               p(rm) = [2]          
                p(s) = [0]          
             p(true) = [4]          
          
          Following rules are strictly oriented:
          ifrm(false(),N,add(M,X)) = [14]          
                                   > [10]          
                                   = add(M,rm(N,X))
          
          
          Following rules are (at-least) weakly oriented:
                      eq(0(),0()) =  [4]                     
                                  >= [4]                     
                                  =  true()                  
          
                     eq(0(),s(X)) =  [4]                     
                                  >= [2]                     
                                  =  false()                 
          
                     eq(s(X),0()) =  [4]                     
                                  >= [2]                     
                                  =  false()                 
          
                    eq(s(X),s(Y)) =  [4]                     
                                  >= [4]                     
                                  =  eq(X,Y)                 
          
          ifrm(true(),N,add(M,X)) =  [16]                    
                                  >= [2]                     
                                  =  rm(N,X)                 
          
                  purge(add(N,X)) =  [1] X + [10]            
                                  >= [12]                    
                                  =  add(N,purge(rm(N,X)))   
          
                     purge(nil()) =  [2]                     
                                  >= [0]                     
                                  =  nil()                   
          
                   rm(N,add(M,X)) =  [2]                     
                                  >= [16]                    
                                  =  ifrm(eq(N,M),N,add(M,X))
          
                      rm(N,nil()) =  [2]                     
                                  >= [0]                     
                                  =  nil()                   
          
        Further, it can be verified that all rules not oriented are covered by the weightgap condition.
* Step 5: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq(s(X),s(Y)) -> eq(X,Y)
            purge(add(N,X)) -> add(N,purge(rm(N,X)))
            rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
        - Weak TRS:
            eq(0(),0()) -> true()
            eq(0(),s(X)) -> false()
            eq(s(X),0()) -> false()
            ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
            ifrm(true(),N,add(M,X)) -> rm(N,X)
            purge(nil()) -> nil()
            rm(N,nil()) -> nil()
        - Signature:
            {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,s
            ,true}
    + 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(add) = {2},
          uargs(ifrm) = {1},
          uargs(purge) = {1}
        
        Following symbols are considered usable:
          {eq,ifrm,purge,rm}
        TcT has computed the following interpretation:
              p(0) = [0]                  
            p(add) = [1] x2 + [2]         
             p(eq) = [0]                  
          p(false) = [0]                  
           p(ifrm) = [8] x1 + [1] x3 + [1]
            p(nil) = [1]                  
          p(purge) = [8] x1 + [8]         
             p(rm) = [1] x2 + [1]         
              p(s) = [0]                  
           p(true) = [0]                  
        
        Following rules are strictly oriented:
        purge(add(N,X)) = [8] X + [24]         
                        > [8] X + [18]         
                        = add(N,purge(rm(N,X)))
        
        
        Following rules are (at-least) weakly oriented:
                     eq(0(),0()) =  [0]                     
                                 >= [0]                     
                                 =  true()                  
        
                    eq(0(),s(X)) =  [0]                     
                                 >= [0]                     
                                 =  false()                 
        
                    eq(s(X),0()) =  [0]                     
                                 >= [0]                     
                                 =  false()                 
        
                   eq(s(X),s(Y)) =  [0]                     
                                 >= [0]                     
                                 =  eq(X,Y)                 
        
        ifrm(false(),N,add(M,X)) =  [1] X + [3]             
                                 >= [1] X + [3]             
                                 =  add(M,rm(N,X))          
        
         ifrm(true(),N,add(M,X)) =  [1] X + [3]             
                                 >= [1] X + [1]             
                                 =  rm(N,X)                 
        
                    purge(nil()) =  [16]                    
                                 >= [1]                     
                                 =  nil()                   
        
                  rm(N,add(M,X)) =  [1] X + [3]             
                                 >= [1] X + [3]             
                                 =  ifrm(eq(N,M),N,add(M,X))
        
                     rm(N,nil()) =  [2]                     
                                 >= [1]                     
                                 =  nil()                   
        
* Step 6: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq(s(X),s(Y)) -> eq(X,Y)
            rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
        - Weak TRS:
            eq(0(),0()) -> true()
            eq(0(),s(X)) -> false()
            eq(s(X),0()) -> false()
            ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
            ifrm(true(),N,add(M,X)) -> rm(N,X)
            purge(add(N,X)) -> add(N,purge(rm(N,X)))
            purge(nil()) -> nil()
            rm(N,nil()) -> nil()
        - Signature:
            {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,s
            ,true}
    + Applied Processor:
        NaturalMI {miDimension = 2, miDegree = 2, 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(add) = {2},
          uargs(ifrm) = {1},
          uargs(purge) = {1}
        
        Following symbols are considered usable:
          {eq,ifrm,purge,rm}
        TcT has computed the following interpretation:
              p(0) = [0]                      
                     [1]                      
            p(add) = [1 4] x2 + [0]           
                     [0 1]      [1]           
             p(eq) = [0 0] x2 + [0]           
                     [0 1]      [0]           
          p(false) = [0]                      
                     [0]                      
           p(ifrm) = [4 0] x1 + [1 1] x3 + [1]
                     [0 0]      [0 1]      [0]
            p(nil) = [4]                      
                     [1]                      
          p(purge) = [2 4] x1 + [0]           
                     [0 1]      [0]           
             p(rm) = [1 1] x2 + [2]           
                     [0 1]      [0]           
              p(s) = [0 0] x1 + [0]           
                     [0 1]      [0]           
           p(true) = [0]                      
                     [0]                      
        
        Following rules are strictly oriented:
        rm(N,add(M,X)) = [1 5] X + [3]           
                         [0 1]     [1]           
                       > [1 5] X + [2]           
                         [0 1]     [1]           
                       = ifrm(eq(N,M),N,add(M,X))
        
        
        Following rules are (at-least) weakly oriented:
                     eq(0(),0()) =  [0]                  
                                    [1]                  
                                 >= [0]                  
                                    [0]                  
                                 =  true()               
        
                    eq(0(),s(X)) =  [0 0] X + [0]        
                                    [0 1]     [0]        
                                 >= [0]                  
                                    [0]                  
                                 =  false()              
        
                    eq(s(X),0()) =  [0]                  
                                    [1]                  
                                 >= [0]                  
                                    [0]                  
                                 =  false()              
        
                   eq(s(X),s(Y)) =  [0 0] Y + [0]        
                                    [0 1]     [0]        
                                 >= [0 0] Y + [0]        
                                    [0 1]     [0]        
                                 =  eq(X,Y)              
        
        ifrm(false(),N,add(M,X)) =  [1 5] X + [2]        
                                    [0 1]     [1]        
                                 >= [1 5] X + [2]        
                                    [0 1]     [1]        
                                 =  add(M,rm(N,X))       
        
         ifrm(true(),N,add(M,X)) =  [1 5] X + [2]        
                                    [0 1]     [1]        
                                 >= [1 1] X + [2]        
                                    [0 1]     [0]        
                                 =  rm(N,X)              
        
                 purge(add(N,X)) =  [2 12] X + [4]       
                                    [0  1]     [1]       
                                 >= [2 10] X + [4]       
                                    [0  1]     [1]       
                                 =  add(N,purge(rm(N,X)))
        
                    purge(nil()) =  [12]                 
                                    [1]                  
                                 >= [4]                  
                                    [1]                  
                                 =  nil()                
        
                     rm(N,nil()) =  [7]                  
                                    [1]                  
                                 >= [4]                  
                                    [1]                  
                                 =  nil()                
        
* Step 7: NaturalMI WORST_CASE(?,O(n^2))
    + Considered Problem:
        - Strict TRS:
            eq(s(X),s(Y)) -> eq(X,Y)
        - Weak TRS:
            eq(0(),0()) -> true()
            eq(0(),s(X)) -> false()
            eq(s(X),0()) -> false()
            ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
            ifrm(true(),N,add(M,X)) -> rm(N,X)
            purge(add(N,X)) -> add(N,purge(rm(N,X)))
            purge(nil()) -> nil()
            rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
            rm(N,nil()) -> nil()
        - Signature:
            {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,s
            ,true}
    + Applied Processor:
        NaturalMI {miDimension = 3, miDegree = 2, miKind = Algebraic, uargs = UArgs, urules = URules, selector = Just any strict-rules}
    + Details:
        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(add) = {2},
          uargs(ifrm) = {1},
          uargs(purge) = {1}
        
        Following symbols are considered usable:
          {eq,ifrm,purge,rm}
        TcT has computed the following interpretation:
              p(0) = [0]                                       
                     [0]                                       
                     [3]                                       
            p(add) = [0 0 0]      [1 0 2]      [0]             
                     [0 0 0] x1 + [0 0 1] x2 + [0]             
                     [0 0 1]      [0 0 1]      [2]             
             p(eq) = [0 0 0]      [0 0 1]      [1]             
                     [0 0 0] x1 + [0 0 0] x2 + [3]             
                     [2 0 0]      [0 0 0]      [0]             
          p(false) = [2]                                       
                     [1]                                       
                     [0]                                       
           p(ifrm) = [1 1 0]      [0 0 0]      [1 1 0]      [0]
                     [0 1 0] x1 + [0 2 0] x2 + [0 1 1] x3 + [0]
                     [0 0 0]      [0 0 0]      [0 0 1]      [0]
            p(nil) = [2]                                       
                     [0]                                       
                     [0]                                       
          p(purge) = [2 0 2]      [0]                          
                     [0 0 2] x1 + [3]                          
                     [0 0 1]      [0]                          
             p(rm) = [0 0 0]      [1 0 1]      [2]             
                     [0 2 0] x1 + [0 0 2] x2 + [1]             
                     [0 0 0]      [0 0 1]      [0]             
              p(s) = [1 1 3]      [0]                          
                     [0 0 1] x1 + [0]                          
                     [0 0 1]      [1]                          
           p(true) = [0]                                       
                     [2]                                       
                     [0]                                       
        
        Following rules are strictly oriented:
        eq(s(X),s(Y)) = [0 0 0]     [0 0 1]     [2]
                        [0 0 0] X + [0 0 0] Y + [3]
                        [2 2 6]     [0 0 0]     [0]
                      > [0 0 0]     [0 0 1]     [1]
                        [0 0 0] X + [0 0 0] Y + [3]
                        [2 0 0]     [0 0 0]     [0]
                      = eq(X,Y)                    
        
        
        Following rules are (at-least) weakly oriented:
                     eq(0(),0()) =  [4]                                    
                                    [3]                                    
                                    [0]                                    
                                 >= [0]                                    
                                    [2]                                    
                                    [0]                                    
                                 =  true()                                 
        
                    eq(0(),s(X)) =  [0 0 1]     [2]                        
                                    [0 0 0] X + [3]                        
                                    [0 0 0]     [0]                        
                                 >= [2]                                    
                                    [1]                                    
                                    [0]                                    
                                 =  false()                                
        
                    eq(s(X),0()) =  [0 0 0]     [4]                        
                                    [0 0 0] X + [3]                        
                                    [2 2 6]     [0]                        
                                 >= [2]                                    
                                    [1]                                    
                                    [0]                                    
                                 =  false()                                
        
        ifrm(false(),N,add(M,X)) =  [0 0 0]     [0 0 0]     [1 0 3]     [3]
                                    [0 0 1] M + [0 2 0] N + [0 0 2] X + [3]
                                    [0 0 1]     [0 0 0]     [0 0 1]     [2]
                                 >= [0 0 0]     [1 0 3]     [2]            
                                    [0 0 0] M + [0 0 1] X + [0]            
                                    [0 0 1]     [0 0 1]     [2]            
                                 =  add(M,rm(N,X))                         
        
         ifrm(true(),N,add(M,X)) =  [0 0 0]     [0 0 0]     [1 0 3]     [2]
                                    [0 0 1] M + [0 2 0] N + [0 0 2] X + [4]
                                    [0 0 1]     [0 0 0]     [0 0 1]     [2]
                                 >= [0 0 0]     [1 0 1]     [2]            
                                    [0 2 0] N + [0 0 2] X + [1]            
                                    [0 0 0]     [0 0 1]     [0]            
                                 =  rm(N,X)                                
        
                 purge(add(N,X)) =  [0 0 2]     [2 0 6]     [4]            
                                    [0 0 2] N + [0 0 2] X + [7]            
                                    [0 0 1]     [0 0 1]     [2]            
                                 >= [0 0 0]     [2 0 6]     [4]            
                                    [0 0 0] N + [0 0 1] X + [0]            
                                    [0 0 1]     [0 0 1]     [2]            
                                 =  add(N,purge(rm(N,X)))                  
        
                    purge(nil()) =  [4]                                    
                                    [3]                                    
                                    [0]                                    
                                 >= [2]                                    
                                    [0]                                    
                                    [0]                                    
                                 =  nil()                                  
        
                  rm(N,add(M,X)) =  [0 0 1]     [0 0 0]     [1 0 3]     [4]
                                    [0 0 2] M + [0 2 0] N + [0 0 2] X + [5]
                                    [0 0 1]     [0 0 0]     [0 0 1]     [2]
                                 >= [0 0 1]     [0 0 0]     [1 0 3]     [4]
                                    [0 0 1] M + [0 2 0] N + [0 0 2] X + [5]
                                    [0 0 1]     [0 0 0]     [0 0 1]     [2]
                                 =  ifrm(eq(N,M),N,add(M,X))               
        
                     rm(N,nil()) =  [0 0 0]     [4]                        
                                    [0 2 0] N + [1]                        
                                    [0 0 0]     [0]                        
                                 >= [2]                                    
                                    [0]                                    
                                    [0]                                    
                                 =  nil()                                  
        
* Step 8: EmptyProcessor WORST_CASE(?,O(1))
    + Considered Problem:
        - Weak TRS:
            eq(0(),0()) -> true()
            eq(0(),s(X)) -> false()
            eq(s(X),0()) -> false()
            eq(s(X),s(Y)) -> eq(X,Y)
            ifrm(false(),N,add(M,X)) -> add(M,rm(N,X))
            ifrm(true(),N,add(M,X)) -> rm(N,X)
            purge(add(N,X)) -> add(N,purge(rm(N,X)))
            purge(nil()) -> nil()
            rm(N,add(M,X)) -> ifrm(eq(N,M),N,add(M,X))
            rm(N,nil()) -> nil()
        - Signature:
            {eq/2,ifrm/3,purge/1,rm/2} / {0/0,add/2,false/0,nil/0,s/1,true/0}
        - Obligation:
            innermost runtime complexity wrt. defined symbols {eq,ifrm,purge,rm} and constructors {0,add,false,nil,s
            ,true}
    + Applied Processor:
        EmptyProcessor
    + Details:
        The problem is already closed. The intended complexity is O(1).

WORST_CASE(?,O(n^2))