The axiom schema [A?]B ↔ (A → B) seems to indicate that for every formula C, there exists an equivalent test-free formula C′—i.e., there is a test-free formula C′ such that  ⊨ C ↔ C′. It is interesting to observe that this assertion is untrue. Let PDL0 be the restriction of PDL to test-free regular programs, i.e. programs which do not contain tests. Berman and Paterson [1981] considered the PDL formula &lt;(p?;π)*;¬p?;π;p?&gt;1, which is