---

Step * of Lemma list_of_extensions_in_fin_spr1

B: List  . b,a: List.
  ({((a  fspr(B)))  (||a|| = (||b|| + 1))  (firstn(||b||;a) = b)}  (a  list_of_extensions_in_fin_spr(B;b)))
BY
{ (Unfold `guard` 0
   THEN ((UnivCD THENA Auto)
         THEN (BoolCase (b  fspr(B)) THENA Auto)
         THEN Unfold `list_of_extensions_in_fin_spr` 0
         THEN skip{(AutoSplit THEN Auto)})
   ) }

1
1. B :  List  @i
2. b :  List@i
3. a :  List@i
4. (b  fspr(B))
 ((a  fspr(B)))  (||a|| = (||b|| + 1))  (firstn(||b||;a) = b)
 (a  if (b  fspr(B)) then mklist((B b) + 1;i.(b @ [i])) else [] fi )

2
1. B :  List  @i
2. b :  List@i
3. (b  fspr(B))
4. a :  List@i
 ((a  fspr(B)))  (||a|| = (||b|| + 1))  (firstn(||b||;a) = b)
 (a  if (b  fspr(B)) then mklist((B b) + 1;i.(b @ [i])) else [] fi )


\mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}b,a:\mBbbN{}  List.
    (\{(\muparrow{}(a  \mmember{}  fspr(B)))  \mwedge{}  (||a||  =  (||b||  +  1))  \mwedge{}  (firstn(||b||;a)  =  b)\}
    \mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  list\_of\_extensions\_in\_fin\_spr(B;b)))


By

(Unfold  `guard`  0
  THEN  ((UnivCD  THENA  Auto)
              THEN  (BoolCase  \mkleeneopen{}(b  \mmember{}  fspr(B))\mkleeneclose{}\mcdot{}  THENA  Auto)
              THEN  Unfold  `list\_of\_extensions\_in\_fin\_spr`  0
              THEN  skip\{(AutoSplit  THEN  Auto)\})
  )



Home Index