Nuprl Lemma : simple-loc-comb-2-classrel-weak

[Info,A,B,C:Type].

[f:Id

A

B

C].

[X:EClass(A)].

[Y:EClass(B)].

[es:EO+(Info)].

[e:E].

[v:C].
(v

lifting-loc-2(f)|Loc,X, Y|(e)

a:A.

b:B. (a

X(e)

b

Y(e)

(v = (f loc(e) a b))))

Proof not projected

Definitions occuring in Statement : lifting-loc-2: lifting-loc-2(f), simple-loc-comb-2: F|Loc,X, Y|, classrel: v

X(e), eclass: EClass(A[eo; e]), event-ordering+: EO+(Info), es-loc: loc(e), es-E: E, Id: Id, uall:

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

x:A. B[x], iff: P

Q, squash:

T, and: P

Q, apply: f a, function: x:A

B[x], universe: Type, equal: s = t
Definitions : uall:

[x:A]. B[x], iff: P

Q, exists:

x:A. B[x], and: P

Q, member: t

T, implies: P

Q, rev_implies: P

Q, prop:

, so_lambda:

x y.t[x; y], uiff: uiff(P;Q), uimplies: b supposing a, all:

x:A. B[x], so_apply: x[s1;s2], subtype: S

T
Lemmas : simple-loc-comb-2-classrel, classrel_wf, simple-loc-comb-2_wf, lifting-loc-2_wf, squash_wf, es-loc_wf, event-ordering+_inc, es-E_wf, event-ordering+_wf, eclass_wf, Id_wf

\mforall{}[Info,A,B,C:Type]. \mforall{}[f:Id {}\mrightarrow{} A {}\mrightarrow{} B {}\mrightarrow{} C]. \mforall{}[X:EClass(A)]. \mforall{}[Y:EClass(B)]. \mforall{}[es:EO+(Info)]. \mforall{}[e:E]. \mforall{}[v:C]. (v \mmember{} lifting-loc-2(f)|Loc,X, Y|(e) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}a:A. \mexists{}b:B. (a \mmember{} X(e) \mwedge{} b \mmember{} Y(e) \mwedge{} (v = (f loc(e) a b)))) Date html generated: 2011_10_20-PM-03_41_56 Last ObjectModification: 2011_08_26-PM-10_55_30 Home Index