Nuprl Lemma : pv8_p1_lt_bnum_wf
[ldrs_uid:Id 
]. (pv8_p1_lt_bnum(ldrs_uid) 
A:
'. ( 
Id + A 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],
unit: Unit,
member: t T,
isect: x:A. B[x],
function: x:A B[x],
product: x:A B[x],
union: left + right,
int: ,
universe: Type
Definitions :
ifthenelse: if b then t else f fi ,
bfalse: ff,
btrue: tt,
outl: outl(x),
isl: isl(x),
bnot: 
b,
band: p 
q,
bor: p 
q,
pv8_p1_lt_bnum: pv8_p1_lt_bnum(ldrs_uid),
member: t T,
uall: [x:A]. B[x]
Lemmas :
isl_wf,
bor_wf,
unit_wf2,
Id_wf,
bfalse_wf,
pv8_p1_lt_bnum'_wf
\mforall{}[ldrs$_{uid}$:Id {}\mrightarrow{} \mBbbZ{}]. (pv8\_p1\_lt\_bnum(ldrs$_{uid}$) \mmember{} \mcap{}A:\000C\mBbbU{}'. (\mBbbZ{} \mtimes{} Id + A {}\mrightarrow{} \mBbbZ{} \mtimes{} Id? {}\mrightarrow{} \mBbbB{}))
Date html generated:
2012_02_20-PM-07_14_21
Last ObjectModification:
2012_02_06-PM-02_04_00
Home
Index