vault backup: 2025-03-03 19:31:59

Concurrent Systems/notes/Lezione1.md

@@ -226,5 +226,8 @@ Reverse induction on ℓ
 Base ($ℓ=n-1$): trivial
 
 Induction (true for ℓ+1, to be proved for ℓ):
-- Assume a $p_x$ blocked at level ℓ $\to \exists k\neq x, F[k]\geqℓ+1 \land A\_Y[ℓ+1]=x$
-- 
+- Assume a $p_x$ blocked at level ℓ (aka blocked in its ℓ+1-th wait) $\to \exists k\neq x, F[k]\geqℓ+1 \land A\_Y[ℓ+1]=x$
+
+- If some $p_{y}$ will eventually set $A\_Y[ℓ+1]$ to $y$, then $p_x$ will eventually exit from its wait and pass to level ℓ+1
+
+- Otherwise, let $G = {$