def ba.hz33

bend-osdev-algo@0.1.0.0 · PROOF.bend:1365

import Base
import bend-osdev-algo@0.1.0.0/proof_u32.bend as U
import bend-osdev-algo@0.1.0.0/proof_bsearch.bend as Q

1365# n < 2^32 < 2^33: the 33 halvings suffice (stated so that 2^33 is never
1366# expanded)
1367def ba.hz33(n: U32) -> {Nat.is_lt(Q.bq.s(0, n), U.uq.pw(33n)) == True{} : Bool}:
1368  match n:
1369    case U32{+w}:
1370      U.uq.lt_succ_pw(32n, 33n, {==}, Word.to_nat(32n, w), Q.bq.s(0, U32{w}), Equal.sym(Nat, Nat.sub(Word.to_nat(32n, w), 0n), Word.to_nat(32n, w), Q.bq.sub_zero(Word.to_nat(32n, w))), U.uq.val_lt(32n, w))