YES
Time: 0.000760
TRS:
 {f(x, g x) -> x,
  f(x, h y) -> f(h x, y)}
 RUF:
  Strict:
   {f(x, h y) -> f(h x, y)}
  Weak:
   {}
  BOUND:
   Bound: match(-raise)-bounded by 1
   Automaton:
    {   h_1(2) -> 2*
        h_1(1) -> 2*
        h_0(1) -> 1*
     f_1(2, 1) -> 1*
     f_0(1, 1) -> 1*}
   Strict:
    {}
   Qed