Abstract:Axioms for removing unguarded recursions in the π calculus are proposed. It is shown that these two axioms are sound with respect to bisimulation equivalence, and are sufficient to reduce any unguarded recursively defined processes into guarded forms. Hence, by adding these axioms to the proof systems for guarded regular π calculus, complete proof systems for the whole regular π calculus are obtained.