YES Problem: f(h(x,d()),y) -> f(h(y,d()),x) h(c(),x) -> h(x,x) Proof: Church Rosser Transformation Processor (no redundant rules): strict: weak: critical peaks: 1 f(h(d(),d()),y) <-0|0[]- f(h(c(),d()),y) -1|[]-> f(h(y,d()),c()) Redundant Rules Transformation: h(c(),x) -> h(x,x) f(h(x,d()),y) -> f(h(y,d()),x) f(h(y,d()),c()) -> f(h(d(),d()),y) Church Rosser Transformation Processor (no redundant rules): strict: f(h(y,d()),c()) -> f(h(d(),d()),y) f(h(x,d()),y) -> f(h(y,d()),x) h(c(),x) -> h(x,x) weak: critical peaks: 4 f(h(d(),d()),x) <-0|[]- f(h(x,d()),c()) -1|[]-> f(h(c(),d()),x) f(h(c(),d()),y) <-1|[]- f(h(y,d()),c()) -0|[]-> f(h(d(),d()),y) f(h(d(),d()),c()) <-2|0[]- f(h(c(),d()),c()) -0|[]-> f(h(d(),d()),c()) f(h(d(),d()),y) <-2|0[]- f(h(c(),d()),y) -1|[]-> f(h(y,d()),c()) Closedness Processor (*upside-parallel*): Qed