---

Step * 4 of Lemma new_23_sig_quorum_mem

.....antecedent..... 
1. Cmd : {T:Type| valueall-type(T)} @i'
2. notify : Atom List@i
3. propose : Atom List@i
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)@i'
5. (f propose) = (ℤ × Cmd) ∈ Type
6. (f notify) = (ℤ × Cmd) ∈ Type
7. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
8. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
9. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
10. f ∈ Name ─→ Type
11. es : EO+(Message(f))@i'
12. e1 : E@i
13. e2 : E@i
14. ni : ℤ × ℤ@i
15. s1 : Cmd List × (Id List)@i
16. s2 : Cmd List × (Id List)@i
17. v : ℤ × ℤ × Cmd × Id@i
18. (e1 <loc e2)@i
19. v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)@i
20. s1 ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))(
         e1)
21. s2 ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))(
         e2)
⊢ single-valued-bag((λloc.{<[], []>}) loc(e1);Cmd List × (Id List))
BY
{ GenMemoryTrans2⋅⋅ }

---

Latex:

---

Latex:
.....antecedent..... 
1.  Cmd  :  \{T:Type|  valueall-type(T)\}  @i'
2.  notify  :  Atom  List@i
3.  propose  :  Atom  List@i
4.  f  :  new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)@i'
5.  (f  propose)  =  (\mBbbZ{}  \mtimes{}  Cmd)
6.  (f  notify)  =  (\mBbbZ{}  \mtimes{}  Cmd)
7.  (f  ``new\_23\_sig  decided``)  =  (\mBbbZ{}  \mtimes{}  Cmd)
8.  (f  ``new\_23\_sig  retry``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd)
9.  (f  ``new\_23\_sig  vote``)  =  (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
10.  f  \mmember{}  Name  {}\mrightarrow{}  Type
11.  es  :  EO+(Message(f))@i'
12.  e1  :  E@i
13.  e2  :  E@i
14.  ni  :  \mBbbZ{}  \mtimes{}  \mBbbZ{}@i
15.  s1  :  Cmd  List  \mtimes{}  (Id  List)@i
16.  s2  :  Cmd  List  \mtimes{}  (Id  List)@i
17.  v  :  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id@i
18.  (e1  <loc  e2)@i
19.  v  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e1)@i
20.  s1  \mmember{}  Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd) 
                                                    ni;\mlambda{}loc.\{<[],  []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e1)
21.  s2  \mmember{}  Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd) 
                                                    ni;\mlambda{}loc.\{<[],  []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e2)
\mvdash{}  single-valued-bag((\mlambda{}loc.\{<[],  []>\})  loc(e1);Cmd  List  \mtimes{}  (Id  List))


By

---

Latex:
GenMemoryTrans2\mcdot{}\mcdot{}

---

Home Index