Nuprl Lemma : bind-prc_wf
[Info:{Info:Type| 
Info} ]
A,B:{T:Type| valueall-type(T)} .
[X:EClass(A)]. [Y:A 
EClass(B)].
Xpr:NormalLProgrammable(A;X). Ypr:a:A. NormalLProgrammable(B;Y[a]).
(bind-prc(A;B;Xpr;Ypr) 
NormalLProgrammable(B;X >a> Y[a]))
Proof not projected
Definitions occuring in Statement :
bind-prc: bind-prc(A;B;Xpr;Ypr),
normal-locally-programmable: NormalLProgrammable(A;X),
bind-class: X >x> Y[x],
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
so_apply: x[s],
all: x:A. B[x],
squash: T,
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
universe: Type,
valueall-type: valueall-type(T)
Definitions :
so_lambda: 
x y.t[x; y],
so_lambda: x.t[x],
prop: 
,
implies: P 
Q,
bind-class-locally-programmable,
bind-prc: bind-prc(A;B;Xpr;Ypr),
member: t T,
so_apply: x[s],
all: x:A. B[x],
uall: [x:A]. B[x],
so_apply: x[s1;s2],
subtype: S 
T
Lemmas :
bind-class_wf,
normal-locally-programmable_wf,
event-ordering+_wf,
event-ordering+_inc,
es-E_wf,
eclass_wf,
valueall-type_wf,
squash_wf,
uall_wf
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}A,B:\{T:Type| valueall-type(T)\} .
\mforall{}[X:EClass(A)]. \mforall{}[Y:A {}\mrightarrow{} EClass(B)].
\mforall{}Xpr:NormalLProgrammable(A;X). \mforall{}Ypr:\mforall{}a:A. NormalLProgrammable(B;Y[a]).
(bind-prc(A;B;Xpr;Ypr) \mmember{} NormalLProgrammable(B;X >a> Y[a]))
Date html generated:
2011_10_20-PM-03_26_24
Last ObjectModification:
2011_08_15-PM-05_03_03
Home
Index