Nuprl Lemma : rsc3_addvote_wf

[Cmd:ValueAllType]. (rsc3_addvote(Cmd)      Cmd  Id  Cmd List  (Id List)  (Cmd List  (Id List)))


Proof not projected



Definitions occuring in Statement :  rsc3_addvote: rsc3_addvote(Cmd),  Id: Id,  uall: [x:A]. B[x],  member: t  T,  function: x:A  B[x],  product: x:A  B[x],  list: type List,  int: ,  vatype: ValueAllType
Definitions :  rsc3_addvote: rsc3_addvote(Cmd),  member: t  T,  vatype: ValueAllType,  uall: [x:A]. B[x]
Lemmas :  valueall-type_wf,  Id_wf
\mforall{}[Cmd:ValueAllType]
    (rsc3\_addvote(Cmd)  \mmember{}  \mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  Cmd  \mtimes{}  Id  {}\mrightarrow{}  Cmd  List  \mtimes{}  (Id  List)  {}\mrightarrow{}  (Cmd  List  \mtimes{}  (Id  List)))


Date html generated: 2012_02_20-PM-04_12_00
Last ObjectModification: 2012_02_02-PM-02_03_24

Home Index