 At the end of the process, one can prove not only the semantical equivalence of validities in PDL with consequences from \(\Delta _{\PDL}\) of the universal closure of their translations, but also that the dynamic calculus proves as theorems all the formulas whose translations are theorems of our theory \(\Delta _{\PDL}\).