---

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


1. B :  List  @i
2. a :  List@i
3. RHS : Base
4. RHS ~ B,a. if (||a|| = 0) then tt else (firstn(||a|| - 1;a)  fspr(B))  last(a) z B firstn(||a|| - 1;a) fi 
 if (||a|| = 0) then tt else (firstn(||a|| - 1;a)  fspr(B))  last(a) z B firstn(||a|| - 1;a) fi  = RHS B a
BY
{ ((HypSubst 4 0 THEN Reduce 0) THEN Auto THEN BLemma `non_null_iff_length`  THEN Auto) }



1.  B  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
2.  a  :  \mBbbN{}  List@i
3.  RHS  :  Base
4.  RHS  \msim{}  \mlambda{}B,a.  if  (||a||  =\msubz{}  0)
                            then  tt
                            else  (firstn(||a||  -  1;a)  \mmember{}  fspr(B))  \mwedge{}\msubb{}  last(a)  \mleq{}z  B  firstn(||a||  -  1;a)
                            fi 
\mvdash{}  if  (||a||  =\msubz{}  0)
    then  tt
    else  (firstn(||a||  -  1;a)  \mmember{}  fspr(B))  \mwedge{}\msubb{}  last(a)  \mleq{}z  B  firstn(||a||  -  1;a)
    fi   
=  RHS  B  a


By

((HypSubst  4  0  THEN  Reduce  0)  THEN  Auto  THEN  BLemma  `non\_null\_iff\_length`    THEN  Auto)\mcdot{}



Home Index