Nuprl Lemma : Propose_wf
[Cmd:ValueAllType]. (Propose(Cmd) 
EClass(
Cmd))
Proof not projected
Definitions occuring in Statement :
Propose: Propose(Cmd),
Message: Message,
eclass: EClass(A[eo; e]),
uall: [x:A]. B[x],
member: t T,
product: x:A B[x],
int: ,
vatype: ValueAllType
Lemmas :
member_wf,
name_wf,
base-headers-msg-val_wf,
vatype_wf
\mforall{}[Cmd:ValueAllType]. (Propose(Cmd) \mmember{} EClass(\mBbbZ{} \mtimes{} Cmd))
Date html generated:
2011_10_21-AM-08_21_41
Last ObjectModification:
2011_07_20-AM-04_39_12
Home
Index