---

Step * 1 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 []
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)
BY
{ (HypSubst' 2 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 
= 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 



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  []
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 
=  (gammaUnfold  h  g  a)


By

(HypSubst'  2  0  THEN  Reduce  0)



Home Index