1. a : 
2. k : 
3. (p,i. if p(i) 1 else 0 fi)  (a {k} )a {k} 2
  (f,i. f(i)=1)  (a {k} 2)a {k} 

By:	Def of a {k} 2 | a {k}  THEN Analyze-1 THEN Analyze

1

4. f : a2 5. Msize(f) = k   size(a)(i.f(i)=1) = k

3 steps

About: IF YOU CAN SEE THIS go to /sfa/Nuprl/Shared/Xindentation_hack_doc.html