Nuprl Lemma : es-cut-at-property
∀[Info:Type]
∀es:EO+(Info). ∀X:EClass(Top). ∀f:sys-antecedent(es;X). ∀c:Cut(X;f). ∀i:Id.
((∀e:E(X). ((e ∈ c(i)) ⇐⇒ (loc(e) = i ∈ Id) ∧ e ∈ c))
∧ (∀e,e':E(X). (e before e' ∈ c(i) ⇐⇒ (e <loc e') ∧ (e' ∈ c(i)))))
Proof
Definitions occuring in Statement :
es-cut-at: c(i),
es-cut: Cut(X;f),
sys-antecedent: sys-antecedent(es;Sys),
es-E-interface: E(X),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-locl: (e <loc e'),
es-eq: es-eq(es),
es-loc: loc(e),
Id: Id,
fset-member: a ∈ s,
l_before: x before y ∈ l,
l_member: (x ∈ l),
uall: ∀[x:A]. B[x],
top: Top,
all: ∀x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
universe: Type,
equal: s = t ∈ T
Lemmas :
subtype_rel_fset,
es-E-interface_wf,
es-E_wf,
event-ordering+_subtype,
es-E-interface-strong-subtype,
es-fset-at-property,
Id_wf,
es-cut_wf,
sys-antecedent_wf,
eclass_wf,
top_wf,
event-ordering+_wf,
l_member_subtype,
es-cut-at_wf,
subtype_rel_list,
es-loc_wf,
fset-member_witness,
es-eq_wf,
l_member_wf,
fset-member_wf-cut,
decidable__lt,
length_wf,
false_wf,
less-iff-le,
add_functionality_wrt_le,
add-swap,
add-commutes,
le-add-cancel,
assert_elim,
in-eclass_wf,
subtype_base_sq,
bool_wf,
bool_subtype_base,
assert_wf,
less_than_wf,
select_wf,
sq_stable__le,
es-locl_wf,
es-cut-locl-closed,
list_wf,
l_before_wf,
sorted-by_wf,
es-le_wf,
no_repeats_wf,
no_repeats_iff,
no_repeats-subtype,
l_before-sorted-by,
l_before_member,
l_tricotomy,
es-locl_transitivity2,
es-le_weakening_eq,
es-locl_irreflexivity,
es-le_weakening
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info). \mforall{}X:EClass(Top). \mforall{}f:sys-antecedent(es;X). \mforall{}c:Cut(X;f). \mforall{}i:Id.
((\mforall{}e:E(X). ((e \mmember{} c(i)) \mLeftarrow{}{}\mRightarrow{} (loc(e) = i) \mwedge{} e \mmember{} c))
\mwedge{} (\mforall{}e,e':E(X). (e before e' \mmember{} c(i) \mLeftarrow{}{}\mRightarrow{} (e <loc e') \mwedge{} (e' \mmember{} c(i)))))
Date html generated:
2015_07_21-PM-03_57_08
Last ObjectModification:
2015_01_27-PM-05_59_19
Home
Index