---

Step * 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 (r,f,l. (r  l z B f)) list_ind_reverse(firstn(||a|| - 1;a);tt;r,f,l. (r  l z B f)) firstn(||a|| - 1;a) la\000Cst(a)
  fi  
= RHS B a
BY
{ (Fold `list-in-fin_spr` 0 THEN Reduce 0) }

1
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



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  (\mlambda{}r,f,l.  (r  \mwedge{}\msubb{}  l  \mleq{}z  B  f))  list\_ind\_reverse(firstn(||a||  -  1;a);tt;\mlambda{}r,f,l.  (r  \mwedge{}\msubb{}  l  \mleq{}z  B  f)) 
              firstn(||a||  -  1;a) 
              last(a)
    fi   
=  RHS  B  a


By

(Fold  `list-in-fin\_spr`  0  THEN  Reduce  0)



Home Index