Word.and_zero: def of bend-collections-laws-crypto@1.0.0.0
Import: import bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend as Word
Lines 271-277 of bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend: https://jend.leeeet.dev/read.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&start_line=271&end_line=277

import Base
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend as S

def and_zero(+p: Nat, +t: Word(p)) -> {uw(p, Word.and(p, t, mask(p, 0n))) == 0n : Nat}:
  match p t:
    case 0n WNil{}:
      {==}
    case 1n+q WCon{b, s}:
      %Equal.sym(Nat, S.bit_value(Bool.and(b, False{})), 0n, and_false_bv(b)) : {Nat.add(_, Nat.double(uw(q, Word.and(q, s, mask(q, 0n))))) == 0n : Nat}
      Equal.cong(Nat, Nat, z => Nat.double(z), uw(q, Word.and(q, s, mask(q, 0n))), 0n, and_zero(q, s))

Uses (15):
  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=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.and
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/lemmas/spec/numeric.bend&name=bit_value
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=and_false_bv
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=mask
  https://jend.leeeet.dev/definition.txt?path=bend-collections-laws-crypto@1.0.0.0/proofs/lib/word.bend&name=uw