diff --git a/.obsidian/workspace.json b/.obsidian/workspace.json
index f6f0a23..aa2c3f5 100644
--- a/.obsidian/workspace.json
+++ b/.obsidian/workspace.json
@@ -213,6 +213,7 @@
   },
   "active": "cdcc59f1bf6d4ae1",
   "lastOpenFiles": [
+    "Pasted image 20250505083948.png",
     "Concurrent Systems/slides/class 15.pdf",
     "Concurrent Systems/notes/15 - A formal language for LTSs.md",
     "Pasted image 20250505083500.png",
diff --git a/Concurrent Systems/notes/15 - A formal language for LTSs.md b/Concurrent Systems/notes/15 - A formal language for LTSs.md
index b9692fd..151e6d4 100644
--- a/Concurrent Systems/notes/15 - A formal language for LTSs.md	
+++ b/Concurrent Systems/notes/15 - A formal language for LTSs.md	
@@ -11,3 +11,9 @@ These processes are not bisimilar as:
 - so there exists an a after which P1 cannot perform a b. But not for P2
 
 ### Syntax and Satisfiability
+$$\phi := TT | \lnot \phi | \phi \land \phi|◇ a \phi \quad where a \in Action$$
+The language generated by this grammar will be denoted by Form; every element of this set will be called formula
+
+![](../../Pasted%20image%2020250505083948.png)
+
+To simplify the proofs, we consider a more general form of conjunction: $\land_{i \in I, \phi i}$
\ No newline at end of file
diff --git a/Pasted image 20250505083948.png b/Pasted image 20250505083948.png
new file mode 100644
index 0000000..8ab6e7c
Binary files /dev/null and b/Pasted image 20250505083948.png differ