---

Step * of Lemma new_23_sig_validity

∀[Cmd:ValueAllType]. ∀[eq:EqDecider(Cmd)]. ∀[reps,clients:bag(Id)]. ∀[coeff:{2...}]. ∀[flrs:ℕ].
∀[propose,notify:Atom List]. ∀[slots:set-sig{i:l}(ℤ)]. ∀[f:new_23_sig_headers_type{i:l}(Cmd;notify;propose)].
∀[es:EO+(Message(f))].
  (new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)
  ⇒ for every p1 in new_23_sig_decided'base(Cmd;notify;propose;f) there is an
     earlier event  with info=m such that
     (msg-header(m) = propose ∈ Name) ∧ (p1 = msg-body(m) ∈ (ℤ × Cmd)))
BY
{ (StartEmlProof
   THEN (Assert ⌈∀e:E
                   ((∀v:ℤ × Cmd
                       (v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
                       ⇒ (↓∃e':E. ((e' < e) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
                   ∧ (∀v:ℤ × ℤ × Cmd × Id
                        (v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
                        ⇒ (↓∃e':E
                              ((e' < e)
                              ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
                   ∧ (∀v:ℤ × ℤ × Cmd
                        (v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)
                        ⇒ (↓∃e':E
                              ((e' < e) ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
                   ∧ (∀e1:E
                        (e1 c≤ e
                        ⇒ (∀n,rnd:ℤ. ∀c:Cmd.
                              ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e1;e)))
                              ⇒ (↓∃e':E. ((e' < e) ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))))))⌉
         ⋅
        THENM (D 0
               THEN Auto
               THEN InstHyp [⌈e⌉] (-4)⋅
               THEN Auto
               THEN FHyp (-4) [-5]
               THEN Auto
               THEN ExRepD
               THEN D 0
               THEN InstConcl [⌈e'⌉]⋅
               THEN Auto
               THEN OnSomeHyp UseClassRel
               THEN Auto)
        )
   ) }

1
.....assertion..... 
1. Cmd : {T:Type| valueall-type(T)} 
2. eq : EqDecider(Cmd)
3. reps : bag(Id)
4. clients : bag(Id)
5. coeff : {2...}
6. flrs : ℕ
7. propose : Atom List
8. notify : Atom List
9. slots : set-sig{i:l}(ℤ)
10. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
11. (f propose) = (ℤ × Cmd) ∈ Type
12. (f notify) = (ℤ × Cmd) ∈ Type
13. (f ``new_23_sig decided``) = (ℤ × Cmd) ∈ Type
14. (f ``new_23_sig retry``) = (ℤ × ℤ × Cmd) ∈ Type
15. (f ``new_23_sig vote``) = (ℤ × ℤ × Cmd × Id) ∈ Type
16. f ∈ Name ─→ Type
17. es : EO+(Message(f))
18. new_23_sig_message-constraint{i:l}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)@i'
⊢ ∀e:E
    ((∀v:ℤ × Cmd
        (v ∈ new_23_sig_decided'base(Cmd;notify;propose;f)(e)
        ⇒ (↓∃e':E. ((e' < e) ∧ v ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
    ∧ (∀v:ℤ × ℤ × Cmd × Id
         (v ∈ new_23_sig_vote'base(Cmd;notify;propose;f)(e)
         ⇒ (↓∃e':E. ((e' < e) ∧ <fst(fst(fst(v))), snd(fst(v))> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
    ∧ (∀v:ℤ × ℤ × Cmd
         (v ∈ new_23_sig_retry'base(Cmd;notify;propose;f)(e)
         ⇒ (↓∃e':E. ((e' < e) ∧ <fst(fst(v)), snd(v)> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e')))))
    ∧ (∀e1:E
         (e1 c≤ e
         ⇒ (∀n,rnd:ℤ. ∀c:Cmd.
               ((c ∈ fst(new_23_sig_QuorumStateFun(Cmd;notify;propose;f;<n, rnd>;es.e1;e)))
               ⇒ (↓∃e':E. ((e' < e) ∧ <n, c> ∈ new_23_sig_propose'base(Cmd;notify;propose;f)(e'))))))))

---

Latex:

---

Latex:
\mforall{}[Cmd:ValueAllType].  \mforall{}[eq:EqDecider(Cmd)].  \mforall{}[reps,clients:bag(Id)].  \mforall{}[coeff:\{2...\}].  \mforall{}[flrs:\mBbbN{}].
\mforall{}[propose,notify:Atom  List].  \mforall{}[slots:set-sig\{i:l\}(\mBbbZ{})].
\mforall{}[f:new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)].  \mforall{}[es:EO+(Message(f))].
    (new\_23\_sig\_message-constraint\{i:l\}(Cmd;clients;eq;coeff;flrs;notify;propose;reps;slots;f)
    {}\mRightarrow{}  for  every  p1  in  new\_23\_sig\_decided'base(Cmd;notify;propose;f)  there  is  an
          earlier  event    with  info=m  such  that
          (msg-header(m)  =  propose)  \mwedge{}  (p1  =  msg-body(m)))


By

---

Latex:
(StartEmlProof
  THEN  (Assert  \mkleeneopen{}\mforall{}e:E
                                  ((\mforall{}v:\mBbbZ{}  \mtimes{}  Cmd
                                          (v  \mmember{}  new\_23\_sig\_decided'base(Cmd;notify;propose;f)(e)
                                          {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                                                      ((e'  <  e)  \mwedge{}  v  \mmember{}  new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')))))
                                  \mwedge{}  (\mforall{}v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id
                                            (v  \mmember{}  new\_23\_sig\_vote'base(Cmd;notify;propose;f)(e)
                                            {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                                                        ((e'  <  e)
                                                        \mwedge{}  <fst(fst(fst(v))),  snd(fst(v))>  \mmember{}
                                                              new\_23\_sig\_propose'base(Cmd;notify;propose;f)(e')))))
                                  \mwedge{}  (\mforall{}v:\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd
                                            (v  \mmember{}  new\_23\_sig\_retry'base(Cmd;notify;propose;f)(e)
                                            {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                                                        ((e'  <  e)
                                                        \mwedge{}  <fst(fst(v)),  snd(v)>  \mmember{}  new\_23\_sig\_propose'base(Cmd;notify;propose;f)(
                                                                                                            e')))))
                                  \mwedge{}  (\mforall{}e1:E
                                            (e1  c\mleq{}  e
                                            {}\mRightarrow{}  (\mforall{}n,rnd:\mBbbZ{}.  \mforall{}c:Cmd.
                                                        ((c  \mmember{}  fst(new\_23\_sig\_QuorumStateFun(Cmd;notify;propose;f;<n,  rnd>es.e1;\000Ce)))
                                                        {}\mRightarrow{}  (\mdownarrow{}\mexists{}e':E
                                                                    ((e'  <  e)
                                                                    \mwedge{}  <n,  c>  \mmember{}  new\_23\_sig\_propose'base(Cmd;notify;propose;f)(
                                                                                          e'))))))))\mkleeneclose{}\mcdot{}
            THENM  (D  0
                          THEN  Auto
                          THEN  InstHyp  [\mkleeneopen{}e\mkleeneclose{}]  (-4)\mcdot{}
                          THEN  Auto
                          THEN  FHyp  (-4)  [-5]
                          THEN  Auto
                          THEN  ExRepD
                          THEN  D  0
                          THEN  InstConcl  [\mkleeneopen{}e'\mkleeneclose{}]\mcdot{}
                          THEN  Auto
                          THEN  OnSomeHyp  UseClassRel
                          THEN  Auto)
            )
  )

---

Home Index