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: ℤ
Definitions unfolded in proof :
uall: ∀[x:A]. B[x],
member: t ∈ T,
bm_wt: bm_wt(i)
Latex:
\mforall{}[i:\mBbbZ{}]. (bm\_wt(i) \mmember{} \mBbbZ{})
Date html generated:
2016_05_17-PM-01_36_49
Last ObjectModification:
2015_12_28-PM-08_11_13
Theory : binary-map
Home
Index