Problem: f(g(x,a(),b())) -> x g(f(h(c(),d())),x,y) -> h(k1(x),k2(y)) k1(a()) -> c() k2(b()) -> d() f(h(k1(a()),k2(b()))) -> f(h(c(),d())) f(h(c(),k2(b()))) -> f(h(c(),d())) f(h(k1(a()),d())) -> f(h(c(),d())) Proof: Church Rosser Transformation Processor: strict: f(g(x,a(),b())) -> x g(f(h(c(),d())),x,y) -> h(k1(x),k2(y)) k1(a()) -> c() k2(b()) -> d() f(h(k1(a()),k2(b()))) -> f(h(c(),d())) f(h(c(),k2(b()))) -> f(h(c(),d())) f(h(k1(a()),d())) -> f(h(c(),d())) weak: critical peaks: 5 f(h(k1(a()),k2(b()))) <-1|0[]- f(g(f(h(c(),d())),a(),b())) -0|[]-> f(h(c(),d())) f(h(c(),k2(b()))) <-2|0,0[]- f(h(k1(a()),k2(b()))) -4|[]-> f(h(c(),d())) f(h(c(),d())) <-2|0,0[]- f(h(k1(a()),d())) -6|[]-> f(h(c(),d())) f(h(k1(a()),d())) <-3|0,1[]- f(h(k1(a()),k2(b()))) -4|[]-> f(h(c(),d())) f(h(c(),d())) <-3|0,1[]- f(h(c(),k2(b()))) -5|[]-> f(h(c(),d())) Closedness Processor (*parallel*): strict: weak: Qed