in reduce_try2 t''
else t'
-let rec reduce_lazy (t:term):term = match t with
+let rec reduce_try3 (t:term):term = match t with
| I -> I
| K -> K
| S -> S
| App (a, b) ->
- let t' = App (reduce_lazy a, b) in
+ let t' = App (reduce_try3 a, b) in
if (is_redex t') then let t'' = reduce_if_redex t'
- in reduce_lazt t''
+ in reduce_try3 t''
else t'