vault backup: 2025-05-05 09:27:04

Concurrent Systems/notes/15 - A formal language for LTSs.md

@@ -50,7 +50,10 @@ To simplify the proof, let us modify the set of formulae by allowing conjunction
 
 Let $(P, Q) \in R$ and $P \xrightarrow{a} P'$. Let's consider $$\phi \triangleq \phi' \space where \space \phi'\triangleq \bigwedge_{\phi'' \in L(P')}\phi''$$
 By construction, $P \models \phi$, hence, $Q \models \phi$, because $L(Q) = L(P)$; then, $\exists Q' : Q \xrightarrow{a} Q'$ such that $Q'\models \phi'$.
+We proven that the formulas satisfied by P' are all satisfied by Q'
 
 Hence, $\forall \phi'' \in L(P').\phi'' \in L(Q'), \space i.e. \space L(P') \subseteq L(Q')$
 
-By contradiction, let us assume that the inclusion is a proper, i.e. $L(P') \subset L(Q')$.
+By contradiction, let us assume that the inclusion is a proper, i.e. $L(P') \subset L(Q')$. Thus, $\exists \hat{\phi}:\hat{\phi}\in L(Q') \land \hat{\phi} \not \in L(P')$.
+
+Then, $\lnot \hat{\phi} \in L(P')$ and this would imply that $\lnot \hat{\phi} \in L(Q')$. This is a contradiction because $L(Q')$ cannot contain a formula and its negation.