diff --git a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md
index 1df2007..a4364c4 100644
--- a/Concurrent Systems/notes/11 - LTSs and Bisimulation.md	
+++ b/Concurrent Systems/notes/11 - LTSs and Bisimulation.md	
@@ -99,7 +99,7 @@ So, (p', q') ∈ ∼
 **Theorem:** For every bisimulation S, it holds that S ⊆ ∼.
 *Proof:*
 Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q); thus, (p, q) ∈ ∼.
-## La parte difficile
+## A syntax for LTSs
 
 ![](../../Pasted%20image%2020250414091521.png)
 
@@ -107,7 +107,7 @@ Let (p,q) ∈ S. Then, there exists a bisimulation that contains the pair (p, q)
 ![](../../Pasted%20image%2020250414091528.png)
 
 The only ingredients we used to write down an LTS are:
-- sequential compsition (of an action and a process)
+- sequential composition (of an action and a process)
 - non-deterministic choice (between a finite set of prefixed processes)
 - recursion