---

Step * 2 1 of Lemma list_of_extensions_in_fin_spr1


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  [])
BY
{ ((InstLemma `firstn_last_sq` [;a]  THENA Auto)
   THEN Try ((BLemma `non_null_iff_length` THEN Auto))
   THEN (Assert ||a|| - 1 ~ ||b|| BY
               Auto)
   THEN HypSubst' (-1) (-2)
   THEN skip{contra}) }

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
8. a ~ firstn(||b||;a) @ [last(a)]
9. ||a|| - 1 ~ ||b||
 (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
5.  \muparrow{}(a  \mmember{}  fspr(B))@i
6.  ||a||  =  (||b||  +  1)@i
7.  firstn(||b||;a)  =  b@i
\mvdash{}  (a  \mmember{}  [])


By

((InstLemma  `firstn\_last\_sq`  [\mkleeneopen{}\mBbbN{}\mkleeneclose{};\mkleeneopen{}a\mkleeneclose{}]  \mcdot{}  THENA  Auto)
  THEN  Try  ((BLemma  `non\_null\_iff\_length`  THEN  Auto))
  THEN  (Assert  ||a||  -  1  \msim{}  ||b||  BY
                          Auto)
  THEN  HypSubst'  (-1)  (-2)
  THEN  skip\{contra\})\mcdot{}



Home Index