def val_lt

bend-collections-laws-math@1.0.0.0 · proofs/math/typed/u32.bend:63

import Base
import bend-collections-laws-math@1.0.0.0/spec/lib/common.bend as SC
import bend-collections-laws-math@1.0.0.0/proofs/lib/u32div.bend as UD
import bend-collections-laws-math@1.0.0.0/proofs/lib/words32.bend as W32
import bend-collections-laws-math@1.0.0.0/proofs/lib/word.bend as WD

63# (one and k stay symbolic, so 2^32 is never expanded)
64def val_lt(+one: Nat, +h1: {one == 1n : Nat}, +k: Nat, +hk: {k == 32n : Nat}, +a: U32) -> {Nat.is_lt(U32.to_nat(a), SC.pow2(k)) == True{} : Bool}:
65  %Equal.sym(Nat, SC.pow2(k), WD.sc(k, one), W32.pow_one(one, h1, k)) : {Nat.is_lt(U32.to_nat(a), _) == True{} : Bool}
66  %Equal.sym(Nat, k, 32n, hk) : {Nat.is_lt(U32.to_nat(a), WD.sc(_, one)) == True{} : Bool}
67  UD.vb(one, h1, a)