---

Step * 1 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  if (b  fspr(B)) then mklist((B b) + 1;i.(b @ [i])) else [] fi )
BY
{ (Subst (b  fspr(B)) ~ tt 0 THEN (All Reduce THENA skip{MaAuto})) }

1
1. B :  List  @i
2. b :  List@i
3. a :  List@i
4. (b  fspr(B))
 (b  fspr(B)) ~ tt

2
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])))



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{}  if  (b  \mmember{}  fspr(B))  then  mklist((B  b)  +  1;\mlambda{}i.(b  @  [i]))  else  []  fi  )


By

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



Home Index