Nuprl Lemma : es-interface-history-iseg
∀[Info:Type]
∀es:EO+(Info)
∀[A:Type]. ∀X:EClass(A List). ∀e',e:E. (e ≤loc e' ⇒ es-interface-history(es;X;e) ≤ es-interface-history(es;X;e'))
Proof
Definitions occuring in Statement :
es-interface-history: es-interface-history(es;X;e),
eclass: EClass(A[eo; e]),
event-ordering+: EO+(Info),
es-le: e ≤loc e' ,
es-E: E,
iseg: l1 ≤ l2,
list: T List,
uall: ∀[x:A]. B[x],
all: ∀x:A. B[x],
implies: P ⇒ Q,
universe: Type
Lemmas :
event-ordering+_subtype,
all_wf,
es-E_wf,
es-le_wf,
iseg_wf,
es-interface-history_wf,
decidable__assert,
es-first_wf2,
es-locl_wf,
eclass_wf,
list_wf,
event-ordering+_wf,
iseg_weakening,
ifthenelse_wf,
bool_wf,
equal_wf,
and_wf,
assert_elim,
es-le-first,
assert_of_bnot,
eqff_to_assert,
uiff_transitivity,
eqtt_to_assert,
not_wf,
bnot_wf,
assert_wf,
equal-wf-T-base,
es-le-pred,
es-pred-locl,
eclass-val_wf,
es-pred_wf,
iseg_append,
subtype_top,
top_wf,
es-interface-subtype_rel2,
in-eclass_wf,
iff_weakening_equal,
es-interface-history-pred,
true_wf,
squash_wf
Latex:
\mforall{}[Info:Type]
\mforall{}es:EO+(Info)
\mforall{}[A:Type]
\mforall{}X:EClass(A List). \mforall{}e',e:E.
(e \mleq{}loc e' {}\mRightarrow{} es-interface-history(es;X;e) \mleq{} es-interface-history(es;X;e'))
Date html generated:
2015_07_20-PM-03_39_44
Last ObjectModification:
2015_07_16-AM-09_43_04
Home
Index