---

Step * 1 2 1 of Lemma new_23_sig_commands_from_votes_wf


1. Cmd : ValueAllType
2. propose : Atom List
3. notify : Atom List
4. f : new_23_sig_headers_type{i:l}(Cmd;notify;propose)
5. es : EO+(Message(f))
6. e : E
7. e' : {e':E| e ≤loc e' } 
8. n : ℤ
9. r : ℤ
10. L : {x:E| e ≤loc x }  List@i
11. [e, e'] = L ∈ ({x:E| e ≤loc x }  List)@i
12. e1 : {x:E| e ≤loc x } @i
13. ↑new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e1;n;r)@i
14. has-es-info-type(es.e;e1;f;ℤ × ℤ × Cmd × Id)
⊢ snd(fst(msgval(e1))) ∈ Cmd
BY
{ (RWO "eo-forward-has-es-info-type" (-1) THEN Auto) }

---

Latex:

---

Latex:

1.  Cmd  :  ValueAllType
2.  propose  :  Atom  List
3.  notify  :  Atom  List
4.  f  :  new\_23\_sig\_headers\_type\{i:l\}(Cmd;notify;propose)
5.  es  :  EO+(Message(f))
6.  e  :  E
7.  e'  :  \{e':E|  e  \mleq{}loc  e'  \} 
8.  n  :  \mBbbZ{}
9.  r  :  \mBbbZ{}
10.  L  :  \{x:E|  e  \mleq{}loc  x  \}    List@i
11.  [e,  e']  =  L@i
12.  e1  :  \{x:E|  e  \mleq{}loc  x  \}  @i
13.  \muparrow{}new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.e;e1;n;r)@i
14.  has-es-info-type(es.e;e1;f;\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id)
\mvdash{}  snd(fst(msgval(e1)))  \mmember{}  Cmd


By

---

Latex:
(RWO  "eo-forward-has-es-info-type"  (-1)  THEN  Auto)

---

Home Index