1.20/1.24	YES
1.20/1.24	
1.20/1.24	Problem:
1.20/1.24	 +(x,y) -> +(y,x)
1.20/1.24	 *(+(x,y),z) -> +(*(x,z),*(y,z))
1.20/1.24	 *(+(y,x),z) -> +(*(x,z),*(y,z))
1.20/1.24	
1.20/1.24	Proof:
1.20/1.24	 Qed (right-reducible TRS)
1.20/1.24	EOF