Nuprl Lemma : ler2_positive_epoch

eo:EO'. e:E. v:  Id.  (v  Nbr(e)  (let epoch,succ = v in 0 <z epoch (IntDeq epoch 0)))


Proof not projected

Error : references
\mforall{}eo:EO'.  \mforall{}e:E.  \mforall{}v:\mBbbZ{}  \mtimes{}  Id.    (v  \mmember{}  Nbr(e)  {}\mRightarrow{}  (\muparrow{}let  epoch,succ  =  v  in  0  <z  epoch  \mvee{}\msubb{}(IntDeq  epoch  0)))


Date html generated: 2012_02_20-PM-07_51_05
Last ObjectModification: 2012_02_02-PM-02_42_11

Home Index