1.59/1.19	YES
1.59/1.19	
1.59/1.19	Problem:
1.59/1.19	 +(0(),y) -> y
1.59/1.19	 +(s(0()),y) -> s(y)
1.59/1.19	 s(s(x)) -> x
1.59/1.19	
1.59/1.19	Proof:
1.59/1.19	 Church Rosser Transformation Processor:
1.59/1.19	  
1.59/1.19	  critical peaks: joinable
1.59/1.19	  Qed
1.66/1.19	EOF