---

Step * of Lemma gammaFIM_unfold1

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
{ (Auto THEN Auto THEN RWO "gammaFIM_unfold<" 0 THEN Auto) }


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

(Auto  THEN  Auto  THEN  RWO  "gammaFIM\_unfold<"  0\mcdot{}  THEN  Auto)



Home Index