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