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