Nuprl Lemma : es-fset-loc-iff

es:EO. ∀s:fset(E). ∀i:Id.  (i ∈ locs(s) ⇐⇒ ∃e:E. ((loc(e) i ∈ Id) ∧ e ∈ s))


Proof




Definitions occuring in Statement :  es-fset-loc: i ∈ locs(s) es-eq: es-eq(es) es-loc: loc(e) es-E: E event_ordering: EO Id: Id fset-member: a ∈ s fset: fset(T) all: x:A. B[x] exists: x:A. B[x] iff: ⇐⇒ Q and: P ∧ Q equal: t ∈ T
Lemmas :  es-fset-at-property es-fset-at_wf list_wf not_wf assert_wf null_wf3 subtype_rel_list top_wf exists_wf es-loc_wf fset-member_wf es-eq_wf all_wf iff_wf l_member_wf no_repeats_wf sorted-by_wf es-le_wf Id_wf fset_wf es-E_wf event_ordering_wf list-cases product_subtype_list null_nil_lemma cons_member btrue_wf member-implies-null-eq-bfalse btrue_neq_bfalse null_cons_lemma false_wf
\mforall{}es:EO.  \mforall{}s:fset(E).  \mforall{}i:Id.    (i  \mmember{}  locs(s)  \mLeftarrow{}{}\mRightarrow{}  \mexists{}e:E.  ((loc(e)  =  i)  \mwedge{}  e  \mmember{}  s))



Date html generated: 2015_07_17-AM-09_01_05
Last ObjectModification: 2015_01_27-PM-00_55_38

Home Index