# Loop Invariance rule deduction from Reflexive transitive closure rule

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.

• Is this what you are looking for? – Fabio Somenzi Feb 7 '17 at 21:32
• I just noted that you asked the other question as well. The last rule you show is the loop invariance rule and $\psi$ is the invariant, while $\alpha$ is the loop body. – Fabio Somenzi Feb 7 '17 at 21:35
• From the loop invariance rule alone, you cannot derive $\psi \rightarrow \psi$. However, if you assume $\psi \rightarrow \psi$ and $\psi \rightarrow [\alpha]\psi$, then the loop invariance rule allows you to conclude that $\psi \rightarrow [\alpha^*]\phi$. – Fabio Somenzi Feb 8 '17 at 0:46
• Also note that the invariance rule is not equivalent to the dual of the reflexive transitive closure rule. Rather, it's a special case of it. – Fabio Somenzi Feb 8 '17 at 0:48
• You are welcome. Actually, I mistyped in one of the comments above. I meant $\psi \rightarrow \phi$, not the tautologous $\psi \rightarrow \psi$. – Fabio Somenzi Feb 8 '17 at 2:26