Nuprl Lemma : send-once-loc-class-nlp
A:ValueAllType'. b:Id 
bag(A). NormalLProgrammable'(A;send-once-loc-class(b))
Proof not projected
Definitions occuring in Statement :
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
send-once-loc-class: send-once-loc-class(b),
Id: Id,
all: x:A. B[x],
function: x:A B[x],
bag: bag(T),
vatype: ValueAllType
Definitions :
all: x:A. B[x],
vatype: ValueAllType,
member: t 
T,
prop: 
,
uall: [x:A]. B[x]
Lemmas :
send-once-loc-class-locally-programmable,
Message_wf,
Message-inhabited,
squash_wf,
Id_wf,
bag_wf,
valueall-type_wf
\mforall{}A:ValueAllType'. \mforall{}b:Id {}\mrightarrow{} bag(A). NormalLProgrammable'(A;send-once-loc-class(b))
Date html generated:
2011_10_20-PM-03_29_28
Last ObjectModification:
2011_08_19-PM-07_52_16
Home
Index