Nuprl Lemma : bind-class-rel
[Info,T,S:Type]. [es:EO+(Info)]. [X:EClass(T)]. [Y:T 
EClass(S)]. [e:E]. [v:S].
uiff(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,
uiff: uiff(P;Q),
uall: [x:A]. B[x],
so_apply: x[s],
exists: x:A. B[x],
squash: T,
and: P Q,
set: {x:A| B[x]} ,
function: x:A B[x],
universe: Type
Definitions :
uall: [x:A]. B[x],
uiff: uiff(P;Q),
classrel: v X(e),
so_apply: x[s],
squash: T,
exists: x:A. B[x],
and: P Q,
member: t T,
uimplies: b supposing a,
true: True,
prop: 
,
so_lambda: 
x.t[x],
bag-member: x bs,
all: x:A. B[x],
cand: A c B,
implies: P 
Q,
so_lambda: x y.t[x; y],
eclass: EClass(A[eo; e]),
bind-class: X >x> Y[x],
so_apply: x[s1;s2],
sq_stable: SqStable(P),
rev_uimplies: rev_uimplies(P;Q),
iff: P 
Q,
rev_implies: P Q,
subtype: S 
T
Lemmas :
classrel_wf,
bind-class_wf,
squash_wf,
exists_wf,
es-E_wf,
event-ordering+_inc,
es-le_wf,
eo-forward_wf,
member-eo-forward-E,
equal_wf,
Id_wf,
es-loc_wf,
eclass_wf,
event-ordering+_wf,
es-le-before_wf2,
bag_qinc,
bag-member-combine,
bag-combine_wf,
sq_stable_from_decidable,
decidable__es-le,
and_wf,
bag-member_wf,
l_member_set2,
member-es-le-before,
bag_wf,
l_member_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].
uiff(v \mmember{} X >u> Y[u](e);\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_00
Last ObjectModification:
2011_12_19-PM-03_41_25
Home
Index