Nuprl Lemma : pv8_p1_lt_bnum'_wf
[ldrs_uid:Id 
]. (pv8_p1_lt_bnum'(ldrs_uid) 
Id Id 
)
Proof not projected
Definitions occuring in Statement :
pv8_p1_lt_bnum': pv8_p1_lt_bnum'(ldrs_uid),
Id: Id,
bool: ,
uall: [x:A]. B[x],
member: t T,
function: x:A B[x],
product: x:A B[x],
int:
Definitions :
pv8_p1_lt_bnum': pv8_p1_lt_bnum'(ldrs_uid),
member: t T,
uall: [x:A]. B[x]
Lemmas :
Id_wf,
int-deq_wf,
eqof_wf,
band_wf,
lt_int_wf,
bor_wf
\mforall{}[ldrs$_{uid}$:Id {}\mrightarrow{} \mBbbZ{}]. (pv8\_p1\_lt\_bnum'(ldrs$_{uid}$) \mmember{} \mBbbZ{} \000C\mtimes{} Id {}\mrightarrow{} \mBbbZ{} \mtimes{} Id {}\mrightarrow{} \mBbbB{})
Date html generated:
2012_02_20-PM-07_14_08
Last ObjectModification:
2012_02_06-PM-02_04_14
Home
Index