Nuprl Lemma : Memory-loc-class-total

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


Proof




Definitions occuring in Statement :  Memory-loc-class: Memory-loc-class(f;init;X) es-total-class: es-total-class(es;X) 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 bag-size: #(bs) bag: bag(T)
Lemmas :  Memory-loc-class-exists es-loc_wf decidable__lt bag-size_wf event-ordering+_subtype nat_wf false_wf add_functionality_wrt_le add-commutes zero-add le-add-cancel bag-member-iff-size Memory-loc-class_wf eclass_wf es-E_wf decidable__le not-le-2 less-iff-le condition-implies-le minus-add minus-one-mul add-swap add-associates add-zero le-add-cancel2 less_than_wf class-ap_wf all_wf Id_wf le_wf event-ordering+_wf bag_wf

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



Date html generated: 2015_07_22-PM-00_12_54
Last ObjectModification: 2015_01_28-AM-11_39_54

Home Index