U32.cmp_bits: law of bend-lawful-stdlib@0.1.0.0
Import: import bend-lawful-stdlib@0.1.0.0/src/u32.bend as U32
Lines 22-29 of bend-lawful-stdlib@0.1.0.0/src/u32.bend: https://jend.leeeet.dev/read.txt?path=bend-lawful-stdlib@0.1.0.0/src/u32.bend&start_line=22&end_line=29

import Base
import bend-lawful-stdlib@0.1.0.0/src/nat.bend as Nat

# comparing bit + 2*rest compares the rests first, then the bits, which is
# what Word.cmp.fin does
law cmp_bits:
  for x: Bool
  for y: Bool
  for a: Nat
  for b: Nat
  {Word.cmp.fin(x, y, Nat.cmp(a, b)) == Nat.cmp(Nat.add(bit(x), Nat.double(a)), Nat.add(bit(y), Nat.double(b))) : Cmp}

Uses (8):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp.fin
  https://jend.leeeet.dev/definition.txt?path=bend-lawful-stdlib@0.1.0.0/src/u32.bend&name=bit