---

Step * 2 of Lemma list_of_extensions_in_fin_spr1


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 )
BY
{ (Subst (b  fspr(B)) ~ ff 0 THEN All Reduce THEN MaAuto) }

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



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


By

(Subst  \mkleeneopen{}(b  \mmember{}  fspr(B))  \msim{}  ff\mkleeneclose{}  0\mcdot{}  THEN  All  Reduce  THEN  MaAuto)



Home Index