Problem:
 or(x,T()) -> T()
 or(x,F()) -> x
 or(x,y) -> or(y,x)

Proof:
 Commute Transformation Processor:
  or(x,T()) -> T()
  or(T(),x) -> T()
  or(x,F()) -> x
  or(F(),x) -> x
  or(x,y) -> or(y,x)
  Church Rosser Transformation Processor:
   
   strict:
    
   weak:
    
   critical peaks: 16
   T() <-0|[]- or(T(),T()) -1|[]-> T()
   T() <-0|[]- or(F(),T()) -3|[]-> T()
   T() <-0|[]- or(x,T()) -4|[]-> or(T(),x)
   T() <-1|[]- or(T(),T()) -0|[]-> T()
   T() <-1|[]- or(T(),F()) -2|[]-> T()
   T() <-1|[]- or(T(),y) -4|[]-> or(y,T())
   T() <-2|[]- or(T(),F()) -1|[]-> T()
   F() <-2|[]- or(F(),F()) -3|[]-> F()
   x <-2|[]- or(x,F()) -4|[]-> or(F(),x)
   T() <-3|[]- or(F(),T()) -0|[]-> T()
   F() <-3|[]- or(F(),F()) -2|[]-> F()
   y <-3|[]- or(F(),y) -4|[]-> or(y,F())
   or(T(),x) <-4|[]- or(x,T()) -0|[]-> T()
   or(x,T()) <-4|[]- or(T(),x) -1|[]-> T()
   or(F(),x) <-4|[]- or(x,F()) -2|[]-> x
   or(x,F()) <-4|[]- or(F(),x) -3|[]-> x
   Closedness Processor (*parallel*):
    
    strict:
     
    weak:
     
    Qed