def uq.hk0

bend-osdev-algo@0.1.0.0 · proof_u32.bend:397

import Base

397# the bound for the bits above the lowest, from the bound for the word
398def uq.hk0(+s2: Nat, -d: Nat, +q: Nat, e: {Nat.double(s2) == d : Nat}, h: {Nat.is_lt(d, Nat.double(q)) == True{} : Bool}) -> {Nat.is_lt(s2, q) == True{} : Bool}:
399  Equal.trans(Bool, Nat.is_lt(s2, q), Nat.is_lt(Nat.double(s2), Nat.double(q)), True{}, Equal.sym(Bool, Nat.is_lt(Nat.double(s2), Nat.double(q)), Nat.is_lt(s2, q), uq.lt_dbl(s2, q)), uq.lt_rw(d, Nat.double(s2), Nat.double(q), Equal.sym(Nat, Nat.double(s2), d, e), h))