---

Step * 1 2 of Lemma list_of_extensions_in_fin_spr1


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  mklist((B b) + 1;i.(b @ [i])))
BY
{ RepeatFor 2 ((D 0 THENA Auto)) }

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

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



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  b  :  \mBbbN{}  List@i
3.  a  :  \mBbbN{}  List@i
4.  \muparrow{}(b  \mmember{}  fspr(B))
\mvdash{}  (\muparrow{}(a  \mmember{}  fspr(B)))  \mwedge{}  (||a||  =  (||b||  +  1))  \mwedge{}  (firstn(||b||;a)  =  b)
\mLeftarrow{}{}\mRightarrow{}  (a  \mmember{}  mklist((B  b)  +  1;\mlambda{}i.(b  @  [i])))


By

RepeatFor  2  ((D  0\mcdot{}  THENA  Auto))



Home Index