Would anyone care to explain how can we deduce the Loop Invariance rule from the Reflexive Transitive Closure rule in PDL:
$$\frac{\psi\rightarrow (\phi\vee [\alpha]\psi)}{\psi\rightarrow [\alpha^*]\phi}$$? to: $$\frac{(\phi\vee\langle\alpha\rangle\psi)\rightarrow\psi}{\langle\alpha^*\rangle\phi\rightarrow\psi}$$
I've already deduced that $$\frac{(\phi\vee\langle\alpha\rangle\psi)\rightarrow\psi}{\langle\alpha^*\rangle\phi\rightarrow\psi}$$ is equivalent to $$ \frac{\psi \rightarrow [\alpha]\psi}{\psi \rightarrow [\alpha^*]\psi} \enspace, $$ if that helps.
Where $\alpha$ is a program, $\phi,\psi$ are formulas and $\langle\alpha\rangle$ is the diamond from PDL.