Nuprl Lemma : aa_list_filtered_indices_smaller
T:Type. l:T List. g:
. (||aa_list_filter_indices(l) g|| 
||l||)
Proof not projected
Error : references
\mforall{}T:Type. \mforall{}l:T List. \mforall{}g:\mBbbN{} {}\mrightarrow{} \mBbbB{}. (||aa\_list\_filter\_indices(l) g|| \mleq{} ||l||)
Date html generated:
2013_03_20-AM-11_02_18
Last ObjectModification:
2012_11_27-AM-10_32_13
Home
Index