---

Step * 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)))
 (a @ [s]  fspr(B))  (RHS1 a B)  (s  (B a))
BY
{ ((RWO "list-in-fin_spr_unfold" 0 THENA Auto) THEN Reduce 0) }

1
1. B :  List  @i
2. a :  List@i
3. s : @i
4. RHS1 : Base
5. RHS1 ~ a,B. ((a  fspr(B)))
 if (||a @ [s]|| = 0)
  then tt
  else (firstn(||a @ [s]|| - 1;a @ [s])  fspr(B))  last(a @ [s]) z B firstn(||a @ [s]|| - 1;a @ [s])
  fi 
 (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)))
\mvdash{}  \muparrow{}(a  @  [s]  \mmember{}  fspr(B))  \mLeftarrow{}{}\mRightarrow{}  (RHS1  a  B)  \mwedge{}  (s  \mleq{}  (B  a))


By

((RWO  "list-in-fin\_spr\_unfold"  0  THENA  Auto)  THEN  Reduce  0)



Home Index