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: 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