Problem:
 f(0()) -> cons(0(),f(s(0())))
 f(s(0())) -> f(p(s(0())))
 p(s(0())) -> 0()

Proof:
 Unfolding Processor:
  loop length: 3
  terms:
   f(0())
   cons(0(),f(s(0())))
   cons(0(),f(p(s(0()))))
  context: cons(0(),[])
  substitution:
   
  Qed