proofs

[Janis Voigtlaender]

I wrote:

> Rijk-Jan van Haaften writes:
> 
> > I used 3 main properties for the process:
> > ...
> > 2. Lifting local let definitions to a higher level
> > let
> >          f =
> >                  let
> >                          g = gExpr
> >                  in
> >                          fExpr
> > in
> >          expr
> > 
> > can be translated into
> > ...
>
> Care has to be taken if g (which might be bound outside this let-block) occurs 
> in expr, because with the translated version it is now bound to gExpr. 
Renaming 
> helps (for some unused g'):
> > let
> >          g' = gExpr
> >          f  = fExpr[g <- g']
> > in
> >          expr

Oops:

let
         g' = gExpr[g <- g']
         f  = fExpr[g <- g']
in
         expr

Hope, I got it right now.
Janis.

--
Janis Voigtlaender
http://wwwtcs.inf.tu-dresden.de/~voigt/
mailto:voigt@tcs.inf.tu-dresden.de