TRS:
 {g(s(x)) -> f(x),
   f(0()) -> s(0()),
  f(s(x)) -> s(s(g(x))),
   g(0()) -> 0()}
 POP*:
  Quasi-Precedence:
  g ~ f > s
  empty
  
Normal:
   pi(g) = [1], pi(f) = [1]
  
Safe:
   pi(s) = [1]
  
Predicative System:
   {g(s(;x);) -> f(x;),
      f(0();) -> s(;0()),
    f(s(;x);) -> s(;s(;g(x;))),
      g(0();) -> 0()}
  Qed