### Nuprl Lemma : es-fset-last_wf

`∀[es:EO]. ∀[s:fset(E)]. ∀[i:Id].`
`  s(i) ∈ {e:E| (loc(e) = i ∈ Id) ∧ e ∈ s ∧ (∀e':E. (e' ∈ s `` (¬(e <loc e'))))}  supposing i ∈ locs(s)`

Proof

Definitions occuring in Statement :  es-fset-last: `s(i)` es-fset-loc: `i ∈ locs(s)` es-locl: `(e <loc e')` es-eq: `es-eq(es)` es-loc: `loc(e)` es-E: `E` event_ordering: `EO` Id: `Id` fset-member: `a ∈ s` fset: `fset(T)` uimplies: `b supposing a` uall: `∀[x:A]. B[x]` all: `∀x:A. B[x]` not: `¬A` implies: `P `` Q` and: `P ∧ Q` member: `t ∈ T` set: `{x:A| B[x]} ` equal: `s = t ∈ T`
Lemmas :  last_wf last_member es-locl_wf es-E_wf es-fset-at_wf list_wf l_member_wf sorted-by_wf es-le_wf not_wf assert_wf null_wf3 subtype_rel_list top_wf event_ordering_wf list-cases null_nil_lemma length_of_nil_lemma product_subtype_list null_cons_lemma length_of_cons_lemma subtract_wf length_wf non_neg_length length_wf_nat decidable__equal_int int_seg_wf int_subtype_base subtype_base_sq es-locl_irreflexivity lelt_wf es-locl_transitivity2
\mforall{}[es:EO].  \mforall{}[s:fset(E)].  \mforall{}[i:Id].
s(i)  \mmember{}  \{e:E|  (loc(e)  =  i)  \mwedge{}  e  \mmember{}  s  \mwedge{}  (\mforall{}e':E.  (e'  \mmember{}  s  {}\mRightarrow{}  (\mneg{}(e  <loc  e'))))\}    supposing  i  \mmember{}  locs(s)

Date html generated: 2015_07_17-AM-09_01_14
Last ObjectModification: 2015_07_16-AM-09_51_43

Home Index