3.31/1.53	YES
3.61/1.53	
3.61/1.53	Problem:
3.61/1.53	 f(f(x)) -> f(g(f(x),f(x)))
3.61/1.53	
3.61/1.53	Proof:
3.61/1.53	 Church Rosser Transformation Processor (critical pair closing system, Thm 2.11):
3.61/1.53	  f(f(g(x11,x13))) -> f(g(f(g(x11,x13)),f(g(x11,x13))))
3.61/1.53	  f(f(x14)) -> f(g(f(x14),f(x14)))
3.61/1.53	  critical peaks: joinable
3.61/1.53	  Matrix Interpretation Processor: dim=2
3.61/1.53	   
3.61/1.53	   interpretation:
3.61/1.53	                  [1 0]     [1 0]     [1]
3.61/1.53	    [g](x0, x1) = [0 0]x0 + [0 0]x1 + [0],
3.61/1.53	    
3.61/1.53	              [1 1]     [0]
3.61/1.53	    [f](x0) = [1 1]x0 + [2]
3.61/1.53	   orientation:
3.61/1.53	                       [2 0]      [2 0]      [4]    [2 0]      [2 0]      [3]                                    
3.61/1.53	    f(f(g(x11,x13))) = [2 0]x11 + [2 0]x13 + [6] >= [2 0]x11 + [2 0]x13 + [5] = f(g(f(g(x11,x13)),f(g(x11,x13))))
3.61/1.53	    
3.61/1.53	                [2 2]      [2]    [2 2]      [1]                      
3.61/1.53	    f(f(x14)) = [2 2]x14 + [4] >= [2 2]x14 + [3] = f(g(f(x14),f(x14)))
3.61/1.53	   problem:
3.61/1.53	    
3.61/1.53	   Qed
3.61/1.54	EOF