def max_val

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

import Base
import bend-collections-laws-crypto@1.0.0.0/src/math/generic.bend as G
import bend-collections-laws-crypto@1.0.0.0/src/math/instances.bend as I
import bend-collections-laws-crypto@1.0.0.0/proofs/lib/u32.bend as U

163# the value of max(x, lo) is the larger value
164def max_val(+x: U32, +lo: U32) -> {U32.to_nat(G.max(~U32, ~I.u32_op, ~I.u32_is, x, lo)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}:
165  %Equal.sym(Bool, U32.is_lt(x, lo), Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)), U.is_lt_nat(x, lo)) : {U32.to_nat(G.pick(U32, _, lo, x)) == Nat.max(U32.to_nat(x), U32.to_nat(lo)) : Nat}
166  max_val_c(x, lo, Nat.is_lt(U32.to_nat(x), U32.to_nat(lo)), {==})