{\llbracket {\pi_2} \rrbracket} (f)} {\leq_{\mathsf{proc}}}g$. Also, $M,e,{\min {\llbracket {\pi_2} \rrbracket} (f')} \models \pi_1\pi_2$. Hence $g {\leq_{\mathsf{proc}}}{\min {\llbracket {\pi_2} \rrbracket} (f')}$. Therefore, $g = {\min {\llbracket {\pi_2} \rrbracket} (f')}$.

The proof that ${\max {\llbracket {\pi_1 \pi_2} \rrbracket} (e)} =
  {\max {\llbracket {\pi_2} \rrbracket} ({\max {\llbracket {\pi_1 {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)})}$ is similar.

\(e) at (0,0) ; (f) at (1,1) ; (fp) at (-1,1) ; (gp) at (-1.1,2) ; (g) at (0,2) ; (leproc) at (0,1) [${\leq_{\mathsf{proc}}}$]{}; at (-0.5,1.95) [${\leq_{\mathsf{proc}}}$]{};

\(e) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right\] [$\pi_1$]{} (f) (e) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left\] [$\pi_1$]{} (fp) (f) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[right\] [$\pi_2$]{} (g) (fp) edge\[decorate,decoration=[snake,post length=0.5mm,amplitude=0.4mm]{},-&gt;=2\] node\[left\] [$\pi_2$]{} (gp);

We turn now to the proof of Lemma \[lem:monotone\]. Actually, we prove a slightly stronger statement. We show by induction on $\pi$ that, for all ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ event formulas $\psi$, the path formula $\pi \cdot {\{\psi\}?}$ is monotone.

Let $e,f$ be events such that $e{\leq_{\mathsf{proc}}}f$, $M,e\models\pi\cdot{\{\psi\}?}$ and $M,f\models\pi\cdot{\{\psi\}?}$. Let $e' = {\min {\llbracket {\pi\cdot{\{\psi\}?}} \rrbracket} (e)}$ and $f' = {\min {\llbracket {\pi\cdot{\{\psi\}?}} \rrbracket} (f)}$. We show that $e'{\leq_{\mathsf{proc}}}f'$. The proof that ${\max {\llbracket {\pi\cdot{\{\psi\}?}} \rrbracket} (e)}{\leq_{\mathsf{proc}}}{\max {\llbracket {\pi\cdot{\{\psi\}?}} \rrbracket} (e)}$ is similar. We start with the base cases.

If $\pi = {\{\varphi\}?}$, we have $e' = e {\leq_{\mathsf{proc}}}f 