such that $M,e\models{\mathop{\langle \pi_1 \cdot \pi_2 \rangle}}$, we have $$\begin{aligned}
    {\min {\llbracket {\pi_1 \cdot \pi_2} \rrbracket} (e)} & = {\min {\llbracket {\pi_2} \rrbracket} ({\min {\llbracket {\pi_1 \cdot {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)})} \text{ and }
      \\
    {\max {\llbracket {\pi_1 \cdot \pi_2} \rrbracket} (e)} & = {\max {\llbracket {\pi_2} \rrbracket} ({\max {\llbracket {\pi_1 \cdot {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)})} \, .
  \end{aligned}$$

\[lem:monotone\] All ${{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ path formulas are monotone.

We first show that Lemma \[lem:min-conc\] holds when $\pi_2$ is monotone. We then use this to prove by induction that all ${\textup{PDL}_{\mathsf{sf}}}$ formulas are monotone (Lemma \[lem:monotone\]). Therefore, we deduce that Lemma \[lem:min-conc\] is always true.

Let $\pi_1,\pi_2 \in {{{\textup{PDL}_{\mathsf{sf}}}[{\mathsf{Loop}}]}}$ be path formulas such that $\pi_2$ is monotone. Let $M$ be an MSCs and $e$ be some event in $M$ such that $M,e\models{\mathop{\langle \pi_1\pi_2 \rangle}}$. The proof is illustrated in Figure \[fig:min-conc\]. We let $g = {\min {\llbracket {\pi_1 \pi_2} \rrbracket} (e)}$. Since $M,e,g \models \pi_1\pi_2$, there exists $f$ such that $M,e,f \models \pi_1$, and $M,f,g \models \pi_2$. In particular, $M,e,f \models \pi_1 {\{{\mathop{\langle \pi_2 \rangle}}\}?}$, so $f' =
  {\min {\llbracket {\pi_1 {\{{\mathop{\langle \pi_2 \rangle}}\}?}} \rrbracket} (e)}$ is well-defined and $f'
  {\leq_{\mathsf{proc}}}f$. Since $\pi_2$ is monotone, ${\min {\llbracket {\pi_2} \rrbracket} (f')} {\leq_{\mathsf{proc}}}{\min 