vault backup: 2025-03-31 16:26:18
This commit is contained in:
parent
597b861a6e
commit
7104a7cca2
1 changed files with 1 additions and 1 deletions
|
@ -145,7 +145,7 @@ Every $p_{j}$ that participates in the k-th consensus increases `last_sn_j[i]` b
|
|||
- if `π2(LAST_OP[i])` is not changed, then the guard of the IF is false and ⟨“op(par)”,i⟩ is not appended in `invoc_j`
|
||||
- otherwise, we have a new invocation from $p_{i}$ (but this can only happen after that ⟨“op(par)”,sn⟩ has been executed)
|
||||
|
||||
**Lemma 3:** the local copies $s_{i}$ if all correct processes behave the same and comply with the sequential specification of Z
|
||||
**Lemma 3:** the local copies $s_{i}$ of all correct processes behave the same and comply with the sequential specification of Z.
|
||||
|
||||
*Proof:*
|
||||
- the processes use CONS in the same order `(CONS[1], CONS[2], …)`
|
||||
|
|
Loading…
Add table
Add a link
Reference in a new issue