Nuprl Lemma : prior-latest-val
∀[Info,T:Type]. ∀[X:EClass(T)]. (((X)-)' = (X)' ∈ EClass(T))
Proof
Definitions occuring in Statement :
es-latest-val: (X)-,
es-prior-val: (X)',
eclass: EClass(A[eo; e]),
uall: ∀[x:A]. B[x],
universe: Type,
equal: s = t ∈ T
Lemmas :
es-interface-extensionality,
es-prior-val_wf,
es-latest-val_wf,
in-eclass_wf,
es-prior-interface_wf1,
es-interface-subtype_rel2,
es-E_wf,
event-ordering+_subtype,
subtype_top,
es-E-interface_wf,
top_wf,
bool_wf,
eqtt_to_assert,
bag_size_single_lemma,
false_wf,
eqff_to_assert,
equal_wf,
bool_cases_sqequal,
subtype_base_sq,
bool_subtype_base,
assert-bnot,
bag_size_empty_lemma,
es-le_weakening_eq,
es-le_wf,
assert_wf,
event-ordering+_wf,
es-locl_wf,
exists_wf,
es-locl_transitivity1,
is-prior-val,
is-latest-val,
all_wf,
iff_wf,
prior-val-val,
latest-val-cases,
es-locl-total,
eclass-val_wf,
has-latest-val,
decidable__es-le,
decidable__es-locl,
es-le-not-locl,
not_assert_elim,
and_wf,
assert_elim,
btrue_neq_bfalse,
es-locl_transitivity2,
es-le_weakening
Latex:
\mforall{}[Info,T:Type]. \mforall{}[X:EClass(T)]. (((X)\msupminus{})' = (X)')
Date html generated:
2015_07_21-PM-04_21_07
Last ObjectModification:
2015_01_27-PM-05_24_35
Home
Index