def and_zero

bend-collections-laws-crypto@1.0.0.0 · proofs/lib/word.bend:271

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

271def and_zero(+p: Nat, +t: Word(p)) -> {uw(p, Word.and(p, t, mask(p, 0n))) == 0n : Nat}:
272  match p t:
273    case 0n WNil{}:
274      {==}
275    case 1n+q WCon{b, s}:
276      %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}
277      Equal.cong(Nat, Nat, z => Nat.double(z), uw(q, Word.and(q, s, mask(q, 0n))), 0n, and_zero(q, s))