Nuprl Lemma : nonempty-es-interface-history
∀[Info:Type]
∀es:EO+(Info)
∀[A:Type]
∀X:EClass(A List). ∀e:E.
(0 < ||es-interface-history(es;X;e)|| ⇐⇒ ∃e':E. (((↑e' ∈b X) ∧ e' ≤loc e ) ∧ 0 < ||X(e')||))
Proof
Definitions occuring in Statement :
es-interface-history: es-interface-history(es;X;e),
eclass-val: X(e),
in-eclass: e ∈b X,
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-le: e ≤loc e' ,
es-E: E,
length: ||as||,
list: T List,
assert: ↑b,
less_than: a < b,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
exists: ∃x:A. B[x],
iff: P ⇐⇒ Q,
and: P ∧ Q,
natural_number: $n,
universe: Type
Lemmas :
less_than_wf,
length_wf,
es-interface-history_wf,
exists_wf,
es-E_wf,
event-ordering+_subtype,
assert_wf,
in-eclass_wf,
es-interface-subtype_rel2,
event-ordering+_wf,
top_wf,
subtype_top,
list_wf,
es-le_wf,
eclass-val_wf,
eclass_wf,
member_exists,
listp-not-nil,
assert_of_lt_int,
lt_int_wf,
member-es-interface-history,
list-cases,
length_of_nil_lemma,
nil_member,
product_subtype_list,
length_of_cons_lemma,
length_wf_nat,
nat_wf,
decidable__lt,
false_wf,
condition-implies-le,
minus-add,
minus-one-mul,
zero-add,
add-commutes,
add_functionality_wrt_le,
add-associates,
add-zero,
le-add-cancel,
l_member_wf,
length_of_not_nil,
member-exists,
member-exists2
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[A:Type]
\mforall{}X:EClass(A List). \mforall{}e:E.
(0 < ||es-interface-history(es;X;e)||
\mLeftarrow{}{}\mRightarrow{} \mexists{}e':E. (((\muparrow{}e' \mmember{}\msubb{} X) \mwedge{} e' \mleq{}loc e ) \mwedge{} 0 < ||X(e')||))
Date html generated:
2015_07_20-PM-03_55_15
Last ObjectModification:
2015_01_27-PM-10_00_21
Home
Index