Nuprl Lemma : RSC_addvote_wf

RSC_addvote()  B,A:'.  (    B  A  B List  (A List)  (B List  (A List)))


Proof not projected



Definitions occuring in Statement :  RSC_addvote: RSC_addvote(),  member: t  T,  isect: x:A. B[x],  function: x:A  B[x],  product: x:A  B[x],  list: type List,  int: ,  universe: Type
Definitions :  member: t  T,  RSC_addvote: RSC_addvote()
RSC\_addvote()  \mmember{}  \mcap{}B,A:\mBbbU{}'.    (\mBbbZ{}  \mtimes{}  \mBbbZ{}  \mtimes{}  B  \mtimes{}  A  {}\mrightarrow{}  B  List  \mtimes{}  (A  List)  {}\mrightarrow{}  (B  List  \mtimes{}  (A  List)))


Date html generated: 2012_02_20-PM-03_40_00
Last ObjectModification: 2012_02_02-PM-01_58_19

Home Index