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) 
e c))
(e,e':E(X). (e before e' c(i) (e <loc e') (e' c(i)))))
Proof not projected
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-loc: loc(e),
es-eq: es-eq(es),
Id: Id,
uall: [x:A]. B[x],
top: Top,
all: x:A. B[x],
iff: P Q,
and: P Q,
universe: Type,
equal: s = t,
l_before: x before y l,
l_member: (x l),
fset-member: a s
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
member: t T,
so_lambda: 
x y.t[x; y],
and: P Q,
iff: P Q,
implies: P Q,
rev_implies: P Q,
prop: 
,
sq_stable: SqStable(P),
so_lambda: x.t[x],
subtype: S 
T,
cand: A c B,
es-E-interface: E(X),
true: True,
ifthenelse: if b then t else f fi ,
btrue: tt,
assert: 
b,
exists: 
x:A. B[x],
l_member: (x l),
label: ...$L... t,
es-cut: Cut(X;f),
uimplies: b supposing a,
so_apply: x[s1;s2],
so_apply: x[s],
sq_type: SQType(T),
guard: {T},
nat: 
,
uiff: uiff(P;Q),
es-le: e 
loc e' ,
not: 
A,
or: P 
Q,
false: False,
es-cut-at: c(i)
Lemmas :
subtype_rel_fset,
es-E-interface_wf,
es-E_wf,
event-ordering+_inc,
es-E-interface-strong-subtype,
es-fset-at-property,
Id_wf,
es-cut_wf,
sys-antecedent_wf,
eclass_wf,
top_wf,
event-ordering+_wf,
property-from-l_member,
equal_wf,
es-loc_wf,
sq_stable__equal,
squash_wf,
es-cut-at_wf,
l_member_wf,
fset-member_wf-cut,
l_member_subtype,
assert_wf,
in-eclass_wf,
es-eq_wf,
fset-member_witness,
assert_elim,
bool_subtype_base,
bool_wf,
subtype_base_sq,
select_wf,
length_wf,
es-locl_wf,
l_before_wf,
sorted-by_wf,
es-le_wf,
no_repeats_wf,
Error :eclass_wf,
no_repeats_iff,
no_repeats-settype,
l_before-sorted-by,
subtype_rel_list,
l_before_member,
l_tricotomy,
es-locl_irreflexivity,
es-le_weakening_eq,
es-locl_transitivity2,
es-le_weakening
\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:
2012_01_23-PM-12_28_37
Last ObjectModification:
2011_12_31-PM-10_07_28
Home
Index