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

This commit is contained in:
Marco Realacci 2025-05-05 09:02:04 +02:00
parent 6023957b48
commit aeca70e82d
2 changed files with 4 additions and 2 deletions

View file

@ -32,3 +32,6 @@ However, this can never happen, whatever P be;
hence, P |= ☐aFF holds true only if P cannot perform any action a
![](../../Pasted%20image%2020250505085454.png)
Let us now define the set of formulae satisfied by a process as $$L(P) = \{ \phi \in Form:P \models \phi \}$$
To simplify the proof, let us modify the set of formulae