Nuprl Lemma : send-once-loc-prc_wf
[Info:{Info:Type| 
Info} ]
A:{A:Type| valueall-type(A)} . b:Id 
bag(A).
(send-once-loc-prc(A;b) 
NormalLProgrammable(A;send-once-loc-class(b)))
Proof not projected
Definitions occuring in Statement :
send-once-loc-prc: send-once-loc-prc(A;b),
normal-locally-programmable: NormalLProgrammable(A;X),
send-once-loc-class: send-once-loc-class(b),
Id: Id,
uall: [x:A]. B[x],
all: x:A. B[x],
squash: T,
member: t T,
set: {x:A| B[x]} ,
function: x:A B[x],
universe: Type,
bag: bag(T),
valueall-type: valueall-type(T)
Definitions :
uall: [x:A]. B[x],
all: x:A. B[x],
member: t T,
send-once-loc-prc: send-once-loc-prc(A;b),
once-prog: once-prog(dfp),
unit: Unit,
it: 
,
send-once-loc-class-locally-programmable,
once-class-locally-programmable,
evalall: evalall(t),
ifthenelse: if b then t else f fi ,
bag-null: bag-null(bs),
spreadn: spread4,
btrue: tt,
bfalse: ff,
null: null(as),
prop: 
,
so_lambda: 
x.t[x],
implies: P 
Q,
so_apply: x[s]
Lemmas :
uall_wf,
squash_wf,
valueall-type_wf,
Id_wf,
bag_wf,
normal-locally-programmable_wf,
send-once-loc-class_wf
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}A:\{A:Type| valueall-type(A)\} . \mforall{}b:Id {}\mrightarrow{} bag(A).
(send-once-loc-prc(A;b) \mmember{} NormalLProgrammable(A;send-once-loc-class(b)))
Date html generated:
2011_10_20-PM-03_25_51
Last ObjectModification:
2011_09_26-AM-10_51_44
Home
Index