Nuprl Lemma : pv8_p1_leq_bnum_wf
[ldrs_uid:Id 
]. (pv8_p1_leq_bnum(ldrs_uid) 
Id? Id? 
)
Proof not projected
Definitions occuring in Statement :
pv8_p1_leq_bnum: pv8_p1_leq_bnum(ldrs_uid),
Id: Id,
bool: ,
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 :
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
outl: outl(x),
band: p 
q,
isl: isl(x),
bnot: 
b,
bor: p 
q,
pv8_p1_leq_bnum: pv8_p1_leq_bnum(ldrs_uid),
member: t T,
uall: [x:A]. B[x]
Lemmas :
btrue_wf,
unit_wf2,
Id_wf,
bfalse_wf,
pv8_p1_leq_bnum'_wf
\mforall{}[ldrs$_{uid}$:Id {}\mrightarrow{} \mBbbZ{}]. (pv8\_p1\_leq\_bnum(ldrs$_{uid}$) \mmember{} \mBbbZ{} \000C\mtimes{} Id? {}\mrightarrow{} \mBbbZ{} \mtimes{} Id? {}\mrightarrow{} \mBbbB{})
Date html generated:
2012_02_20-PM-07_13_54
Last ObjectModification:
2012_02_06-PM-02_04_19
Home
Index