1.61/0.87	YES
1.61/0.87	
1.61/0.87	Problem:
1.61/0.87	 f(x1,g(x2)) -> f(x1,g(x1))
1.61/0.87	 f(g(y1),y2) -> f(g(y1),g(y1))
1.61/0.87	 g(a()) -> g(b())
1.61/0.87	 b() -> a()
1.61/0.87	
1.61/0.87	Proof:
1.61/0.87	 Church Rosser Transformation Processor (no redundant rules):
1.61/0.87	  strict:
1.61/0.87	   b() -> a()
1.61/0.87	   g(a()) -> g(b())
1.61/0.87	   f(g(y1),y2) -> f(g(y1),g(y1))
1.61/0.87	   f(x1,g(x2)) -> f(x1,g(x1))
1.61/0.87	  weak:
1.61/0.87	   
1.61/0.87	  critical peaks: 4
1.61/0.87	   f(g(b()),y2) <-1|0[]- f(g(a()),y2) -2|[]-> f(g(a()),g(a()))
1.61/0.87	   f(x1,g(b())) <-1|1[]- f(x1,g(a())) -3|[]-> f(x1,g(x1))
1.61/0.87	   f(g(x32),g(x32)) <-2|[]- f(g(x32),g(x2)) -3|[]-> f(g(x32),g(g(x32)))
1.61/0.87	   f(g(y1),g(g(y1))) <-3|[]- f(g(y1),g(x35)) -2|[]-> f(g(y1),g(y1))
1.61/0.87	  Closedness Processor (*development*):
1.61/0.87	   
1.61/0.87	   Qed
1.61/0.88	EOF