YES(O(1),O(n^1))

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs:
  { or(x, true()) -> true()
  , or(true(), y) -> true()
  , or(false(), false()) -> false()
  , mem(x, nil()) -> false()
  , mem(x, set(y)) -> =(x, y)
  , mem(x, union(y, z)) -> or(mem(x, y), mem(x, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(or) = {1, 2}

TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).

     [or](x1, x2) = [1] x1 + [1] x2 + [7]
                                         
           [true] = [7]                  
                                         
          [false] = [3]                  
                                         
    [mem](x1, x2) = [1] x2 + [3]         
                                         
            [nil] = [7]                  
                                         
        [set](x1) = [1] x1 + [7]         
                                         
      [=](x1, x2) = [1] x2 + [1]         
                                         
  [union](x1, x2) = [1] x1 + [1] x2 + [7]

The following symbols are considered usable

  {or, mem}

The order satisfies the following ordering constraints:

         [or(x, true())] = [1] x + [14]              
                         > [7]                       
                         = [true()]                  
                                                     
         [or(true(), y)] = [1] y + [14]              
                         > [7]                       
                         = [true()]                  
                                                     
  [or(false(), false())] = [13]                      
                         > [3]                       
                         = [false()]                 
                                                     
         [mem(x, nil())] = [10]                      
                         > [3]                       
                         = [false()]                 
                                                     
        [mem(x, set(y))] = [1] y + [10]              
                         > [1] y + [1]               
                         = [=(x, y)]                 
                                                     
   [mem(x, union(y, z))] = [1] y + [1] z + [10]      
                         ? [1] y + [1] z + [13]      
                         = [or(mem(x, y), mem(x, z))]
                                                     

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(n^1)).

Strict Trs: { mem(x, union(y, z)) -> or(mem(x, y), mem(x, z)) }
Weak Trs:
  { or(x, true()) -> true()
  , or(true(), y) -> true()
  , or(false(), false()) -> false()
  , mem(x, nil()) -> false()
  , mem(x, set(y)) -> =(x, y) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(n^1))

The weightgap principle applies (using the following nonconstant
growth matrix-interpretation)

The following argument positions are usable:
  Uargs(or) = {1, 2}

TcT has computed the following matrix interpretation satisfying
not(EDA) and not(IDA(1)).

     [or](x1, x2) = [1] x1 + [1] x2 + [0]
                                         
           [true] = [7]                  
                                         
          [false] = [4]                  
                                         
    [mem](x1, x2) = [1] x2 + [0]         
                                         
            [nil] = [7]                  
                                         
        [set](x1) = [1] x1 + [7]         
                                         
      [=](x1, x2) = [1] x2 + [7]         
                                         
  [union](x1, x2) = [1] x1 + [1] x2 + [7]

The following symbols are considered usable

  {or, mem}

The order satisfies the following ordering constraints:

         [or(x, true())] =  [1] x + [7]               
                         >= [7]                       
                         =  [true()]                  
                                                      
         [or(true(), y)] =  [1] y + [7]               
                         >= [7]                       
                         =  [true()]                  
                                                      
  [or(false(), false())] =  [8]                       
                         >  [4]                       
                         =  [false()]                 
                                                      
         [mem(x, nil())] =  [7]                       
                         >  [4]                       
                         =  [false()]                 
                                                      
        [mem(x, set(y))] =  [1] y + [7]               
                         >= [1] y + [7]               
                         =  [=(x, y)]                 
                                                      
   [mem(x, union(y, z))] =  [1] y + [1] z + [7]       
                         >  [1] y + [1] z + [0]       
                         =  [or(mem(x, y), mem(x, z))]
                                                      

Further, it can be verified that all rules not oriented are covered by the weightgap condition.

We are left with following problem, upon which TcT provides the
certificate YES(O(1),O(1)).

Weak Trs:
  { or(x, true()) -> true()
  , or(true(), y) -> true()
  , or(false(), false()) -> false()
  , mem(x, nil()) -> false()
  , mem(x, set(y)) -> =(x, y)
  , mem(x, union(y, z)) -> or(mem(x, y), mem(x, z)) }
Obligation:
  innermost runtime complexity
Answer:
  YES(O(1),O(1))

Empty rules are trivially bounded

Hurray, we answered YES(O(1),O(n^1))