Nuprl Lemma : pv8_p1_max_bnum_wf
[ldrs_uid:Id 
]. (pv8_p1_max_bnum(ldrs_uid) 
Id? Id? ( Id?))
Proof not projected
Definitions occuring in Statement :
pv8_p1_max_bnum: pv8_p1_max_bnum(ldrs_uid),
Id: Id,
uall: [x:A]. B[x],
unit: Unit,
member: t T,
function: x:A B[x],
product: x:A B[x],
union: left + right,
int:
Definitions :
pv8_p1_max_bnum: pv8_p1_max_bnum(ldrs_uid),
member: t T,
uall: [x:A]. B[x]
Lemmas :
unit_wf2,
Id_wf,
pv8_p1_leq_bnum_wf,
ifthenelse_wf
\mforall{}[ldrs$_{uid}$:Id {}\mrightarrow{} \mBbbZ{}]. (pv8\_p1\_max\_bnum(ldrs$_{uid}$) \mmember{} \mBbbZ{} \000C\mtimes{} Id? {}\mrightarrow{} \mBbbZ{} \mtimes{} Id? {}\mrightarrow{} (\mBbbZ{} \mtimes{} Id?))
Date html generated:
2012_02_20-PM-07_14_34
Last ObjectModification:
2012_02_06-PM-02_03_51
Home
Index