Problem: or(true(),true()) -> true() or(x,y) -> or(y,x) Proof: Church Rosser Transformation Processor: strict: or(true(),true()) -> true() or(x,y) -> or(y,x) weak: critical peaks: 2 true() <-0|[]- or(true(),true()) -1|[]-> or(true(),true()) or(true(),true()) <-1|[]- or(true(),true()) -0|[]-> true() Closedness Processor (*parallel*): strict: weak: Qed