0.53/0.78	YES
0.53/0.78	
0.53/0.78	Problem:
0.53/0.78	 or(true(),true()) -> true()
0.53/0.78	 or(x,y) -> or(y,x)
0.53/0.78	
0.53/0.78	Proof:
0.53/0.78	 Church Rosser Transformation Processor (critical pair closing system, Thm 2.4):
0.53/0.78	  or(true(),true()) -> true()
0.53/0.78	  critical peaks: joinable
0.53/0.78	  Matrix Interpretation Processor: dim=1
0.53/0.78	   
0.53/0.78	   interpretation:
0.53/0.78	    [or](x0, x1) = x0 + 2x1 + 1,
0.53/0.78	    
0.53/0.78	    [true] = 4
0.53/0.78	   orientation:
0.53/0.78	    or(true(),true()) = 13 >= 4 = true()
0.53/0.78	   problem:
0.53/0.78	    
0.53/0.78	   Qed
0.53/0.78	EOF