2.76/1.79	YES
2.76/1.79	
2.76/1.79	Problem:
2.76/1.79	 f(a()) -> f(f(a()))
2.76/1.79	 a() -> b()
2.76/1.79	 f(x) -> f(b())
2.76/1.79	
2.76/1.79	Proof:
2.76/1.79	 Church Rosser Transformation Processor (no redundant rules):
2.76/1.79	  strict:
2.76/1.79	   f(x) -> f(b())
2.76/1.79	   a() -> b()
2.76/1.79	   f(a()) -> f(f(a()))
2.76/1.79	  weak:
2.76/1.79	   
2.76/1.79	  critical peaks: 3
2.76/1.79	   f(b()) <-0|[]- f(a()) -2|[]-> f(f(a()))
2.76/1.79	   f(b()) <-1|0[]- f(a()) -2|[]-> f(f(a()))
2.76/1.79	   f(f(a())) <-2|[]- f(a()) -0|[]-> f(b())
2.76/1.79	  Closedness Processor (*upside-parallel*):
2.76/1.79	   
2.76/1.79	   Qed
3.37/1.79	EOF