YES

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

Proof:
 Bounds Processor:
  bound: 3
  enrichment: roof
  automaton:
   final states: {7,6,5}
   transitions:
    f1(6,6,6) -> 5*
    f1(7,7,7) -> 5*
    f1(5,5,5) -> 5*
    g1(6,5,7) -> 5*
    g1(6,7,7) -> 5*
    g1(7,5,5) -> 5*
    g1(5,5,6) -> 5*
    g1(7,7,5) -> 5*
    g1(5,7,6) -> 5*
    g1(7,6,7) -> 5*
    g1(6,6,6) -> 5*
    g1(7,5,6) -> 5*
    g1(7,7,6) -> 5*
    g1(5,6,5) -> 5*
    g1(5,5,7) -> 5*
    g1(5,7,7) -> 5*
    g1(6,5,5) -> 5*
    g1(6,7,5) -> 5*
    g1(6,6,7) -> 5*
    g1(7,6,5) -> 5*
    g1(5,6,6) -> 5*
    g1(7,5,7) -> 5*
    g1(7,7,7) -> 5*
    g1(6,5,6) -> 5*
    g1(6,7,6) -> 5*
    g1(7,6,6) -> 5*
    g1(5,5,5) -> 5*
    g1(5,7,5) -> 5*
    g1(5,6,7) -> 5*
    g1(6,6,5) -> 5*
    f2(6,6,6) -> 5*
    f2(7,7,7) -> 5*
    f2(5,5,5) -> 5*
    g2(6,6,6) -> 5*
    g2(7,7,7) -> 5*
    g2(5,5,5) -> 5*
    g3(6,6,6) -> 5*
    g3(7,7,7) -> 5*
    g3(5,5,5) -> 5*
    f0(6,5,7) -> 5*
    f0(6,7,7) -> 5*
    f0(7,5,5) -> 5*
    f0(5,5,6) -> 5*
    f0(7,7,5) -> 5*
    f0(5,7,6) -> 5*
    f0(7,6,7) -> 5*
    f0(6,6,6) -> 5*
    f0(7,5,6) -> 5*
    f0(7,7,6) -> 5*
    f0(5,6,5) -> 5*
    f0(5,5,7) -> 5*
    f0(5,7,7) -> 5*
    f0(6,5,5) -> 5*
    f0(6,7,5) -> 5*
    f0(6,6,7) -> 5*
    f0(7,6,5) -> 5*
    f0(5,6,6) -> 5*
    f0(7,5,7) -> 5*
    f0(7,7,7) -> 5*
    f0(6,5,6) -> 5*
    f0(6,7,6) -> 5*
    f0(7,6,6) -> 5*
    f0(5,5,5) -> 5*
    f0(5,7,5) -> 5*
    f0(5,6,7) -> 5*
    f0(6,6,5) -> 5*
    g0(6,5,7) -> 5*
    g0(6,7,7) -> 5*
    g0(7,5,5) -> 5*
    g0(5,5,6) -> 5*
    g0(7,7,5) -> 5*
    g0(5,7,6) -> 5*
    g0(7,6,7) -> 5*
    g0(6,6,6) -> 5*
    g0(7,5,6) -> 5*
    g0(7,7,6) -> 5*
    g0(5,6,5) -> 5*
    g0(5,5,7) -> 5*
    g0(5,7,7) -> 5*
    g0(6,5,5) -> 5*
    g0(6,7,5) -> 5*
    g0(6,6,7) -> 5*
    g0(7,6,5) -> 5*
    g0(5,6,6) -> 5*
    g0(7,5,7) -> 5*
    g0(7,7,7) -> 5*
    g0(6,5,6) -> 5*
    g0(6,7,6) -> 5*
    g0(7,6,6) -> 5*
    g0(5,5,5) -> 5*
    g0(5,7,5) -> 5*
    g0(5,6,7) -> 5*
    g0(6,6,5) -> 5*
    00() -> 6*
    10() -> 7*
  problem:
   
  Qed