Nuprl Lemma : bm_wt_wf
∀[i:ℤ]. (bm_wt(i) ∈ ℤ)
Proof
Definitions occuring in Statement :
bm_wt: bm_wt(i),
uall: ∀[x:A]. B[x],
member: t ∈ T,
int: ℤ
\mforall{}[i:\mBbbZ{}]. (bm\_wt(i) \mmember{} \mBbbZ{})
Date html generated:
2015_07_17-AM-08_17_30
Last ObjectModification:
2015_01_27-PM-00_40_11
Home
Index