---

Step * of Lemma new_23_sig_quorum_mem

∀Cmd:ValueAllType. ∀notify,propose:Atom List. ∀f:new_23_sig_headers_type{i:l}(Cmd;notify;propose). ∀es:EO+(Message(f)).
∀e1,e2:E. ∀ni:ℤ × ℤ. ∀s1,s2:Cmd List × (Id List). ∀v:ℤ × ℤ × Cmd × Id.
  ((e1 <loc e2)
  ⇒ v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e1)
  ⇒ s1 ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e1)
  ⇒ s2 ∈ new_23_sig_QuorumState(Cmd;notify;propose;f) ni(e2)
  ⇒ let cmds1,locs1 = s1 
     in let cmds2,locs2 = s2 
        in let x,i = v 
           in let ni',c = x 
              in (ni = ni' ∈ (ℤ × ℤ)) ⇒ ((i ∈ locs2) ∧ ((¬(i ∈ locs1)) ⇒ (c ∈ cmds2))))
BY
{ (GenMemoryTrans1 3 MemoryLemmas⋅⋅ THEN Try (CompleteAuto)) }

1
.....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)))

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

3
.....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-classrel(es;new_23_sig_vote'base(Cmd;notify;propose;f);ℤ × ℤ × Cmd × Id)

4
.....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))

---

Latex:

---

Latex:
\mforall{}Cmd:ValueAllType.  \mforall{}notify,propose:Atom  List.  \mforall{}f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose).
\mforall{}es:EO+(Message(f)).  \mforall{}e1,e2:E.  \mforall{}ni:\mBbbZ{}  \mtimes{}  \mBbbZ{}.  \mforall{}s1,s2:Cmd  List  \mtimes{}  (Id  List).  \mforall{}v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id.
    ((e1  <loc  e2)
    {}\mRightarrow{}  v  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e1)
    {}\mRightarrow{}  s1  \mmember{}  new\_23\_sig\_QuorumState(Cmd;notify;propose;f)  ni(e1)
    {}\mRightarrow{}  s2  \mmember{}  new\_23\_sig\_QuorumState(Cmd;notify;propose;f)  ni(e2)
    {}\mRightarrow{}  let  cmds1,locs1  =  s1 
          in  let  cmds2,locs2  =  s2 
                in  let  x,i  =  v 
                      in  let  ni',c  =  x 
                            in  (ni  =  ni')  {}\mRightarrow{}  ((i  \mmember{}  locs2)  \mwedge{}  ((\mneg{}(i  \mmember{}  locs1))  {}\mRightarrow{}  (c  \mmember{}  cmds2))))


By

---

Latex:
(GenMemoryTrans1  3  MemoryLemmas\mcdot{}\mcdot{}  THEN  Try  (CompleteAuto))

---

Home Index