Problem: f(x) -> g(f(x)) h(x) -> p(h(x)) f(x) -> h(f(x)) g(x) -> p(p(h(x))) Proof: Church Rosser Transformation Processor (star): strict: weak: g(0)(x) -> p(0)(p(0)(h(0)(x))) f(0)(x) -> h(0)(f(0)(x)) h(0)(x) -> p(0)(h(0)(x)) f(0)(x) -> g(0)(f(0)(x)) critical peaks: 2 g(f(x)) <-0|[]- f(x) -2|[]-> h(f(x)) h(f(x)) <-2|[]- f(x) -0|[]-> g(f(x)) Shift Processor lab=left (dd): strict: f(x) -> g(f(x)) f(x) -> h(f(x)) g(f(x)) -> p(p(h(f(x)))) h(f(x)) -> p(h(f(x))) p(h(f(x))) -> p(p(h(f(x)))) f(x) -> h(f(x)) f(x) -> g(f(x)) h(f(x)) -> p(h(f(x))) p(h(f(x))) -> p(p(h(f(x)))) g(f(x)) -> p(p(h(f(x)))) weak: f(x) -> g(f(x)) h(x) -> p(h(x)) f(x) -> h(f(x)) g(x) -> p(p(h(x))) Shift Processor (ldh) lab=left (force): strict: weak: Rule Labeling Processor: strict: weak: rule labeling (right): f(x) -> g(f(x)): 1 h(x) -> p(h(x)): 0 f(x) -> h(f(x)): 1 g(x) -> p(p(h(x))): 0 Decreasing Processor: The following diagrams are decreasing: peak: g(f(x)) <-0|[1,1]- f(x) -2|[1,1]-> h(f(x)) joins: g(f(x)) -3|[1,0]-> p(p(h(f(x)))) h(f(x)) -1|[1,0]-> p(h(f(x))) -1|0[1,0]-> p(p(h(f(x)))) peak: h(f(x)) <-2|[1,1]- f(x) -0|[1,1]-> g(f(x)) joins: h(f(x)) -1|[1,0]-> p(h(f(x))) -1|0[1,0]-> p(p(h(f(x)))) g(f(x)) -3|[1,0]-> p(p(h(f(x)))) Qed