Nuprl Lemma : Proposal_wf
[Cmd:ValueAllType]. (Proposal(Cmd) 
EClass(
Cmd))
Proof not projected
Definitions occuring in Statement :
Proposal: Proposal(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 :
Propose_wf,
Vote_wf,
F_wf,
Message_wf,
simple-comb-2_wf,
vatype_wf
\mforall{}[Cmd:ValueAllType]. (Proposal(Cmd) \mmember{} EClass(\mBbbZ{} \mtimes{} Cmd))
Date html generated:
2011_10_21-AM-08_28_31
Last ObjectModification:
2011_07_20-AM-04_45_21
Home
Index