YES

Problem:
 f(x,g(x)) -> x
 f(x,h(y)) -> f(h(x),y)

Proof:
 Bounds Processor:
  bound: 0
  enrichment: match
  automaton:
   final states: {7,6,2,1}
   transitions:
    h0(7) -> 6*
    h0(6) -> 6*
    h0(1) -> 6*,2,3
    h0(3) -> 6*,2,3
    f30() -> 7*,2,1
    f0(3,1) -> 2*
    f0(3,7) -> 2*
    f0(6,1) -> 2*
    f0(6,7) -> 2*
    1 -> 2*
    3 -> 2*
  problem:
   
  Qed