Nuprl Lemma : simple-loc-comb-1-concat-single-val

∀[Info:Type]. ∀[es:EO+(Info)]. ∀[A,B:Type]. ∀[F:Id ─→ A ─→ bag(B)]. ∀[X:EClass(A)].
  (single-valued-classrel(es;F@(Loc, X);B)) supposing
     ((∀i:Id. ∀a:A. ∀e:E.  (a ∈ X(e) ⇒ single-valued-bag(F i a;B))) and
     single-valued-classrel(es;X;A))

Proof

Definitions occuring in Statement : concat-lifting-loc-1: f@, simple-loc-comb-1: F(Loc, X), single-valued-classrel: single-valued-classrel(es;X;T), classrel: v ∈ X(e), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-E: E, Id: Id, uimplies: b supposing a, 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 : simple-loc-comb-1-concat-classrel, bag-member_wf, es-loc_wf, classrel_wf, simple-loc-comb-1_wf, concat-lifting-loc-1_wf, es-E_wf, event-ordering+_subtype, all_wf, Id_wf, single-valued-bag_wf, single-valued-classrel_wf, eclass_wf, event-ordering+_wf, bag_wf

Latex:
\mforall{}[Info:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[A,B:Type]. \mforall{}[F:Id {}\mrightarrow{} A {}\mrightarrow{} bag(B)]. \mforall{}[X:EClass(A)]. (single-valued-classrel(es;F@(Loc, X);B)) supposing ((\mforall{}i:Id. \mforall{}a:A. \mforall{}e:E. (a \mmember{} X(e) {}\mRightarrow{} single-valued-bag(F i a;B))) and single-valued-classrel(es;X;A)) Date html generated: 2015_07_22-PM-00_16_01 Last ObjectModification: 2015_01_28-AM-10_43_45 Home Index