---

Step * of Lemma list-in-fin_spr_unfold_prp

B: List  . a: List. s:.  ((a @ [s]  fspr(B))  ((a  fspr(B)))  (s  (B a)))
BY
{ ((RepeatFor 3 ((D 0 THENA Auto)) THEN AbbreviateTerm (a  fspr(B)) `RHS1' )
   THEN skip{(RWO "list-in-fin_spr_unfold" 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)))
 (a @ [s]  fspr(B))  (RHS1 a B)  (s  (B a))


\mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  List.  \mforall{}s:\mBbbN{}.    (\muparrow{}(a  @  [s]  \mmember{}  fspr(B))  \mLeftarrow{}{}\mRightarrow{}  (\muparrow{}(a  \mmember{}  fspr(B)))  \mwedge{}  (s  \mleq{}  (B  a)))


By

((RepeatFor  3  ((D  0  THENA  Auto))  THEN  AbbreviateTerm  \mkleeneopen{}\muparrow{}(a  \mmember{}  fspr(B))\mkleeneclose{}  `RHS1'  \mcdot{})
  THEN  skip\{(RWO  "list-in-fin\_spr\_unfold"  0  THENA  Auto)\}
  )



Home Index