Nuprl Lemma : max_over_fin_spr_bound

Nuprl Lemma : max_over_fin_spr_bound_length

B,V:

List

.

k:

.

m:

.

a:

List. ((||a||

k)

(

(a

fspr(B)))

((V a)

m))

Proof not projected

Error : references
\mforall{}B,V:\mBbbN{} List {}\mrightarrow{} \mBbbN{}. \mforall{}k:\mBbbN{}. \mexists{}m:\mBbbN{}. \mforall{}a:\mBbbN{} List. ((||a|| \mleq{} k) {}\mRightarrow{} (\muparrow{}(a \mmember{} fspr(B))) {}\mRightarrow{} ((V a) \mleq{} m)) Date html generated: 2013_03_20-AM-11_02_12 Last ObjectModification: 2013_03_18-PM-05_17_00 Home Index