---

Step * of Lemma list-in-fin_spr_unfold

B: List  . a: List.
  ((a  fspr(B)) ~ if (||a|| = 0) then tt else (firstn(||a|| - 1;a)  fspr(B))  last(a) z B firstn(||a|| - 1;a) fi )
BY
{ (Auto
   THEN AbbreviateTerm if (||a|| = 0)
        then tt
        else (firstn(||a|| - 1;a)  fspr(B))  last(a) z B firstn(||a|| - 1;a)
        fi  `RHS'
   ) }

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 
 (a  fspr(B)) = RHS B a


\mforall{}B:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  List.
    ((a  \mmember{}  fspr(B))  \msim{}  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  )


By

(Auto
  THEN  AbbreviateTerm  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'\mcdot{}
  )



Home Index