{ 
A:ValueAllType'. b:bag(A). NormalLProgrammable'(A;Send(b)) }
{ Proof }
Definitions occuring in Statement :
Message: Message,
normal-locally-programmable: NormalLProgrammable(A;X),
send-once-class: Send(b),
all: x:A. B[x],
bag: bag(T),
vatype: ValueAllType
Lemmas :
Message-inhabited,
squash_wf,
Message_wf,
subtype_rel_wf,
member_wf,
send-once-class-locally-programmable,
valueall-type_wf,
bag_wf
\mforall{}A:ValueAllType'. \mforall{}b:bag(A). NormalLProgrammable'(A;Send(b))
Date html generated:
2011_08_17-PM-04_11_44
Last ObjectModification:
2011_07_20-AM-02_02_33
Home
Index