  A non-deterministic call-by-need lambda-calculus \calc with case,
constructors, letrec and a (non-deterministic) erratic choice, based on
rewriting rules is investigated. A standard reduction is defined as a variant
of left-most outermost reduction. The semantics is defined by contextual
equivalence of expressions instead of using $\alpha\beta(\eta)$-equivalence. It
is shown that several program transformations are correct, for example all
(deterministic) rules of the calculus, and in addition the rules for garbage
collection, removing indirections and unique copy.
  This shows that the combination of a context lemma and a meta-rewriting on
reductions using complete sets of commuting (forking, resp.) diagrams is a
useful and successful method for providing a semantics of a functional
programming language and proving correctness of program transformations.
