YES

Problem:
 g(0(),f(x,x)) -> x
 g(x,s(y)) -> g(f(x,y),0())
 g(s(x),y) -> g(f(x,y),0())
 g(f(x,y),0()) -> f(g(x,0()),g(y,0()))

Proof:
 Bounds Processor:
  bound: 1
  enrichment: match
  automaton:
   final states: {12,10,5,2,1}
   transitions:
    f40() -> 1*
    g0(3,3) -> 9*
    g0(4,3) -> 10*,7,6,2
    g0(1,3) -> 11*,7,6
    f0(10,9) -> 11*
    f0(10,11) -> 12*,5
    f0(11,6) -> 12*,5
    f0(6,6) -> 10*,7,6,2
    f0(11,10) -> 12*,5
    f0(6,10) -> 10*
    f0(11,12) -> 5,12*
    f0(6,12) -> 10*
    f0(12,9) -> 11*
    f0(12,11) -> 5,12*
    f0(7,11) -> 5*
    f0(10,6) -> 12*,5
    f0(10,10) -> 12*,5
    f0(10,12) -> 5,12*
    f0(1,1) -> 4*
    f0(1,3) -> 1*
    f0(11,9) -> 11*
    f0(6,9) -> 11*,6,7
    f0(11,11) -> 12*,5
    f0(6,11) -> 10*
    f0(12,6) -> 5,12*
    f0(7,6) -> 5*
    f0(12,10) -> 5,12*
    f0(7,10) -> 5*
    f0(12,12) -> 5,12*
    f0(7,12) -> 5*
    00() -> 3*
    f1(11,9) -> 11*
    f1(11,11) -> 10,5,12*
    g1(3,3) -> 9*
    g1(1,3) -> 6,7,11*
    01() -> 3*
    2 -> 6,7
  problem:
   
  Qed