---

Step * 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 
 (a  fspr(B)) = RHS B a
BY
{ (Auto THEN Unfold `list-in-fin_spr` 0 THEN (RWO "list_ind_reverse_unfold1" 0 THENA Auto)) }

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 (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



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{}  (a  \mmember{}  fspr(B))  =  RHS  B  a


By

(Auto  THEN  Unfold  `list-in-fin\_spr`  0  THEN  (RWO  "list\_ind\_reverse\_unfold1"  0  THENA  Auto))\mcdot{}



Home Index