(* is reduced, the delta-reduction is succesfull and the whole algorithm *)
(* is applied again to the new redex; Step 3) is applied to the result *)
(* of the recursive simplification. Otherwise, if the Fix can not be *)
(* is reduced, the delta-reduction is succesfull and the whole algorithm *)
(* is applied again to the new redex; Step 3) is applied to the result *)
(* of the recursive simplification. Otherwise, if the Fix can not be *)