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