Problem: join(x,meet(x,y)) -> x meet(x,join(y,z)) -> join(meet(x,y),meet(x,z)) meet(x,x) -> x join(x,x) -> x meet(meet(x,y),z) -> meet(x,meet(y,z)) meet(x,y) -> meet(y,x) join(join(x,y),z) -> join(x,join(y,z)) join(x,y) -> join(y,x) Proof: Church Rosser Transformation Processor (ac): f3_AC(x,f5_AC(x,y)) -> x f5_AC(x,f3_AC(y,z)) -> f3_AC(f5_AC(x,y),f5_AC(x,z)) f5_AC(x,x) -> x f3_AC(x,x) -> x AC critical peaks: joinable AC-RPO Processor: precedence: f5_AC > f3_AC status: problem: Qed