(* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
\lambda n, p, g. (iter_p_gen n p nat g O plus).
(* sigma_p on nautral numbers is a specialization of sigma_p_gen *)
definition sigma_p: nat \to (nat \to bool) \to (nat \to nat) \to nat \def
\lambda n, p, g. (iter_p_gen n p nat g O plus).