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 > f5_AC ~ 0 ~ b ~ a
    weight function:
     [0] = 1,
     
     [g](x0) = 2x0 + 2,
     
     [f5_AC](x0, x1) = x0 + x1,
     
     [a] = 1,
     
     [b] = 1
    problem:
     
    Qed