YES Problem: f(g(x)) -> h(x,x) g(a()) -> b() f(x) -> h(x,x) b() -> a() h(x,y) -> h(g(x),g(y)) g(x) -> x a() -> b() Proof: Church Rosser Transformation Processor: strict: weak: critical peaks: 7 h(x47,x47) <-0|[]- f(g(x47)) -2|[]-> h(g(x47),g(x47)) f(b()) <-1|0[]- f(g(a())) -0|[]-> h(a(),a()) b() <-1|[]- g(a()) -5|[]-> a() h(g(x),g(x)) <-2|[]- f(g(x)) -0|[]-> h(x,x) f(x) <-5|0[]- f(g(x)) -0|[]-> h(x,x) a() <-5|[]- g(a()) -1|[]-> b() g(b()) <-6|0[]- g(a()) -1|[]-> b() Redundant Rules Transformation: f(x) -> h(x,x) g(x) -> x a() -> b() Church Rosser Transformation Processor (no redundant rules): strict: a() -> b() g(x) -> x f(x) -> h(x,x) weak: critical peaks: 0 Closedness Processor (*feeble*): Qed