fun b_norm_form strat (m, 0) = (m, false)
  | b_norm_form strat (m, i) = if not (has_b_redex m) then (m, true)
                               else b_norm_form strat (strat m, i-1);