Step
*
of Lemma
pv11_p1_ldr_state_eq
∀[Cmd:ValueAllType]. ∀[f:pv11_p1_headers_type{i:l}(Cmd)]. ∀[es:EO+(Message(f))]. ∀[e:E]. ∀[ldrs_uid:Id ─→ ℤ].
∀[v:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)].
uiff(v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(e);↓if first(e)
then v
= (pv11_p1_init_leader(Cmd) loc(e))
∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
if pred(e) ∈b pv11_p1_propose'base(Cmd;f)
then ∃x:ℤ × Cmd
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v
= (pv11_p1_on_propose(Cmd) loc(e) x s)
∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
if pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
then ∃x:pv11_p1_Ballot_Num()
× ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v
= (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s)
∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
if pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
then ∃x:pv11_p1_Ballot_Num()
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v
= (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) x s)
∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
else v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
fi )
BY
{ (StartEmlProof
THEN UnfoldAtAddr [1;3] 0
THEN (RWO "memory-class3-classrel" 0 THENA Auto)
THEN Fold `pv11_p1_LeaderState` 0
THEN Repeat (AutoSplit)
THEN D 0
THEN Auto
THEN ExRepD) }
1
1. Cmd : {T:Type| valueall-type(T)}
2. f : pv11_p1_headers_type{i:l}(Cmd)
3. (f [decision]) = (ℤ × Cmd) ∈ Type
4. (f [propose]) = (ℤ × Cmd) ∈ Type
5. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
6. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
7. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
8. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
9. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
10. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
11. f ∈ Name ─→ Type
12. es : EO+(Message(f))
13. e : E
14. ¬↑first(e)
15. ldrs_uid : Id ─→ ℤ
16. v : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
17. ↑pred(e) ∈b pv11_p1_propose'base(Cmd;f)
18. b : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
19. b ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
20. (∃a1:ℤ × Cmd
(a1 ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_on_propose(Cmd) loc(e) a1 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a2:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
(a2 ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) a2 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a3:pv11_p1_Ballot_Num()
(a3 ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) a3 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
⊢ ↓∃x:ℤ × Cmd
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v = (pv11_p1_on_propose(Cmd) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
2
1. Cmd : {T:Type| valueall-type(T)}
2. f : pv11_p1_headers_type{i:l}(Cmd)
3. (f [decision]) = (ℤ × Cmd) ∈ Type
4. (f [propose]) = (ℤ × Cmd) ∈ Type
5. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
6. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
7. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
8. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
9. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
10. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
11. f ∈ Name ─→ Type
12. es : EO+(Message(f))
13. e : E
14. ¬↑pred(e) ∈b pv11_p1_propose'base(Cmd;f)
15. ¬↑first(e)
16. ldrs_uid : Id ─→ ℤ
17. v : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
18. ↑pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
19. b : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
20. b ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
21. (∃a1:ℤ × Cmd
(a1 ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_on_propose(Cmd) loc(e) a1 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a2:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
(a2 ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) a2 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a3:pv11_p1_Ballot_Num()
(a3 ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) a3 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
⊢ ↓∃x:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
3
1. Cmd : {T:Type| valueall-type(T)}
2. f : pv11_p1_headers_type{i:l}(Cmd)
3. (f [decision]) = (ℤ × Cmd) ∈ Type
4. (f [propose]) = (ℤ × Cmd) ∈ Type
5. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
6. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
7. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
8. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
9. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
10. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
11. f ∈ Name ─→ Type
12. es : EO+(Message(f))
13. e : E
14. ¬↑pred(e) ∈b pv11_p1_propose'base(Cmd;f)
15. ¬↑first(e)
16. ldrs_uid : Id ─→ ℤ
17. v : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
18. ↑pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
19. x : pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
20. s : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
21. x ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
22. s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
23. v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
⊢ ↓∃b:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(b ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ ((∃a1:ℤ × Cmd
(a1 ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_on_propose(Cmd) loc(e) a1 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a2:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
(a2 ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) a2 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a3:pv11_p1_Ballot_Num()
(a3 ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) a3 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))))
4
1. Cmd : {T:Type| valueall-type(T)}
2. f : pv11_p1_headers_type{i:l}(Cmd)
3. (f [decision]) = (ℤ × Cmd) ∈ Type
4. (f [propose]) = (ℤ × Cmd) ∈ Type
5. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
6. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
7. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
8. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
9. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
10. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
11. f ∈ Name ─→ Type
12. es : EO+(Message(f))
13. e : E
14. ¬↑pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
15. ¬↑pred(e) ∈b pv11_p1_propose'base(Cmd;f)
16. ¬↑first(e)
17. ldrs_uid : Id ─→ ℤ
18. v : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
19. ↑pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
20. b : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
21. b ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
22. (∃a1:ℤ × Cmd
(a1 ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_on_propose(Cmd) loc(e) a1 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a2:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
(a2 ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) a2 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a3:pv11_p1_Ballot_Num()
(a3 ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) a3 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
⊢ ↓∃x:pv11_p1_Ballot_Num()
∃s:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(x ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
∧ s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))))
5
1. Cmd : {T:Type| valueall-type(T)}
2. f : pv11_p1_headers_type{i:l}(Cmd)
3. (f [decision]) = (ℤ × Cmd) ∈ Type
4. (f [propose]) = (ℤ × Cmd) ∈ Type
5. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
6. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
7. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
8. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
9. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
10. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
11. f ∈ Name ─→ Type
12. es : EO+(Message(f))
13. e : E
14. ¬↑pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
15. ¬↑pred(e) ∈b pv11_p1_propose'base(Cmd;f)
16. ¬↑first(e)
17. ldrs_uid : Id ─→ ℤ
18. v : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
19. ↑pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
20. x : pv11_p1_Ballot_Num()
21. s : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
22. x ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
23. s ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
24. v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) x s) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
⊢ ↓∃b:pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
(b ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
∧ ((∃a1:ℤ × Cmd
(a1 ∈ pv11_p1_propose'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_on_propose(Cmd) loc(e) a1 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a2:pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)
(a2 ∈ pv11_p1_adopted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_adopted(Cmd;ldrs_uid) loc(e) a2 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))
∨ (∃a3:pv11_p1_Ballot_Num()
(a3 ∈ pv11_p1_preempted'base(Cmd;f)(pred(e))
∧ (v = (pv11_p1_when_preempted(Cmd;ldrs_uid) loc(e) a3 b) ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)))))))
6
1. Cmd : {T:Type| valueall-type(T)}
2. f : pv11_p1_headers_type{i:l}(Cmd)
3. (f [decision]) = (ℤ × Cmd) ∈ Type
4. (f [propose]) = (ℤ × Cmd) ∈ Type
5. (f ``pv11_p1 adopted``) = (pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List)) ∈ Type
6. (f ``pv11_p1 preempted``) = pv11_p1_Ballot_Num() ∈ Type
7. (f ``pv11_p1 p2b``) = (Id × pv11_p1_Ballot_Num() × ℤ × pv11_p1_Ballot_Num()) ∈ Type
8. (f ``pv11_p1 p2a``) = (Id × pv11_p1_Ballot_Num() × ℤ × Cmd) ∈ Type
9. (f ``pv11_p1 p1b``)
= (Id × pv11_p1_Ballot_Num() × pv11_p1_Ballot_Num() × ((pv11_p1_Ballot_Num() × ℤ × Cmd) List))
∈ Type
10. (f ``pv11_p1 p1a``) = (Id × pv11_p1_Ballot_Num()) ∈ Type
11. f ∈ Name ─→ Type
12. es : EO+(Message(f))
13. e : E
14. ¬↑pred(e) ∈b pv11_p1_preempted'base(Cmd;f)
15. ¬↑pred(e) ∈b pv11_p1_adopted'base(Cmd;f)
16. ¬↑pred(e) ∈b pv11_p1_propose'base(Cmd;f)
17. ¬↑first(e)
18. ldrs_uid : Id ─→ ℤ
19. v : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
20. b : pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List)
21. b ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
22. v = b ∈ (pv11_p1_Ballot_Num() × 𝔹 × ((ℤ × Cmd) List))
⊢ ↓v ∈ pv11_p1_LeaderState(Cmd;ldrs_uid;f)(pred(e))
Latex:
Latex:
\mforall{}[Cmd:ValueAllType]. \mforall{}[f:pv11\_p1\_headers\_type\{i:l\}(Cmd)]. \mforall{}[es:EO+(Message(f))]. \mforall{}[e:E].
\mforall{}[ldrs$_{uid}$:Id {}\mrightarrow{} \mBbbZ{}]. \mforall{}[v:pv11\_p1\_Ballot\_Num() \mtimes{} \mBbbB{} \mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List)].
uiff(v \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_{uid}$;f)(e);\mdownarrow{}if first(e)
then v = (pv11\_p1\_init\_leader(Cmd) loc(e))
if pred(e) \mmember{}\msubb{} pv11\_p1\_propose'base(Cmd;f)
then \mexists{}x:\mBbbZ{} \mtimes{} Cmd
\mexists{}s:pv11\_p1\_Ballot\_Num()
\mtimes{} \mBbbB{}
\mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List)
(x \mmember{} pv11\_p1\_propose'base(Cmd;f)(pred(e))
\mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$\mbackslash{}f\000Cf5f{uid}$;f)(
pred(e))
\mwedge{} (v
= (pv11\_p1\_on\_propose(Cmd) loc(e) x
s)))
if pred(e) \mmember{}\msubb{} pv11\_p1\_adopted'base(Cmd;f)
then \mexists{}x:pv11\_p1\_Ballot\_Num()
\mtimes{} ((pv11\_p1\_Ballot\_Num()
\mtimes{} \mBbbZ{}
\mtimes{} Cmd) List)
\mexists{}s:pv11\_p1\_Ballot\_Num()
\mtimes{} \mBbbB{}
\mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List)
(x \mmember{} pv11\_p1\_adopted'base(Cmd;f)(pred(e))
\mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$\mbackslash{}f\000Cf5f{uid}$;f)(
pred(e))
\mwedge{} (v
= (pv11\_p1\_when\_adopted(Cmd;ldrs$\mbackslash{}f\000Cf5f{uid}$)
loc(e)
x
s)))
if pred(e) \mmember{}\msubb{} pv11\_p1\_preempted'base(Cmd;f)
then \mexists{}x:pv11\_p1\_Ballot\_Num()
\mexists{}s:pv11\_p1\_Ballot\_Num()
\mtimes{} \mBbbB{}
\mtimes{} ((\mBbbZ{} \mtimes{} Cmd) List)
(x \mmember{} pv11\_p1\_preempted'base(Cmd;f)(
pred(e))
\mwedge{} s \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$\mbackslash{}f\000Cf5f{uid}$;f)(
pred(e))
\mwedge{} (v
= (pv11\_p1\_when\_preempted(Cmd;ldrs$\000C_{uid}$)
loc(e)
x
s)))
else v \mmember{} pv11\_p1\_LeaderState(Cmd;ldrs$_\mbackslash{}ff\000C7buid}$;f)(
pred(e))
fi )
By
Latex:
(StartEmlProof
THEN UnfoldAtAddr [1;3] 0
THEN (RWO "memory-class3-classrel" 0 THENA Auto)
THEN Fold `pv11\_p1\_LeaderState` 0
THEN Repeat (AutoSplit)
THEN D 0
THEN Auto
THEN ExRepD)
Home
Index