vault backup: 2025-03-31 12:33:39

Concurrent Systems/notes/9 - Consensus.md

@@ -135,7 +135,7 @@ It suffices to prove that ∃ k s.t. `CONS[k].propose(-)` returns a list that co
 
 As shown before, every invocation is executed; we have to show that this cannot happen more than once.
 
-**Lemma 2:** metti nome lemma
+**Lemma 2:** all operations invoked by processes are executed exactly once
 If $p_i$ has inserted ⟨“op(par)”,sn⟩ in `LAST_OP[i]`, it cannot invoke another operation until ⟨“op(par)”,sn⟩ appears in a list chosen by the consensus
 - the sequence number of `LAST_OP[i]` can increase only after ⟨“op(par)”,sn⟩ has been executed