Nuprl Lemma : oar-deliver_wf

[Info:Type]. ∀[es:EO+(Info)].
  ∀M:Type. ∀V:EClass(Id × Atom1 × Id × ℕ × M). ∀correct:Id ─→ ℙ. ∀f:ℕ. ∀orderers:bag(Id).
  ∀OARDeliver:EClass(Id × ℕ × M).
    (oar-deliver(es;M;V;correct;orderers;f;OARDeliver) ∈ ℙ)


Proof




Definitions occuring in Statement :  oar-deliver: oar-deliver(es;M;V;correct;orderers;f;OARDeliver) eclass: EClass(A[eo; e]) event-ordering+: EO+(Info) Id: Id nat: atom: Atom$n uall: [x:A]. B[x] prop: all: x:A. B[x] member: t ∈ T function: x:A ─→ B[x] product: x:A × B[x] universe: Type bag: bag(T)
Lemmas :  all_wf es-E_wf event-ordering+_subtype classrel_wf es-loc_wf less_than_wf exists_wf es-locl_wf subtract_wf decidable__le false_wf not-le-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 le_wf list_wf length_wf no_repeats_wf l_all_wf2 l_member_wf bag-member_wf es-E-interface_wf es-interface-subtype_rel2 top_wf subtype_top es-le_wf eclass_wf Id_wf nat_wf event-ordering+_wf bag_wf

Latex:
\mforall{}[Info:Type].  \mforall{}[es:EO+(Info)].
    \mforall{}M:Type.  \mforall{}V:EClass(Id  \mtimes{}  Atom1  \mtimes{}  Id  \mtimes{}  \mBbbN{}  \mtimes{}  M).  \mforall{}correct:Id  {}\mrightarrow{}  \mBbbP{}.  \mforall{}f:\mBbbN{}.  \mforall{}orderers:bag(Id).
    \mforall{}OARDeliver:EClass(Id  \mtimes{}  \mBbbN{}  \mtimes{}  M).
        (oar-deliver(es;M;V;correct;orderers;f;OARDeliver)  \mmember{}  \mBbbP{})



Date html generated: 2015_07_23-PM-00_26_50
Last ObjectModification: 2015_01_29-AM-01_30_03

Home Index