---

Step * 1 of Lemma gammaFIM_unfold


1. gammaUnfold : Base
2. gammaUnfold ~ h,g,a. if (||a|| = 0) then []
                        if (g (gammaFIM(firstn(||a|| - 1;a);g;h) @ [last(a)]) = 0)
                          then gammaFIM(firstn(||a|| - 1;a);g;h) @ [last(a)]
                        else gammaFIM(firstn(||a|| - 1;a);g;h) @ [h gammaFIM(firstn(||a|| - 1;a);g;h)]
                        fi 
 g,h: List  . a: List.  (gammaFIM(a;g;h) ~ gammaUnfold h g a)
BY
{ (Auto THEN Unfold `gammaFIM` 0 THEN (RWO "list_ind_reverse_unfold1" 0 THENA Auto)) }

1
1. gammaUnfold : Base
2. gammaUnfold ~ h,g,a. if (||a|| = 0) then []
                        if (g (gammaFIM(firstn(||a|| - 1;a);g;h) @ [last(a)]) = 0)
                          then gammaFIM(firstn(||a|| - 1;a);g;h) @ [last(a)]
                        else gammaFIM(firstn(||a|| - 1;a);g;h) @ [h gammaFIM(firstn(||a|| - 1;a);g;h)]
                        fi 
3. g :  List  @i
4. h :  List  @i
5. a :  List@i
 if (||a|| = 0)
then []
else (r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi ) 
     list_ind_reverse(firstn(||a|| - 1;a);[];r,f,l. if (g (r @ [l]) = 0) then r @ [l] else r @ [h r] fi ) 
     firstn(||a|| - 1;a) 
     last(a)
fi 
= (gammaUnfold h g a)



1.  gammaUnfold  :  Base
2.  gammaUnfold  \msim{}  \mlambda{}h,g,a.  if  (||a||  =\msubz{}  0)  then  []
                                                if  (g  (gammaFIM(firstn(||a||  -  1;a);g;h)  @  [last(a)])  =\msubz{}  0)
                                                    then  gammaFIM(firstn(||a||  -  1;a);g;h)  @  [last(a)]
                                                else  gammaFIM(firstn(||a||  -  1;a);g;h)
                                                          @  [h  gammaFIM(firstn(||a||  -  1;a);g;h)]
                                                fi 
\mvdash{}  \mforall{}g,h:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  List.    (gammaFIM(a;g;h)  \msim{}  gammaUnfold  h  g  a)


By

(Auto  THEN  Unfold  `gammaFIM`  0  THEN  (RWO  "list\_ind\_reverse\_unfold1"  0  THENA  Auto))\mcdot{}



Home Index