---

Step * 1 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)
⊢ ∀a:ℤ × ℤ × Cmd × Id. ∀s:Cmd List × (Id List). ∀e:E.
    (e1 ≤loc e 
    ⇒ (e <loc e2)
    ⇒ a ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
    ⇒ s ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) ni;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;propose;f))\000C(
           e)
    ⇒ (λ2s2.let cmds1,locs1 = s 
             in let cmds2,locs2 = s2 
                in let x,i = a 
                   in let ni',c = x 
                      in (ni = ni' ∈ (ℤ × ℤ)) ⇒ ((i ∈ locs2) ∧ ((¬(i ∈ locs1)) ⇒ (c ∈ cmds2))) 
        (new_23_sig_add_to_quorum(Cmd) ni loc(e) a s)))
BY
{ GenMemoryTrans2⋅⋅ }

1
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. n1 : ℤ@i
15. n2 : ℤ@i
16. s7 : Cmd List@i
17. s8 : Id List@i
18. s5 : Cmd List@i
19. s6 : Id List@i
20. v5 : ℤ@i
21. v6 : ℤ@i
22. v4 : Cmd@i
23. v2 : Id@i
24. (e1 <loc e2)@i
25. <<<v5, v6>, v4>, v2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)@i
26. <s7, s8> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e1)
27. <s5, s6> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e2)
28. a5 : ℤ@i
29. a6 : ℤ@i
30. a4 : Cmd@i
31. a2 : Id@i
32. s3 : Cmd List@i
33. s4 : Id List@i
34. ¬¬(a2 ∈ s4)
35. e : E@i
36. e1 ≤loc e @i
37. (e <loc e2)@i
38. <<<a5, a6>, a4>, a2> ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)@i
39. <s3, s4> ∈ Memory-loc-class(new_23_sig_add_to_quorum(Cmd) <n1, n2>;λloc.{<[], []>};new_23_sig_vote'base(Cmd;notify;p\000Cropose;f))(e)@i
40. n1 = a5 ∈ ℤ
41. n2 = a6 ∈ ℤ
⊢ (a2 ∈ s4)

---

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{}  \mforall{}a:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id.  \mforall{}s:Cmd  List  \mtimes{}  (Id  List).  \mforall{}e:E.
        (e1  \mleq{}loc  e 
        {}\mRightarrow{}  (e  <loc  e2)
        {}\mRightarrow{}  a  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e)
        {}\mRightarrow{}  s  \mmember{}  Memory-loc-class(new\_23\_sig\_add\_to\_quorum(Cmd) 
                                                        ni;\mlambda{}loc.\{<[],  []>\};new\_23\_sig\_vote'base(Cmd;notify;propose;f))(e)
        {}\mRightarrow{}  (\mlambda{}\msubtwo{}s2.let  cmds1,locs1  =  s 
                          in  let  cmds2,locs2  =  s2 
                                in  let  x,i  =  a 
                                      in  let  ni',c  =  x 
                                            in  (ni  =  ni')  {}\mRightarrow{}  ((i  \mmember{}  locs2)  \mwedge{}  ((\mneg{}(i  \mmember{}  locs1))  {}\mRightarrow{}  (c  \mmember{}  cmds2))) 
                (new\_23\_sig\_add\_to\_quorum(Cmd)  ni  loc(e)  a  s)))


By

---

Latex:
GenMemoryTrans2\mcdot{}\mcdot{}

---

Home Index