Nuprl Lemma : rec-combined-loc-class-opt-1-single-val

[Info,A,B:Type].

[es:EO+(Info)].

[F:Id

A

B

B].

[X:EClass(A)].

[init:Id

bag(B)].
  (single-valued-classrel(es;lifting-loc-2(F)|Loc, X, Prior(self)?init|;B)) supposing
     (single-valued-classrel(es;X;A) and
     (

l:Id. single-valued-bag(init l;B)))

Proof not projected

Definitions occuring in Statement : lifting-loc-2: lifting-loc-2(f), rec-combined-loc-class-opt-1: F|Loc, X, Prior(self)?init|, single-valued-classrel: single-valued-classrel(es;X;T), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), Id: Id, uimplies: b supposing a, uall:

[x:A]. B[x], all:

x:A. B[x], apply: f a, function: x:A

B[x], universe: Type, single-valued-bag: single-valued-bag(b;T), bag: bag(T)
Definitions : so_lambda:

x y.t[x; y], so_lambda:

x.t[x], member: t

T, implies: P

Q, single-valued-classrel: single-valued-classrel(es;X;T), all:

x:A. B[x], so_apply: x[s1;s2], so_apply: x[s], prop:

, uimplies: b supposing a, uall:

[x:A]. B[x], subtype: S

T, guard: {T}
Lemmas : event-ordering+_wf, eclass_wf, bag_wf, single-valued-bag_wf, Id_wf, all_wf, single-valued-classrel_wf, es-loc_wf, event-ordering+_inc, es-E_wf, lifting-loc-2_wf, rec-combined-loc-class-opt-1_wf, classrel_wf, rec-combined-loc-class-opt-1-single-val0

\mforall{}[Info,A,B:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[F:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} B]. \mforall{}[X:EClass(A)]. \mforall{}[init:Id {}\mrightarrow{} bag(B)]. (single-valued-classrel(es;lifting-loc-2(F)|Loc, X, Prior(self)?init|;B)) supposing (single-valued-classrel(es;X;A) and (\mforall{}l:Id. single-valued-bag(init l;B))) Date html generated: 2012_02_20-PM-02_58_02 Last ObjectModification: 2012_02_07-PM-12_46_46 Home Index