7.12/2.82	YES
7.12/2.82	
7.12/2.82	Problem:
7.12/2.82	 +(0(),x) -> x
7.12/2.82	 +(x,0()) -> x
7.12/2.82	 +(1(),-(1())) -> 0()
7.12/2.82	 +(-(1()),1()) -> 0()
7.12/2.82	 -(0()) -> 0()
7.12/2.82	 -(-(x)) -> x
7.12/2.82	 -(+(x,y)) -> +(-(x),-(y))
7.12/2.82	 +(+(x,y),z) -> +(x,+(y,z))
7.12/2.82	 +(x,y) -> +(y,x)
7.12/2.82	
7.12/2.82	Proof:
7.12/2.82	 Church Rosser Transformation Processor (ac):
7.12/2.82	  f4_AC(0(),x) -> x
7.12/2.82	  f4_AC(x,0()) -> x
7.12/2.82	  f4_AC(1(),-(1())) -> 0()
7.12/2.82	  f4_AC(-(1()),1()) -> 0()
7.12/2.82	  -(0()) -> 0()
7.12/2.82	  -(-(x)) -> x
7.12/2.82	  -(f4_AC(x,y)) -> f4_AC(-(x),-(y))
7.12/2.82	  AC critical peaks: joinable
7.12/2.82	  AC-RPO Processor:
7.12/2.82	   precedence:
7.12/2.82	    1 > 0 > - > f4_AC
7.12/2.82	   status:
7.12/2.82	    
7.12/2.82	   problem:
7.12/2.82	    
7.12/2.82	   Qed
7.12/2.82	EOF