---

Step * 1 1 1 1 of Lemma list-in-fin_spr_unfold_prp


1. B :  List  @i
2. a :  List@i
3. s : @i
4. RHS1 : Base
5. RHS1 ~ a,B. ((a  fspr(B)))
6. (||a @ [s]|| = 0) ~ ff
 ((firstn(||a @ [s]|| - 1;a @ [s])  fspr(B))  last(a @ [s]) z B firstn(||a @ [s]|| - 1;a @ [s]))
 (RHS1 a B)  (s  (B a))
BY
{ ((RWO "firstn_append_front_singleton" 0 THENA Auto) THEN (RWO "last_append_singleton" 0 THENA Auto)) }

1
1. B :  List  @i
2. a :  List@i
3. s : @i
4. RHS1 : Base
5. RHS1 ~ a,B. ((a  fspr(B)))
6. (||a @ [s]|| = 0) ~ ff
 ((a  fspr(B))  s z B a)  (RHS1 a B)  (s  (B a))



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  a  :  \mBbbN{}  List@i
3.  s  :  \mBbbN{}@i
4.  RHS1  :  Base
5.  RHS1  \msim{}  \mlambda{}a,B.  (\muparrow{}(a  \mmember{}  fspr(B)))
6.  (||a  @  [s]||  =\msubz{}  0)  \msim{}  ff
\mvdash{}  \muparrow{}((firstn(||a  @  [s]||  -  1;a  @  [s])  \mmember{}  fspr(B))
    \mwedge{}\msubb{}  last(a  @  [s])  \mleq{}z  B  firstn(||a  @  [s]||  -  1;a  @  [s]))
\mLeftarrow{}{}\mRightarrow{}  (RHS1  a  B)  \mwedge{}  (s  \mleq{}  (B  a))


By

((RWO  "firstn\_append\_front\_singleton"  0  THENA  Auto)  THEN  (RWO  "last\_append\_singleton"  0  THENA  Auto))



Home Index