{ 
[Info:{Info:Type| 
Info} ]
A:{A:Type| valueall-type(A)} . b:bag(A).
(send-once-prc(A;b) 
NormalLProgrammable(A;Send(b))) }
{ Proof }
Definitions occuring in Statement :
send-once-prc: send-once-prc(A;b),
normal-locally-programmable: NormalLProgrammable(A;X),
send-once-class: Send(b),
uall: [x:A]. B[x],
all: x:A. B[x],
squash: T,
member: t 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,
send-once-prc: send-once-prc(A;b),
btrue: tt,
bfalse: ff,
null-df-program: null-df-program(B),
unit: Unit,
it: 
,
send-once-class-locally-programmable,
decidable__assert,
bag-null: bag-null(bs),
null: null(as),
empty-bag: {},
once-prog: once-prog(dfp),
once-class-locally-programmable,
evalall: evalall(t),
ifthenelse: if b then t else f fi ,
spreadn: spread4,
prop: 
,
so_lambda: 
x.t[x],
implies: P 
Q,
so_apply: x[s]
Lemmas :
uall_wf,
squash_wf,
valueall-type_wf,
bag_wf,
normal-locally-programmable_wf,
send-once-class_wf
\mforall{}[Info:\{Info:Type| \mdownarrow{}Info\} ]
\mforall{}A:\{A:Type| valueall-type(A)\} . \mforall{}b:bag(A). (send-once-prc(A;b) \mmember{} NormalLProgrammable(A;Send(b)))
Date html generated:
2011_08_16-PM-06_33_21
Last ObjectModification:
2011_08_13-PM-09_21_56
Home
Index