---

Step * of Lemma gammaFIM_unfold

g,h: List  . a: List.
  (gammaFIM(a;g;h) ~ 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 )
BY
{ (AbbreviateTerm 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' 
   THEN skip{appreving RHS to prevent unfoldings in RHS}
   ) }

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 
 g,h: List  . a: List.  (gammaFIM(a;g;h) ~ gammaUnfold h g a)


\mforall{}g,h:\mBbbN{}  List  {}\mrightarrow{}  \mBbbN{}.  \mforall{}a:\mBbbN{}  List.
    (gammaFIM(a;g;h)  \msim{}  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  )


By

(AbbreviateTerm  \mkleeneopen{}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  \mkleeneclose{}  `gammaUnfold'  \mcdot{}
  THEN  skip\{appreving  RHS  to  prevent  unfoldings  in  RHS\}
  )



Home Index