I have been looking at the Until operator and the release operator and when introduced to the release operator it was suggested that it is equivalent to:
$\phi R \psi \equiv \neg(\neg\phi U \neg \psi)$
But when trying to get from the semantic definition of the Until operator to the semantic definition of the Release operator by negation I get stuck part way. Specifically, I get stuck trying to negate a $\forall j < i$ expression as I will show below.
So the semantic definition of Until:
$\pi \models \phi U \psi \iff \exists i \geq0, \pi[i] \models \psi \land \forall j\leq i-1, \pi[j]\models \phi$
Putting the negations in:
$\pi \models \neg(\neg\phi U \neg\psi) \iff \neg(\exists i \geq0, \pi[i] \models \neg\psi \land \forall j< i, \pi[j]\models \neg\phi)$
$\iff \forall i \geq 0, \neg(\pi[i]\models\neg\psi)\lor \neg(\forall j < i,\pi[j]\models\neg\phi)$
$\iff \forall i \geq 0, (\pi[i]\models\psi)\lor (\exists j < i,\pi[j]\models\phi)$
In words, I am ending up with globally $\psi$ or globally there always exists some predecessor that satisfies $\phi$. Which cannot be correct as $\pi[j]$ is not defined when $i=0$.
The semantic definition for the release operator that I was aiming for is:
$\pi \models \phi R\psi \iff (\exists i\geq 0, \pi[i]\models\phi \land \forall j\leq i, \pi[j]\models\psi)\lor (\forall k \geq 0, \pi[k] \models \psi)$
So I have part of the expression correct ($\forall k \geq 0, \pi[k] \models \psi \equiv \forall i \geq 0, (\pi[i]\models\psi)$), but I am really stumped about how to get the second part or where I went wrong.
Any help enlightening me is greatly appreciated!