def andv

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/f64bits.bend:310

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as C
import bend-collections-laws-math@1.0.0.0/proofs/lib/logic.bend as L
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

310def andv(+h: U32, +c: U32, +hc: {c == U32{WD.pw(32n, 31n)} : U32}) -> {v(U32.and(h, c)) == C.shift(31n, C.high(31n, v(h))) : Nat}:
311  L.subst(U32, z => {v(U32.and(h, z)) == C.shift(31n, C.high(31n, v(h))) : Nat}, U32{WD.pw(32n, 31n)}, c, Equal.sym(U32, c, U32{WD.pw(32n, 31n)}, hc), andv0(h))