Nuprl Lemma : ohc_v2_newvote_wf
ohc_v2_newvote() 
B,A:
'. (
B Id A (Id List) 
)
Proof not projected
Definitions occuring in Statement :
ohc_v2_newvote: ohc_v2_newvote(),
Id: Id,
bool: ,
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,
ohc_v2_newvote: ohc_v2_newvote(),
uall: 
[x:A]. B[x]
Lemmas :
band_wf,
eqof_wf,
product-deq_wf,
int-deq_wf,
bnot_wf,
deq-member_wf,
Id_wf,
id-deq_wf
ohc\_v2\_newvote() \mmember{} \mcap{}B,A:\mBbbU{}'. (\mBbbZ{} \mtimes{} \mBbbZ{} {}\mrightarrow{} \mBbbZ{} \mtimes{} \mBbbZ{} \mtimes{} B \mtimes{} Id {}\mrightarrow{} A \mtimes{} (Id List) {}\mrightarrow{} \mBbbB{})
Date html generated:
2012_02_20-PM-05_32_52
Last ObjectModification:
2012_02_17-PM-10_31_43
Home
Index