---

Step * 1 1 of Lemma new_23_sig_commands_from_votes_wf

.....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
BY
{ (BLemma `list-set-type2` 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 : ℤ
⊢ (∀x∈[e, e'].e ≤loc x )

---

Latex:

---

Latex:
.....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  \mleq{}loc  e'  \} 
8.  n  :  \mBbbZ{}
9.  r  :  \mBbbZ{}
\mvdash{}  [e,  e']  \mmember{}  \{x:E|  e  \mleq{}loc  x  \}    List


By

---

Latex:
(BLemma  `list-set-type2`  THEN  Auto)

---

Home Index