bend-osdev-u32

Releases (1):
  0.1.0.0  0xab9c812df432dacce3e8b343e9fd7ab7  indexed  https://jend.leeeet.dev/files.txt?path=bend-osdev-u32@0.1.0.0

Definitions (397, 1 to 100 shown):
  LAWS.dbl_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_zero)
   law dbl_zero:
     for +n: Nat
     {U.U32Nat.dbl(n, 0n) == 0n : Nat}
  LAWS.dbl_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_add)
   law dbl_add:
     for +n: Nat
     for +x: Nat
     for +y: Nat
     {U.U32Nat.dbl(n, Nat.add(x, y)) == Nat.add(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) : Nat}
  LAWS.dbl_dbl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_dbl)
   law dbl_dbl:
     for +m: Nat
     for +k: Nat
     for +x: Nat
     {U.U32Nat.dbl(m, U.U32Nat.dbl(k, x)) == U.U32Nat.dbl(Nat.add(m, k), x) : Nat}
  LAWS.dbl_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_lt)
   law dbl_lt:
     for +n: Nat
     for +x: Nat
     for +y: Nat
     {Nat.is_lt(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) == Nat.is_lt(x, y) : Bool}
  LAWS.dbl_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_le)
   law dbl_le:
     for +n: Nat
     for +x: Nat
     for +y: Nat
     {Nat.is_le(U.U32Nat.dbl(n, x), U.U32Nat.dbl(n, y)) == Nat.is_le(x, y) : Bool}
  LAWS.half_double (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=half_double)
   law half_double:
     for +x: Nat
     {U.U32Nat.half(Nat.double(x)) == x : Nat}
  LAWS.half_double_one (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=half_double_one)
   law half_double_one:
     for +x: Nat
     {U.U32Nat.half(1n+Nat.double(x)) == x : Nat}
  LAWS.word_zero_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_zero_value)
   law word_zero_value:
     for +n: Nat
     {Word.to_nat(n, Word.zero(n)) == 0n : Nat}
  LAWS.word_value_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_value_lt)
   law word_value_lt:
     for +n: Nat
     for +w: Word(n)
     {Nat.is_lt(Word.to_nat(n, w), U.U32Nat.dbl(n, 1n)) == True{} : Bool}
  LAWS.word_value_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_value_eq)
   law word_value_eq:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     for e: {Word.to_nat(n, a) == Word.to_nat(n, b) : Nat}
     {a == b : Word(n)}
  LAWS.word_cmp_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_cmp_value)
   law word_cmp_value:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Word.cmp(n, a, b) == Nat.cmp(Word.to_nat(n, a), Word.to_nat(n, b)) : Cmp}
  LAWS.word_not_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_not_value)
   law word_not_value:
     for +n: Nat
     for +w: Word(n)
     {1n+Nat.add(Word.to_nat(n, Word.not(n, w)), Word.to_nat(n, w)) == U.U32Nat.dbl(n, 1n) : Nat}
  LAWS.word_add_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_add_wrap)
   law word_add_wrap:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Nat.add(Word.to_nat(n, Word.add(n, a, b)), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, Word.add(n, a, b), a))))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
  LAWS.word_add_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_add_value)
   law word_add_value:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     for +z: Word(n)
     for h: {Nat.is_le(Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)), Word.to_nat(n, z)) == True{} : Bool}
     {Word.to_nat(n, Word.add(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
  LAWS.word_sub_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_sub_wrap)
   law word_sub_wrap:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Nat.add(Word.to_nat(n, Word.sub(n, a, b)), Word.to_nat(n, b)) == Nat.add(Word.to_nat(n, a), U.U32Nat.dbl(n, U.U32Nat.bit(Cmp.is_lt(Word.cmp(n, a, b))))) : Nat}
  LAWS.word_sub_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_sub_value)
   law word_sub_value:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     for h: {Nat.is_le(Word.to_nat(n, b), Word.to_nat(n, a)) == True{} : Bool}
     {Word.to_nat(n, Word.sub(n, a, b)) == Nat.sub(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
  LAWS.word_inc_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_inc_value)
   law word_inc_value:
     for +n: Nat
     for +w: Word(n)
     for +z: Word(n)
     for h: {Nat.is_le(1n+Word.to_nat(n, w), Word.to_nat(n, z)) == True{} : Bool}
     {Word.to_nat(n, Word.inc(n, w)) == 1n+Word.to_nat(n, w) : Nat}
  LAWS.word_shl_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_shl_value)
   law word_shl_value:
     for +n: Nat
     for +w: Word(n)
     for +z: Word(n)
     for h: {Nat.is_le(Nat.double(Word.to_nat(n, w)), Word.to_nat(n, z)) == True{} : Bool}
     {Word.to_nat(n, Word.shl(n, w)) == Nat.double(Word.to_nat(n, w)) : Nat}
  LAWS.word_shr_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_shr_value)
   law word_shr_value:
     for +n: Nat
     for +w: Word(n)
     {Word.to_nat(n, Word.shr(n, w)) == U.U32Nat.half(Word.to_nat(n, w)) : Nat}
  LAWS.u32_cmp_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_cmp_value)
   law u32_cmp_value:
     for +a: U32
     for +b: U32
     {U32.cmp(a, b) == Nat.cmp(U32.to_nat(a), U32.to_nat(b)) : Cmp}
  LAWS.u32_lt_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_lt_value)
   law u32_lt_value:
     for +a: U32
     for +b: U32
     {U32.is_lt(a, b) == Nat.is_lt(U32.to_nat(a), U32.to_nat(b)) : Bool}
  LAWS.u32_le_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_le_value)
   law u32_le_value:
     for +a: U32
     for +b: U32
     {U32.is_le(a, b) == Nat.is_le(U32.to_nat(a), U32.to_nat(b)) : Bool}
  LAWS.u32_eq_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_eq_value)
   law u32_eq_value:
     for +a: U32
     for +b: U32
     {U32.is_eq(a, b) == Nat.is_eq(U32.to_nat(a), U32.to_nat(b)) : Bool}
  LAWS.u32_value_eq (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_value_eq)
   law u32_value_eq:
     for +a: U32
     for +b: U32
     for e: {U32.to_nat(a) == U32.to_nat(b) : Nat}
     {a == b : U32}
  LAWS.u32_add_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_add_wrap)
   law u32_add_wrap:
     for +a: U32
     for +b: U32
     {Nat.add(U32.to_nat(U32.add(a, b)), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(U32.add(a, b), a)))) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWS.u32_add_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_add_value)
   law u32_add_value:
     for +a: U32
     for +b: U32
     for +c: U32
     for h: {Nat.is_le(Nat.add(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(c)) == True{} : Bool}
     {U32.to_nat(U32.add(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWS.u32_sub_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_sub_wrap)
   law u32_sub_wrap:
     for +a: U32
     for +b: U32
     {Nat.add(U32.to_nat(U32.sub(a, b)), U32.to_nat(b)) == Nat.add(U32.to_nat(a), U.U32Nat.dbl(32n, U.U32Nat.bit(U32.is_lt(a, b)))) : Nat}
  LAWS.u32_sub_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_sub_value)
   law u32_sub_value:
     for +a: U32
     for +b: U32
     for h: {Nat.is_le(U32.to_nat(b), U32.to_nat(a)) == True{} : Bool}
     {U32.to_nat(U32.sub(a, b)) == Nat.sub(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWS.u32_inc_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_inc_value)
   law u32_inc_value:
     for +a: U32
     for +c: U32
     for h: {Nat.is_le(1n+U32.to_nat(a), U32.to_nat(c)) == True{} : Bool}
     {U32.to_nat(U32.inc(a)) == 1n+U32.to_nat(a) : Nat}
  LAWS.u32_shl_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_shl_value)
   law u32_shl_value:
     for +a: U32
     for +c: U32
     for h: {Nat.is_le(Nat.double(U32.to_nat(a)), U32.to_nat(c)) == True{} : Bool}
     {U32.to_nat(U32.shl(a)) == Nat.double(U32.to_nat(a)) : Nat}
  LAWS.u32_shln_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_shln_value)
   law u32_shln_value:
     for +a: U32
     for +k: Nat
     for +c: U32
     for +h: {Nat.is_le(U.U32Nat.dbl(k, U32.to_nat(a)), U32.to_nat(c)) == True{} : Bool}
     {U32.to_nat(U32.shln(a, k)) == U.U32Nat.dbl(k, U32.to_nat(a)) : Nat}
  LAWS.u32_shr_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_shr_value)
   law u32_shr_value:
     for +a: U32
     {U32.to_nat(U32.shr(a)) == U.U32Nat.half(U32.to_nat(a)) : Nat}
  LAWS.u32_wit (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_wit)
   # the bounds can hold, and the wrapping cases happen: 2^32 - 1 + 1 wraps to
   # 0, below the first operand; 0 - 1 borrows
   law u32_wit:
     {(Nat.is_le(Nat.add(U32.to_nat(3), U32.to_nat(4)), U32.to_nat(7)), U32.is_lt(U32.add(4294967295, 1), 4294967295), U32.is_lt(0, 1), U32.add(4294967295, 1), U32.sub(0, 1)) == (True{}, True{}, True{}, 0, 4294967295) : Bool & Bool & Bool & U32 & U32}
  LAWS.dbl_vec (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_vec)
   law dbl_vec:
     {(U.U32Nat.dbl(3n, 5n), U.U32Nat.bit(True{}), U.U32Nat.half(7n)) == (40n, 1n, 3n) : Nat & Nat & Nat}
  LAWS.nat_add_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_zero)
   law nat_add_zero:
     for +x: Nat
     {Nat.add(x, 0n) == x : Nat}
  LAWS.nat_add_succ (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_succ)
   law nat_add_succ:
     for +x: Nat
     for +y: Nat
     {Nat.add(x, 1n+y) == 1n+Nat.add(x, y) : Nat}
  LAWS.nat_add_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_comm)
   law nat_add_comm:
     for +x: Nat
     for +y: Nat
     {Nat.add(x, y) == Nat.add(y, x) : Nat}
  LAWS.nat_add_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_assoc)
   law nat_add_assoc:
     for +x: Nat
     for +y: Nat
     for +z: Nat
     {Nat.add(Nat.add(x, y), z) == Nat.add(x, Nat.add(y, z)) : Nat}
  LAWS.nat_add_left_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_left_comm)
   law nat_add_left_comm:
     for +x: Nat
     for +y: Nat
     for +z: Nat
     {Nat.add(x, Nat.add(y, z)) == Nat.add(y, Nat.add(x, z)) : Nat}
  LAWS.nat_add_cancel (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_cancel)
   law nat_add_cancel:
     for +k: Nat
     for +x: Nat
     for +y: Nat
     for e: {Nat.add(k, x) == Nat.add(k, y) : Nat}
     {x == y : Nat}
  LAWS.nat_mul_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_mul_zero)
   law nat_mul_zero:
     for +x: Nat
     {Nat.mul(x, 0n) == 0n : Nat}
  LAWS.nat_mul_one (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_mul_one)
   law nat_mul_one:
     for +x: Nat
     {Nat.mul(x, 1n) == x : Nat}
  LAWS.nat_one_mul (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_one_mul)
   law nat_one_mul:
     for +x: Nat
     {Nat.mul(1n, x) == x : Nat}
  LAWS.nat_mul_succ (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_mul_succ)
   law nat_mul_succ:
     for +x: Nat
     for +y: Nat
     {Nat.mul(x, 1n+y) == Nat.add(x, Nat.mul(x, y)) : Nat}
  LAWS.nat_mul_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_mul_comm)
   law nat_mul_comm:
     for +x: Nat
     for +y: Nat
     {Nat.mul(x, y) == Nat.mul(y, x) : Nat}
  LAWS.nat_mul_assoc (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_mul_assoc)
   law nat_mul_assoc:
     for +x: Nat
     for +y: Nat
     for +z: Nat
     {Nat.mul(Nat.mul(x, y), z) == Nat.mul(x, Nat.mul(y, z)) : Nat}
  LAWS.nat_mul_left_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_mul_left_comm)
   law nat_mul_left_comm:
     for +x: Nat
     for +y: Nat
     for +z: Nat
     {Nat.mul(x, Nat.mul(y, z)) == Nat.mul(y, Nat.mul(x, z)) : Nat}
  LAWS.nat_mul_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_mul_add)
   law nat_mul_add:
     for +x: Nat
     for +y: Nat
     for +z: Nat
     {Nat.mul(x, Nat.add(y, z)) == Nat.add(Nat.mul(x, y), Nat.mul(x, z)) : Nat}
  LAWS.nat_add_mul (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_add_mul)
   law nat_add_mul:
     for +x: Nat
     for +y: Nat
     for +z: Nat
     {Nat.mul(Nat.add(x, y), z) == Nat.add(Nat.mul(x, z), Nat.mul(y, z)) : Nat}
  LAWS.nat_double (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_double)
   law nat_double:
     for +x: Nat
     {Nat.double(x) == Nat.add(x, x) : Nat}
  LAWS.dbl_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_comm)
   law dbl_comm:
     for +j: Nat
     for +k: Nat
     for +x: Nat
     {U.U32Nat.dbl(j, U.U32Nat.dbl(k, x)) == U.U32Nat.dbl(k, U.U32Nat.dbl(j, x)) : Nat}
  LAWS.dbl_mul_l (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_mul_l)
   law dbl_mul_l:
     for +k: Nat
     for +x: Nat
     for +y: Nat
     {Nat.mul(U.U32Nat.dbl(k, x), y) == U.U32Nat.dbl(k, Nat.mul(x, y)) : Nat}
  LAWS.dbl_mul_r (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_mul_r)
   law dbl_mul_r:
     for +k: Nat
     for +x: Nat
     for +y: Nat
     {Nat.mul(x, U.U32Nat.dbl(k, y)) == U.U32Nat.dbl(k, Nat.mul(x, y)) : Nat}
  LAWS.nat_le_refl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_refl)
   law nat_le_refl:
     for +x: Nat
     {Nat.is_le(x, x) == True{} : Bool}
  LAWS.nat_le_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_add)
   law nat_le_add:
     for +x: Nat
     for +w: Nat
     {Nat.is_le(x, Nat.add(w, x)) == True{} : Bool}
  LAWS.nat_lt_add (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_add)
   law nat_lt_add:
     for +x: Nat
     for +w: Nat
     {Nat.is_lt(x, Nat.add(w, 1n+x)) == True{} : Bool}
  LAWS.nat_le_witness (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_le_witness)
   law nat_le_witness:
     for +x: Nat
     for +y: Nat
     for h: {Nat.is_le(x, y) == True{} : Bool}
     {Nat.add(Nat.sub(y, x), x) == y : Nat}
  LAWS.nat_lt_witness (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_lt_witness)
   law nat_lt_witness:
     for +x: Nat
     for +y: Nat
     for h: {Nat.is_lt(x, y) == True{} : Bool}
     {Nat.add(Nat.sub(y, 1n+x), 1n+x) == y : Nat}
  LAWS.nat_succ_add_absurd (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_succ_add_absurd)
   law nat_succ_add_absurd:
     for +w: Nat
     for +x: Nat
     for e: {Nat.add(w, 1n+x) == x : Nat}
     Empty
  LAWS.nat_div_unique (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_div_unique)
   law nat_div_unique:
     for +b: Nat
     for +q1: Nat
     for +r1: Nat
     for +q2: Nat
     for +r2: Nat
     for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
     for h1: {Nat.is_lt(r1, b) == True{} : Bool}
     for h2: {Nat.is_lt(r2, b) == True{} : Bool}
     {q1 == q2 : Nat}
  LAWS.nat_mod_unique (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_mod_unique)
   law nat_mod_unique:
     for +b: Nat
     for +q1: Nat
     for +r1: Nat
     for +q2: Nat
     for +r2: Nat
     for e: {Nat.add(Nat.mul(q1, b), r1) == Nat.add(Nat.mul(q2, b), r2) : Nat}
     for h1: {Nat.is_lt(r1, b) == True{} : Bool}
     for h2: {Nat.is_lt(r2, b) == True{} : Bool}
     {r1 == r2 : Nat}
  LAWS.dbl_nowrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=dbl_nowrap)
   law dbl_nowrap:
     for +n: Nat
     for +k: Nat
     for +r: Nat
     for +p: Nat
     for +z: Nat
     for e: {Nat.add(r, U.U32Nat.dbl(n, k)) == p : Nat}
     for h: {Nat.is_le(p, z) == True{} : Bool}
     for hz: {Nat.is_lt(z, U.U32Nat.dbl(n, 1n)) == True{} : Bool}
     {r == p : Nat}
  LAWS.nat_odd_half (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_odd_half)
   law nat_odd_half:
     for +x: Nat
     {Nat.add(U.U32Nat.odd(x), Nat.double(U.U32Nat.half(x))) == x : Nat}
  LAWS.nat_odd_le (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=nat_odd_le)
   law nat_odd_le:
     for +x: Nat
     {Nat.is_le(U.U32Nat.odd(x), 1n) == True{} : Bool}
  LAWS.low_high (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_high)
   law low_high:
     for +k: Nat
     for +x: Nat
     {Nat.add(U.U32Nat.low(k, x), U.U32Nat.dbl(k, U.U32Nat.high(k, x))) == x : Nat}
  LAWS.low_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_lt)
   law low_lt:
     for +k: Nat
     for +x: Nat
     {Nat.is_lt(U.U32Nat.low(k, x), U.U32Nat.dbl(k, 1n)) == True{} : Bool}
  LAWS.low_unique (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_unique)
   law low_unique:
     for +k: Nat
     for +x: Nat
     for +r: Nat
     for +q: Nat
     for e: {Nat.add(r, U.U32Nat.dbl(k, q)) == x : Nat}
     for h: {Nat.is_lt(r, U.U32Nat.dbl(k, 1n)) == True{} : Bool}
     {r == U.U32Nat.low(k, x) : Nat}
  LAWS.high_unique (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=high_unique)
   law high_unique:
     for +k: Nat
     for +x: Nat
     for +r: Nat
     for +q: Nat
     for e: {Nat.add(r, U.U32Nat.dbl(k, q)) == x : Nat}
     for h: {Nat.is_lt(r, U.U32Nat.dbl(k, 1n)) == True{} : Bool}
     {q == U.U32Nat.high(k, x) : Nat}
  LAWS.low_add_dbl (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_add_dbl)
   law low_add_dbl:
     for +k: Nat
     for +x: Nat
     for +q: Nat
     {U.U32Nat.low(k, Nat.add(x, U.U32Nat.dbl(k, q))) == U.U32Nat.low(k, x) : Nat}
  LAWS.low_small (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=low_small)
   law low_small:
     for +k: Nat
     for +x: Nat
     for h: {Nat.is_lt(x, U.U32Nat.dbl(k, 1n)) == True{} : Bool}
     {U.U32Nat.low(k, x) == x : Nat}
  LAWS.word_mul_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_mul_wrap)
   law word_mul_wrap:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Nat.add(Word.to_nat(n, Word.mul(n, a, b)), U.U32Nat.dbl(n, U.U32Nat.high(n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))))) == Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
  LAWS.word_mul_low (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_mul_low)
   law word_mul_low:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Word.to_nat(n, Word.mul(n, a, b)) == U.U32Nat.low(n, Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b))) : Nat}
  LAWS.word_mul_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_mul_value)
   law word_mul_value:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     for +z: Word(n)
     for h: {Nat.is_le(Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)), Word.to_nat(n, z)) == True{} : Bool}
     {Word.to_nat(n, Word.mul(n, a, b)) == Nat.mul(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
  LAWS.u32_mul_wrap (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_mul_wrap)
   law u32_mul_wrap:
     for +a: U32
     for +b: U32
     {Nat.add(U32.to_nat(U32.mul(a, b)), U.U32Nat.dbl(32n, U.U32Nat.high(32n, Nat.mul(U32.to_nat(a), U32.to_nat(b))))) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWS.u32_mul_low (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_mul_low)
   law u32_mul_low:
     for +a: U32
     for +b: U32
     {U32.to_nat(U32.mul(a, b)) == U.U32Nat.low(32n, Nat.mul(U32.to_nat(a), U32.to_nat(b))) : Nat}
  LAWS.u32_mul_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_mul_value)
   law u32_mul_value:
     for +a: U32
     for +b: U32
     for +c: U32
     for h: {Nat.is_le(Nat.mul(U32.to_nat(a), U32.to_nat(b)), U32.to_nat(c)) == True{} : Bool}
     {U32.to_nat(U32.mul(a, b)) == Nat.mul(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWS.u32_divmod (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_divmod)
   law u32_divmod:
     for +a: U32
     for +b: U32
     for h: {U32.is_zero(b) == False{} : Bool}
     {Nat.add(Nat.mul(U32.to_nat(U32.div(a, b)), U32.to_nat(b)), U32.to_nat(U32.mod(a, b))) == U32.to_nat(a) : Nat}
  LAWS.u32_mod_lt (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_mod_lt)
   law u32_mod_lt:
     for +a: U32
     for +b: U32
     for h: {U32.is_zero(b) == False{} : Bool}
     {Nat.is_lt(U32.to_nat(U32.mod(a, b)), U32.to_nat(b)) == True{} : Bool}
  LAWS.u32_div_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_div_zero)
   law u32_div_zero:
     for +a: U32
     {U32.div(a, 0) == 0 : U32}
  LAWS.u32_mod_zero (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_mod_zero)
   law u32_mod_zero:
     for +a: U32
     {U32.mod(a, 0) == a : U32}
  LAWS.word_and_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_and_comm)
   law word_and_comm:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Word.and(n, a, b) == Word.and(n, b, a) : Word(n)}
  LAWS.word_or_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_or_comm)
   law word_or_comm:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Word.or(n, a, b) == Word.or(n, b, a) : Word(n)}
  LAWS.word_xor_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_xor_comm)
   law word_xor_comm:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Word.xor(n, a, b) == Word.xor(n, b, a) : Word(n)}
  LAWS.word_and_or (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_and_or)
   law word_and_or:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Nat.add(Word.to_nat(n, Word.and(n, a, b)), Word.to_nat(n, Word.or(n, a, b))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
  LAWS.word_xor_and (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_xor_and)
   law word_xor_and:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     {Nat.add(Word.to_nat(n, Word.xor(n, a, b)), Nat.double(Word.to_nat(n, Word.and(n, a, b)))) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
  LAWS.word_or_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_or_split)
   law word_or_split:
     for +n: Nat
     for +a: Word(n)
     for +b: Word(n)
     for +k: Nat
     for +q: Nat
     for e: {Word.to_nat(n, a) == U.U32Nat.dbl(k, q) : Nat}
     for h: {Nat.is_lt(Word.to_nat(n, b), U.U32Nat.dbl(k, 1n)) == True{} : Bool}
     {Word.to_nat(n, Word.or(n, a, b)) == Nat.add(Word.to_nat(n, a), Word.to_nat(n, b)) : Nat}
  LAWS.word_mask_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_mask_value)
   law word_mask_value:
     for +n: Nat
     for +k: Nat
     for h: {Nat.is_le(k, n) == True{} : Bool}
     {1n+Word.to_nat(n, U.U32Word.mask(n, k)) == U.U32Nat.dbl(k, 1n) : Nat}
  LAWS.word_and_mask (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_and_mask)
   law word_and_mask:
     for +n: Nat
     for +w: Word(n)
     for +m: Word(n)
     for +k: Nat
     for h: {1n+Word.to_nat(n, m) == U.U32Nat.dbl(k, 1n) : Nat}
     {Word.to_nat(n, Word.and(n, w, m)) == U.U32Nat.low(k, Word.to_nat(n, w)) : Nat}
  LAWS.word_not_sub (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=word_not_sub)
   law word_not_sub:
     for +n: Nat
     for +w: Word(n)
     {Word.not(n, w) == Word.sub(n, U.U32Word.mask(n, n), w) : Word(n)}
  LAWS.u32_and_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_and_comm)
   law u32_and_comm:
     for +a: U32
     for +b: U32
     {U32.and(a, b) == U32.and(b, a) : U32}
  LAWS.u32_or_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_or_comm)
   law u32_or_comm:
     for +a: U32
     for +b: U32
     {U32.or(a, b) == U32.or(b, a) : U32}
  LAWS.u32_xor_comm (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_xor_comm)
   law u32_xor_comm:
     for +a: U32
     for +b: U32
     {U32.xor(a, b) == U32.xor(b, a) : U32}
  LAWS.u32_and_or (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_and_or)
   law u32_and_or:
     for +a: U32
     for +b: U32
     {Nat.add(U32.to_nat(U32.and(a, b)), U32.to_nat(U32.or(a, b))) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWS.u32_xor_and (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_xor_and)
   law u32_xor_and:
     for +a: U32
     for +b: U32
     {Nat.add(U32.to_nat(U32.xor(a, b)), Nat.double(U32.to_nat(U32.and(a, b)))) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWS.u32_or_split (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_or_split)
   law u32_or_split:
     for +a: U32
     for +b: U32
     for +k: Nat
     for +q: Nat
     for e: {U32.to_nat(a) == U.U32Nat.dbl(k, q) : Nat}
     for h: {Nat.is_lt(U32.to_nat(b), U.U32Nat.dbl(k, 1n)) == True{} : Bool}
     {U32.to_nat(U32.or(a, b)) == Nat.add(U32.to_nat(a), U32.to_nat(b)) : Nat}
  LAWS.u32_and_mask (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_and_mask)
   law u32_and_mask:
     for +a: U32
     for +m: U32
     for +k: Nat
     for h: {1n+U32.to_nat(m) == U.U32Nat.dbl(k, 1n) : Nat}
     {U32.to_nat(U32.and(a, m)) == U.U32Nat.low(k, U32.to_nat(a)) : Nat}
  LAWS.u32_and_65535 (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_and_65535)
   # the 16-bit mask, written as Base reads it (65535 = U32Word.mask(32, 16))
   law u32_and_65535:
     for +a: U32
     {U32.to_nat(U32.and(a, 65535)) == U.U32Nat.low(16n, U32.to_nat(a)) : Nat}
  LAWS.u32_not_sub (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_not_sub)
   law u32_not_sub:
     for +a: U32
     {U32.not(a) == U32.sub(4294967295, a) : U32}
  LAWS.u32_shrn_value (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_shrn_value)
   law u32_shrn_value:
     for +a: U32
     for +k: Nat
     {U32.to_nat(U32.shrn(a, k)) == U.U32Nat.high(k, U32.to_nat(a)) : Nat}
  LAWS.u32_shln_low (https://jend.leeeet.dev/definition.txt?path=bend-osdev-u32@0.1.0.0/LAWS.bend&name=u32_shln_low)
   law u32_shln_low:
     for +a: U32
     for +k: Nat
     {U32.to_nat(U32.shln(a, k)) == U.U32Nat.low(32n, U.U32Nat.dbl(k, U32.to_nat(a))) : Nat}
More: https://jend.leeeet.dev/packages/bend-osdev-u32.txt?definitions_offset=100