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