YES Problem: +(a(),x) -> a() +(b(),g(a())) -> a() +(0(),x) -> x +(x,+(y,z)) -> +(+(x,y),z) +(+(x,y),z) -> +(x,+(y,z)) +(x,y) -> +(y,x) Proof: Church Rosser Transformation Processor (ac): f5_AC(a(),x) -> a() f5_AC(b(),g(a())) -> a() f5_AC(0(),x) -> x AC critical peaks: joinable AC-KBO Processor: precedence: g > 0 > f5_AC > b > a weight function: w0 = 1 w(0) = w(g) = 4 w(a) = 2 w(b) = 1 w(f5_AC) = 0 problem: Qed