The proof system uses a number of the propositional axioms suggested by Rosner and Pnueli but also includes our own axioms and inference rules for the operators and chop-plus.
Instead of ChopPlusEqv one can use