~/jendhub

def uand_all

bend-collections-laws-math@1.0.0.0 · proofs/math/random/uint64n.bend:276

import bend-collections-laws-math@1.0.0.0/proofs/math/random/uint64n.bend as Uint64n
import Base

276def uand_all(+y: U32, +M: U32, +hM: {M == U32{all1(32n)} : U32}) -> {U32.and(y, M) == y : U32}:
277  match y:
278    case U32{+w}:
279      %Equal.sym(U32, M, U32{all1(32n)}, hM) : {U32.and(U32{w}, _) == U32{w} : U32}
280      Equal.cong(Word(32n), U32, z => U32{z}, Word.and(32n, w, all1(32n)), w, and_all1(32n, w))

Uses (8)

Used by (1)