~/jendhub

def wb.mlt

bend-osdev-word64@0.1.1.0 · PROOF_bits.bend:140

import bend-osdev-word64@0.1.1.0/PROOF_bits.bend as PROOFBits
import Base
import bend-osdev-u32@0.1.0.0/u32.bend as U
import bend-osdev-u32@0.1.0.0/LAWS.bend as UL
import bend-osdev-word64@0.1.1.0/proof_value.bend as P

140# nothing is above the mask of all n bits
141def wb.mlt(+n: Nat, +w: Word(n)) -> {Cmp.is_lt(Word.cmp(n, U.U32Word.mask(n, n), w)) == False{} : Bool}:
142  Equal.trans(Bool, Cmp.is_lt(Word.cmp(n, U.U32Word.mask(n, n), w)), Nat.is_lt(Word.to_nat(n, U.U32Word.mask(n, n)), Word.to_nat(n, w)), False{}, Equal.cong(Cmp, Bool, zz => Cmp.is_lt(zz), Word.cmp(n, U.U32Word.mask(n, n), w), Nat.cmp(Word.to_nat(n, U.U32Word.mask(n, n)), Word.to_nat(n, w)), UL.word_cmp_value(n, U.U32Word.mask(n, n), w)), P.wn.le_not_lt(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n)), Equal.trans(Bool, Nat.is_le(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), True{}, Equal.sym(Bool, Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_le(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n))), wb.lts(Word.to_nat(n, w), Word.to_nat(n, U.U32Word.mask(n, n)))), Equal.trans(Bool, Nat.is_lt(Word.to_nat(n, w), 1n+Word.to_nat(n, U.U32Word.mask(n, n))), Nat.is_lt(Word.to_nat(n, w), U.U32Nat.dbl(n, 1n)), True{}, Equal.cong(Nat, Bool, zz => Nat.is_lt(Word.to_nat(n, w), zz), 1n+Word.to_nat(n, U.U32Word.mask(n, n)), U.U32Nat.dbl(n, 1n), UL.word_mask_value(n, n, UL.nat_le_refl(n))), UL.word_value_lt(n, w)))))

Uses (21)

Used by (1)