TRS:
 { f(0()) -> 1(),
  f(s(x)) -> g(f(x)),
     g(x) -> +(x, s(x)),
  f(s(x)) -> +(f(x), s(f(x)))}
 MPO:
  Prec:
   f > 1, 
   f > g, 
   f > s, 
   f > +, 
   g > +, 
   g > s
   empty
  Strict:
   {}
   Weak:
    {}
  Qed