---

Step * 1 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 
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)
BY
{ (Fold `gammaFIM` 0 THEN Reduce 0) }

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 []
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 
= (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 
3.  g  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
4.  h  :  \mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}@i
5.  a  :  \mBbbN{}  List@i
\mvdash{}  if  (||a||  =\msubz{}  0)
then  []
else  (\mlambda{}r,f,l.  if  (g  (r  @  [l])  =\msubz{}  0)  then  r  @  [l]  else  r  @  [h  r]  fi  ) 
          list\_ind\_reverse(firstn(||a||  -  1;a);[];\mlambda{}r,f,l.  if  (g  (r  @  [l])  =\msubz{}  0)
                                                                                                        then  r  @  [l]
                                                                                                        else  r  @  [h  r]
                                                                                                        fi  ) 
          firstn(||a||  -  1;a) 
          last(a)
fi 
=  (gammaUnfold  h  g  a)


By

(Fold  `gammaFIM`  0  THEN  Reduce  0)\mcdot{}



Home Index