Nuprl Lemma : Memory-class-functional

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


Definitions occuring in Statement :  Memory-class: Memory-class(f;init;X) es-functional-class: is functional single-valued-classrel: single-valued-classrel(es;X;T) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id uimplies: supposing a uall: [x:A]. B[x] le: A ≤ B all: x:A. B[x] apply: a function: x:A ─→ B[x] natural_number: $n universe: Type single-valued-bag: single-valued-bag(b;T) bag-size: #(bs) bag: bag(T)
Lemmas :  Memory-class-single-val Memory-class-total classrel_wf Memory-class_wf es-E_wf event-ordering+_subtype less_than_wf bag-size_wf class-ap_wf nat_wf single-valued-classrel_wf all_wf Id_wf single-valued-bag_wf le_wf event-ordering+_wf eclass_wf bag_wf

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

Date html generated: 2015_07_22-PM-00_13_02
Last ObjectModification: 2015_01_28-AM-10_46_52

Home Index