Nuprl Lemma : bind-class-rel-weak
[Info,T,S:Type]. [es:EO+(Info)]. [X:EClass(T)]. [Y:T 
EClass(S)]. [e:E]. [v:S].
(v 
X >u> Y[u](e) 
e':{e':E| e' 
loc e } . u:T. (u X(e') 
v Y[u](e)))
Proof not projected
Definitions occuring in Statement :
bind-class: X >x> Y[x],
classrel: v X(e),
eclass: EClass(A[eo; e]),
eo-forward: eo.e,
event-ordering+: EO+(Info),
es-le: e loc e' ,
es-E: E,
uall: [x:A]. B[x],
so_apply: x[s],
exists: x:A. B[x],
iff: P Q,
squash: T,
and: P Q,
set: {x:A| B[x]} ,
function: x:A B[x],
universe: Type
Definitions :
so_lambda: 
x y.t[x; y],
bag-member: x bs,
so_lambda: x.t[x],
true: True,
rev_implies: P Q,
implies: P Q,
member: t T,
and: P Q,
exists: x:A. B[x],
squash: T,
so_apply: x[s],
classrel: v X(e),
iff: P Q,
uall: [x:A]. B[x],
uimplies: b supposing a,
so_apply: x[s1;s2],
all: x:A. B[x],
prop: 
,
uiff: uiff(P;Q),
sq_stable: SqStable(P),
subtype: S 
T
Lemmas :
event-ordering+_wf,
eclass_wf,
bind-class_wf,
eo-forward_wf,
and_wf,
es-le_wf,
event-ordering+_inc,
es-E_wf,
exists_wf,
squash_wf,
classrel_wf,
bind-class-rel,
decidable__es-le,
sq_stable_from_decidable,
member-eo-forward-E,
es-loc_wf,
Id_wf,
equal_wf
\mforall{}[Info,T,S:Type]. \mforall{}[es:EO+(Info)]. \mforall{}[X:EClass(T)]. \mforall{}[Y:T {}\mrightarrow{} EClass(S)]. \mforall{}[e:E]. \mforall{}[v:S].
(v \mmember{} X >u> Y[u](e) \mLeftarrow{}{}\mRightarrow{} \mdownarrow{}\mexists{}e':\{e':E| e' \mleq{}loc e \} . \mexists{}u:T. (u \mmember{} X(e') \mwedge{} v \mmember{} Y[u](e)))
Date html generated:
2012_01_23-PM-12_23_09
Last ObjectModification:
2011_12_13-AM-10_35_01
Home
Index