A complete equational axiomatization for BPA-δε with prefix iteration

Prex iteration x is added to Basic Process Algebra with deadlock and \nempty process. We present a nite equational axiomatization for this process \nalgebra, and we prove that this axiomatization is complete with respect to \nstrong bisimulation equivalence. This result is a mild generalization of a similar \nresult in the setting of basic CCS in Fokkink (1994b). \nTo obtain this completeness result, we set up a rewrite system, based on \nthe axioms. In order to prove that this rewrite system is terminating modulo \nAC of the +, we generalize a termination theorem from Zantema and Geser \n(1994) to the setting of rewriting modulo equations. Finally, we show that \nbisimilar normal forms are syntactically equal modulo AC of the +.