---

Step * 1 1 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 : ℤ
⊢ (∀x∈[e, e'].e ≤loc x )
BY
{ (BLemma  `l_all_iff` 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. x : E@i
11. (x ∈ [e, e'])@i
⊢ e ≤loc x 

---

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{}  (\mforall{}x\mmember{}[e,  e'].e  \mleq{}loc  x  )


By

---

Latex:
(BLemma    `l\_all\_iff`  THEN  Auto)

---

Home Index