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