---

Step * 1 2 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
⊢ mapfilter(λe.(snd(fst(msgval(e))));λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;r);L)
  ∈ Cmd List
BY
{ (MemCD
   THEN Reduce 0
   THEN MemCD
   THEN Try ((D -1 THEN FLemma `new_23_sig_vote_with_ballot_first-assert-type` [-1] THEN Auto))
   THEN Auto) }

1
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

---

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
\mvdash{}  mapfilter(\mlambda{}e.(snd(fst(msgval(e))));
                        \mlambda{}e'.new\_23\_sig\_vote\_with\_ballot\_first(Cmd;notify;propose;f;es.e;e';n;r);
                        L)  \mmember{}  Cmd  List


By

---

Latex:
(MemCD
  THEN  Reduce  0
  THEN  MemCD
  THEN  Try  ((D  -1  THEN  FLemma  `new\_23\_sig\_vote\_with\_ballot\_first-assert-type`  [-1]  THEN  Auto))
  THEN  Auto)

---

Home Index