6.41/2.52	YES
6.41/2.52	
6.41/2.52	Problem:
6.41/2.52	 +(a(),x) -> a()
6.41/2.52	 +(b(),g(a())) -> a()
6.41/2.52	 +(0(),x) -> x
6.41/2.52	 +(x,+(y,z)) -> +(+(x,y),z)
6.41/2.52	 +(+(x,y),z) -> +(x,+(y,z))
6.41/2.52	 +(x,y) -> +(y,x)
6.41/2.52	
6.41/2.52	Proof:
6.41/2.52	 Church Rosser Transformation Processor (ac):
6.41/2.52	  f5_AC(a(),x) -> a()
6.41/2.52	  f5_AC(b(),g(a())) -> a()
6.41/2.52	  f5_AC(0(),x) -> x
6.41/2.52	  AC critical peaks: joinable
6.41/2.52	  AC-KBO Processor:
6.41/2.52	   precedence:
6.41/2.52	    g > 0 > f5_AC > b > a
6.41/2.52	    weight function:
6.41/2.52	     w0 = 1
6.41/2.52	     w(0) = w(g) = 4
6.41/2.52	     w(a) = 2
6.41/2.52	     w(b) = 1
6.41/2.52	     w(f5_AC) = 0
6.41/2.52	    problem:
6.41/2.52	     
6.41/2.52	    Qed
6.41/2.53	EOF