Nuprl Lemma : Memory-class-es-sv

[Info,A:Type]. ∀[init:Id ─→ bag(Top)]. ∀[f:Top]. ∀[X:EClass(A)]. ∀[es:EO+(Info)].
  (es-sv-class(es;Memory-class(f;init;X))) supposing (es-sv-class(es;X) and (∀l:Id. (#(init l) ≤ 1)))


Definitions occuring in Statement :  Memory-class: Memory-class(f;init;X) es-sv-class: es-sv-class(es;X) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id uimplies: supposing a uall: [x:A]. B[x] top: Top le: A ≤ B all: x:A. B[x] apply: a function: x:A ─→ B[x] natural_number: $n universe: Type bag-size: #(bs) bag: bag(T)
Lemmas :  primed-class-opt_wf rec-combined-class-opt-1_wf lifting-2_wf es-sv-class_wf all_wf le_wf bag-size_wf nat_wf eclass_wf es-E_wf event-ordering+_subtype event-ordering+_wf top_wf Id_wf bag_wf less_than_wf squash_wf sq_stable__all sq_stable__le primed-class-opt-es-sv Accum-class_wf Accum-class-es-sv

\mforall{}[Info,A:Type].  \mforall{}[init:Id  {}\mrightarrow{}  bag(Top)].  \mforall{}[f:Top].  \mforall{}[X:EClass(A)].  \mforall{}[es:EO+(Info)].
    (es-sv-class(es;Memory-class(f;init;X)))  supposing 
          (es-sv-class(es;X)  and 
          (\mforall{}l:Id.  (\#(init  l)  \mleq{}  1)))

Date html generated: 2015_07_22-PM-00_18_11
Last ObjectModification: 2015_01_28-AM-10_42_47

Home Index