Problem:
 or(true(),true()) -> true()
 or(x,y) -> or(y,x)

Proof:
 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
  or(true(),true()) -> true()
  critical peaks: joinable
  Matrix Interpretation Processor: dim=1
   
   interpretation:
    [or](x0, x1) = x0 + x1 + 1,
    
    [true] = 0
   orientation:
    or(true(),true()) = 1 >= 0 = true()
   problem:
    
   Qed