Nuprl Lemma : send-once-class-locally-programmable
[Info:{Info:Type| 
Info} ]. A:{A:Type| valueall-type(A)} . b:bag(A). NormalLProgrammable(A;Send(b))
Proof not projected
Definitions occuring in Statement :
normal-locally-programmable: NormalLProgrammable(A;X),
send-once-class: Send(b),
uall: [x:A]. B[x],
all: x:A. B[x],
squash: T,
set: {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,
prop: 
,
normal-locally-programmable: NormalLProgrammable(A;X),
sq_exists: 
x:{A| B[x]},
so_lambda: 
x.t[x],
squash: T,
true: True,
send-once-class: Send(b),
dataflow-program: DataflowProgram(A),
unit: Unit,
eclass: EClass(A[eo; e]),
decidable: Dec(P),
or: P 
Q,
so_apply: x[s],
uimplies: b supposing a,
sq_stable: SqStable(P),
implies: P 
Q,
subtype: S 
T
Lemmas :
decidable__assert,
bag-null_wf,
bag_wf,
valueall-type_wf,
squash_wf,
Id_wf,
all_wf,
local-program-at_wf,
send-once-class_wf,
null-df-program_wf,
sq_stable__valueall-type,
dataflow-program_wf,
df-program-type_wf,
once-class-locally-programmable,
unit_wf2,
equal-valueall-type,
it_wf,
es-E_wf,
event-ordering+_inc,
event-ordering+_wf
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}A:\{A:Type| valueall-type(A)\} . \mforall{}b:bag(A). NormalLProgrammable(A;Send(b))
Date html generated:
2012_01_23-PM-12_33_14
Last ObjectModification:
2012_01_01-PM-11_14_58
Home
Index