TRS:
 {       or(true(), y) -> true(),
         or(x, true()) -> 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))}
 LMPO:
  Quasi-Precedence:
  mem > or
  empty
  
Normal:
   pi(mem) = [1,2]
  
Safe:
   pi(or) = [1,2]
  
Predicative System:
   {       or(;true(),y) -> true(),
           or(;x,true()) -> 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;))}
  

   
  

  Qed