---

Step * of Lemma list_of_lists_of_given_size_in_fin_spr1

B: List  . k:. a: List.  (((a  fspr(B)))  (||a|| = k)  (a  list_of_lists_of_given_size_in_fin_spr(B;k)))
BY
{ (RepeatFor 2 ((D 0 THENA Auto))
   THEN NatInd (-1)
   THEN Unfold `list_of_lists_of_given_size_in_fin_spr` 0
   THEN Reduce 0) }

1
1. B :  List  @i
 a: List. (((a  fspr(B)))  (||a|| = 0)  (a  [[]]))

2
1. B :  List  @i
2. k : 
3. 0 < k
4. a: List. (((a  fspr(B)))  (||a|| = (k - 1))  (a  list_of_lists_of_given_size_in_fin_spr(B;k - 1)))
 a: List
    (((a  fspr(B)))  (||a|| = k)
     (a  primrec(k;[[]];n,rl. l-union-list(list-deq(NatDeq);map(b.list_of_extensions_in_fin_spr(B;b);rl)))))


\mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}k:\mBbbN{}.  \mforall{}a:\mBbbN{}  List.
    ((\muparrow{}(a  \mmember{}  fspr(B)))  \mwedge{}  (||a||  =  k)  \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  list\_of\_lists\_of\_given\_size\_in\_fin\_spr(B;k)))


By

(RepeatFor  2  ((D  0  THENA  Auto))
  THEN  NatInd  (-1)
  THEN  Unfold  `list\_of\_lists\_of\_given\_size\_in\_fin\_spr`  0
  THEN  Reduce  0)



Home Index