---

Step * 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 : ℤ
⊢ mapfilter(λe.(snd(fst(msgval(e))));λe'.new_23_sig_vote_with_ballot_first(Cmd;notify;propose;f;es.e;e';n;r);[e, e'])
  ∈ Cmd List
BY
{ (GenConcl ⌜[e, e'] = L ∈ ({x:E| e ≤loc x }  List)⌝⋅ THENA Auto) }

1
.....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 : ℤ
⊢ [e, e'] ∈ {x:E| e ≤loc x }  List

2
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

---

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{}
\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);
                        [e,  e'])  \mmember{}  Cmd  List


By

---

Latex:
(GenConcl  \mkleeneopen{}[e,  e']  =  L\mkleeneclose{}\mcdot{}  THENA  Auto)

---

Home Index