Nuprl Lemma : Accum-class-single-val

∀[Info,A,B:Type]. ∀[es:EO+(Info)].
  ∀X:EClass(A)
    ∀[init:Id ─→ bag(B)]. ∀[f:A ─→ B ─→ B].
      (single-valued-classrel(es;X;A)
      ⇒ (∀l:Id. single-valued-bag(init l;B))
      ⇒ single-valued-classrel(es;Accum-class(f;init;X);B))

Proof

Definitions occuring in Statement : Accum-class: Accum-class(f;init;X), single-valued-classrel: single-valued-classrel(es;X;T), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), Id: Id, uall: ∀[x:A]. B[x], all: ∀x:A. B[x], implies: P ⇒ Q, apply: f a, function: x:A ─→ B[x], universe: Type, single-valued-bag: single-valued-bag(b;T), bag: bag(T)
Lemmas : rec-combined-class-opt-1-single-val, all_wf, Id_wf, single-valued-bag_wf, single-valued-classrel_wf, classrel_wf, Accum-class_wf, es-E_wf, event-ordering+_subtype, bag_wf, eclass_wf, event-ordering+_wf

Latex:
\mforall{}[Info,A,B:Type]. \mforall{}[es:EO+(Info)]. \mforall{}X:EClass(A) \mforall{}[init:Id {}\mrightarrow{} bag(B)]. \mforall{}[f:A {}\mrightarrow{} B {}\mrightarrow{} B]. (single-valued-classrel(es;X;A) {}\mRightarrow{} (\mforall{}l:Id. single-valued-bag(init l;B)) {}\mRightarrow{} single-valued-classrel(es;Accum-class(f;init;X);B)) Date html generated: 2015_07_22-PM-00_17_36 Last ObjectModification: 2015_01_28-AM-10_42_26 Home Index