lawful-words
Releases (1)
-
0.1.0.0 indexed
Definitions (468)
proof_u32.bend
- law wmul.m
- law wsub_val.m
- law to_nat_lt.m
- law to_nat_lt_p
- law to_nat_inj
- law wrap_small_p
- law to_nat_inc.m
- law to_nat_inc_p
- law to_nat_from_nat.m
- law to_nat_from_nat_p
- law from_nat_to_nat.m
- law from_nat_to_nat
- law cmp_to_nat
- law is_eq_to_nat
- law is_lt_to_nat
- law is_le_to_nat
- law is_gt_to_nat
- law is_ge_to_nat
- law is_ne_to_nat
- law is_zero_to_nat
- law is_eq_true
- law fin_eq
- law xor_bit_eq
- law wxor_zero
- law is_zero_xor
- law to_nat_add.m
- law to_nat_add_p
- law to_nat_sub.m
- law to_nat_sub_p
- law to_nat_mul.m
- law to_nat_mul_p
- law from_nat_add.m
- law from_nat_add
- law from_nat_mul.m
- law from_nat_mul
- law to_nat_inc_lt.m
- law to_nat_inc_lt
- law to_nat_add_fits_p
- law to_nat_mul_fits_p
- law sub_add_comm(x + m) - y = (x - y) + m for y <= x.
- law sub_le
- law mod_add_self
- law to_nat_sub_le.m
- law to_nat_sub_le
- law shl_out
- def DMOKWhat U32.divmod.go(k, a, b) returns: q * b + r = a and r < b.
- law divstep1One step of long division, as numbers (quotient bit 1, then 0).
- law divstep0
- law lt_add_cancel_l
- law sub_lt_dblx < 2b and b <= x give x - b < b.
- law ge_le
- def dm_fin.tThe quotient bit is 1: the remainder becomes 2r + a0 - b.
- def dm_rec
- law dm_ok
- def div_fin_ok
- def mod_fin_ok
- law ne_zero_pos
- def div_if_ok
- def mod_if_ok
- law to_nat_div
- law to_nat_mod
- law min_lt
- law min_nlt
- law max_lt
- law max_nlt
- def min_ok
- def max_ok
- law to_nat_min
- law to_nat_max
- law to_nat_shr
- law to_nat_shl.m
- law to_nat_shl_p
- law to_nat_shrn
- law to_nat_shln.m
- law to_nat_shln_p
- law to_nat_shln_fits_p
- def shln_mod.go
- law to_nat_shln_mod.m
- law to_nat_shln_mod
- law to_nat_shrn_lt.m
- law to_nat_shrn_lt
- law to_nat_and_mask
- law to_nat_not.m
- law to_nat_not_p
- law to_nat_or_split
- law to_nat_xor_split
- law to_nat_split
- law shrn_lt_words
- law bitw
- law bit_and
- law bit_or
- law bit_xor
- law bit_not
- law bit_ext
proof_word.bend
- law wconThe value of a word with head bit b and tail t.
- law bn_lt2
- law wcon2The same value as t * 2 + b.
- law lt_dbl_bitb + 2x < 2y when x < y.
- law lt_dbl_invb + 2x < 2y gives x < y.
- law moddbl(b + 2x) % 2q = b + 2 (x % q).