LAWS.vec64_zero: law of bend-osdev-algo@0.1.0.0
Import: import bend-osdev-algo@0.1.0.0/LAWS.bend as LAWS
Lines 336-337 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=336&end_line=337

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

law vec64_zero:
  {(A.bits64.first_set(W.W64.zero()), A.bits64.ctz(W.W64.zero())) == (None{}, 64n) : Maybe<&2, Nat> & Nat}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Maybe
  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=bits64.ctz
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-algo@0.1.0.0/algo.bend&name=bits64.first_set
  https://jend.leeeet.dev/definition.txt?path=bend-osdev-word64@0.1.1.1/word64.bend&name=W64.zero