0.53/0.57	YES
0.53/0.57	
0.53/0.57	Problem:
0.53/0.57	 f(g(h(x))) -> g(f(h(g(x))))
0.53/0.57	 f(x) -> x
0.53/0.57	 g(x) -> x
0.53/0.57	 h(x) -> x
0.53/0.57	
0.53/0.57	Proof:
0.53/0.57	 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
0.53/0.57	  g(x33) -> x33
0.53/0.57	  f(x35) -> x35
0.53/0.57	  h(x59) -> x59
0.53/0.57	  critical peaks: joinable
0.53/0.57	  Matrix Interpretation Processor: dim=1
0.53/0.57	   
0.53/0.57	   interpretation:
0.53/0.57	    [g](x0) = x0 + 1,
0.53/0.57	    
0.53/0.57	    [h](x0) = x0 + 1,
0.53/0.57	    
0.53/0.57	    [f](x0) = x0 + 1
0.53/0.57	   orientation:
0.53/0.57	    g(x33) = x33 + 1 >= x33 = x33
0.53/0.57	    
0.53/0.57	    f(x35) = x35 + 1 >= x35 = x35
0.53/0.57	    
0.53/0.57	    h(x59) = x59 + 1 >= x59 = x59
0.53/0.57	   problem:
0.53/0.57	    
0.53/0.57	   Qed
0.63/0.58	EOF