Nuprl Lemma : Memory-class-exists

[Info,B,A:Type]. ∀[f:A ─→ B ─→ B]. ∀[init:Id ─→ bag(B)]. ∀[X:EClass(A)]. ∀[es:EO+(Info)]. ∀[e:E].
  ↓∃v:B. v ∈ Memory-class(f;init;X)(e) supposing 0 < #(init loc(e))


Proof




Definitions occuring in Statement :  Memory-class: Memory-class(f;init;X) classrel: v ∈ X(e) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) es-loc: loc(e) es-E: E Id: Id less_than: a < b uimplies: supposing a uall: [x:A]. B[x] exists: x:A. B[x] squash: T apply: a function: x:A ─→ B[x] natural_number: $n universe: Type bag-size: #(bs) bag: bag(T)
Lemmas :  es-causl-swellfnd nat_properties less_than_transitivity1 less_than_irreflexivity ge_wf less_than_wf bag-size_wf es-loc_wf nat_wf decidable__le subtract_wf false_wf not-ge-2 less-iff-le condition-implies-le minus-one-mul zero-add minus-add minus-minus add-associates add-swap add-commutes add_functionality_wrt_le add-zero le-add-cancel decidable__lt es-causl_wf decidable__assert es-first_wf2 zero-le-nat le_wf add-mul-special zero-mul event-ordering+_subtype es-E_wf event-ordering+_wf eclass_wf Id_wf bag_wf Memory-class_wf classrel_wf es-pred_wf iterated-classrel_wf assert_wf not_wf Memory-classrel2 bag-member-iff-size iff_weakening_equal es-pred-loc-base true_wf squash_wf es-causl_weakening es-pred-locl bag-member_wf all_wf or_wf exists_wf le_weakening empty-bag-iff-size empty-bag-iff-no-member assert-bnot bool_subtype_base subtype_base_sq bool_cases_sqequal equal_wf eqff_to_assert eqtt_to_assert bool_wf

Latex:
\mforall{}[Info,B,A:Type].  \mforall{}[f:A  {}\mrightarrow{}  B  {}\mrightarrow{}  B].  \mforall{}[init:Id  {}\mrightarrow{}  bag(B)].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].  \mforall{}[e:E].
    \mdownarrow{}\mexists{}v:B.  v  \mmember{}  Memory-class(f;init;X)(e)  supposing  0  <  \#(init  loc(e))



Date html generated: 2015_07_22-PM-00_12_49
Last ObjectModification: 2015_07_16-AM-09_39_49

Home Index