---

Step * 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)))
 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))
BY
{ (Assert (||a @ [s]|| = 0) ~ ff BY
         MaAuto) }

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
 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{}if  (||a  @  [s]||  =\msubz{}  0)
    then  tt
    else  (firstn(||a  @  [s]||  -  1;a  @  [s])  \mmember{}  fspr(B))
              \mwedge{}\msubb{}  last(a  @  [s])  \mleq{}z  B  firstn(||a  @  [s]||  -  1;a  @  [s])
    fi 
\mLeftarrow{}{}\mRightarrow{}  (RHS1  a  B)  \mwedge{}  (s  \mleq{}  (B  a))


By

(Assert  (||a  @  [s]||  =\msubz{}  0)  \msim{}  ff  BY
              MaAuto)



Home Index