TRS:
 {       not(x) -> xor(x, true()),
  implies(x, y) -> xor(and(x, y), xor(x, true())),
       or(x, y) -> xor(and(x, y), xor(x, y)),
        =(x, y) -> xor(x, xor(y, true()))}
 LMPO:
  Quasi-Precedence:
  empty
  
Normal:
   pi(=) = [1,2], pi(or) = [1,2], pi(implies) = [1,2], pi(not) = [1]
  
Safe:
   
  
Predicative System:
   {      not(x;) -> xor(x,true();),
    implies(x,y;) -> xor(and(x,y;),xor(x,true(););),
         or(x,y;) -> xor(and(x,y;),xor(x,y;);),
          =(x,y;) -> xor(x,xor(y,true(););)}
  

   
  

  Qed