*** 1 Progress [(O(1),O(n^1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        mem(x,nil()) -> false()
        mem(x,set(y)) -> =(x,y)
        mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
        or(x,true()) -> true()
        or(false(),false()) -> false()
        or(true(),y) -> true()
      Weak DP Rules:
        
      Weak TRS Rules:
        
      Signature:
        {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
      Obligation:
        Innermost
        basic terms: {mem,or}/{=,false,nil,set,true,union}
    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(or) = {1,2}
        
        Following symbols are considered usable:
          {}
        TcT has computed the following interpretation:
              p(=) = [0]                   
          p(false) = [3]                   
            p(mem) = [4] x2 + [4]          
            p(nil) = [1]                   
             p(or) = [1] x1 + [1] x2 + [12]
            p(set) = [3]                   
           p(true) = [8]                   
          p(union) = [1] x1 + [1] x2 + [6] 
        
        Following rules are strictly oriented:
               mem(x,nil()) = [8]                  
                            > [3]                  
                            = false()              
        
              mem(x,set(y)) = [16]                 
                            > [0]                  
                            = =(x,y)               
        
          mem(x,union(y,z)) = [4] y + [4] z + [28] 
                            > [4] y + [4] z + [20] 
                            = or(mem(x,y),mem(x,z))
        
               or(x,true()) = [1] x + [20]         
                            > [8]                  
                            = true()               
        
        or(false(),false()) = [18]                 
                            > [3]                  
                            = false()              
        
               or(true(),y) = [1] y + [20]         
                            > [8]                  
                            = true()               
        
        
        Following rules are (at-least) weakly oriented:
        
      Further, it can be verified that all rules not oriented are covered by the weightgap condition.
*** 1.1 Progress [(O(1),O(1))]  ***
    Considered Problem:
      Strict DP Rules:
        
      Strict TRS Rules:
        
      Weak DP Rules:
        
      Weak TRS Rules:
        mem(x,nil()) -> false()
        mem(x,set(y)) -> =(x,y)
        mem(x,union(y,z)) -> or(mem(x,y),mem(x,z))
        or(x,true()) -> true()
        or(false(),false()) -> false()
        or(true(),y) -> true()
      Signature:
        {mem/2,or/2} / {=/2,false/0,nil/0,set/1,true/0,union/2}
      Obligation:
        Innermost
        basic terms: {mem,or}/{=,false,nil,set,true,union}
    Applied Processor:
      EmptyProcessor
    Proof:
      The problem is already closed. The intended complexity is O(1).