TRS:
 { f(t(), x, y) -> f(g(x, y), x, s(y)),
   g(s(x), 0()) -> t(),
  g(s(x), s(y)) -> g(x, y)}
 Fail