LAWS.vec_zero: law of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/LAWS.bend as LAWS
Lines 324-325 of bend-osdev-algo@0.1.0.0/LAWS.bend: https://jend.leeeet.dev/read.txt?path=bend-osdev-algo@0.1.0.0/LAWS.bend&start_line=324&end_line=325

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

law vec_zero:
  {(A.bits32.ffs(0), A.bits32.fls(0), A.bits32.ctz(0), A.bits32.clz(0)) == (0n, 0n, 32n, 32n) : Nat & Nat & Nat & Nat}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Pair
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Sigma
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/algo.bend&name=bits32.clz
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/algo.bend&name=bits32.ctz
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/algo.bend&name=bits32.ffs
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/algo.bend&name=bits32.fls