432 unfolding numeral_simps by simp
433
434 lemmas normalize_bin_simps =
435 Bit0_Pls Bit1_Min
436 *)
437
438 end