U64.is_zero: def of bend-collections-laws-math@1.0.0.0
Import: import bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend as U64
Lines 150-156 of bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&start_line=150&end_line=156

import Base
import bend-collections-laws-math@1.0.0.0/src/math/u64.bend as U
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend as W
import bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

# THEOREM: is_zero is the specification's zero test.
def is_zero(+a: U.U64) -> {U.is_zero(a) == S.zero(bits(a)) : Bool}:
  match a:
    case U.U64{lo, hi}:
      %Equal.sym(Word(64n), W.pack(0, 0), Word.zero(64n), zero_pack()) : {U.is_zero(U.U64{lo, hi}) == Cmp.is_eq(Word.cmp(64n, W.pack(lo, hi), _)) : Bool}
      %Equal.sym(Cmp, Word.cmp(64n, W.pack(lo, hi), W.pack(0, 0)), U.order(U32.cmp(hi, 0), U32.cmp(lo, 0)), cmp_pack(lo, hi, 0, 0)) : {U.is_zero(U.U64{lo, hi}) == Cmp.is_eq(_) : Bool}
      Equal.sym(Bool, Cmp.is_eq(U.order(U32.cmp(hi, 0), U32.cmp(lo, 0))), Bool.and(Cmp.is_eq(U32.cmp(lo, 0)), Cmp.is_eq(U32.cmp(hi, 0))), eq_order(U32.cmp(hi, 0), U32.cmp(lo, 0)))

Uses (18):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool.and
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Cmp.is_eq
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.cmp
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/lib/lemmas/src/wide.bend&name=pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=bits
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=cmp_pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=eq_order
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/proofs/math/u64/u64.bend&name=zero_pack
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=U64
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=is_zero
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-math@1.0.0.0/src/math/u64.bend&name=order