def ba.jz_eq

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

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

1286# after a halving that keeps the upper half: hi - (mid + 1) is
1287# (hi - lo) - (1 + (hi - lo) / 2)
1288def ba.jz_eq(+lo: U32, +hi: U32, eI: {U32.to_nat(U32.inc(Q.bq.mid(lo, hi))) == 1n+Q.bq.m(lo, hi) : Nat}, ehs: {Nat.add(U32.to_nat(lo), Q.bq.s(lo, hi)) == U32.to_nat(hi) : Nat}) -> {Nat.sub(Q.bq.s(lo, hi), 1n+U.uq.half(Q.bq.s(lo, hi))) == Q.bq.s(U32.inc(Q.bq.mid(lo, hi)), hi) : Nat}:
1289  +l0 = U32.to_nat(lo)
1290  +s = Q.bq.s(lo, hi)
1291  +hs = U.uq.half(s)
1292  +m = Q.bq.m(lo, hi)
1293  %Equal.sym(Nat, U32.to_nat(U32.inc(Q.bq.mid(lo, hi))), 1n+m, eI) : {Nat.sub(s, 1n+hs) == Nat.sub(U32.to_nat(hi), _) : Nat}
1294  %ehs : {Nat.sub(s, 1n+hs) == Nat.sub(_, 1n+m) : Nat}
1295  %U.uq.add_succ(l0, hs) : {Nat.sub(s, 1n+hs) == Nat.sub(Nat.add(l0, s), _) : Nat}
1296  Equal.sym(Nat, Nat.sub(Nat.add(l0, s), Nat.add(l0, 1n+hs)), Nat.sub(s, 1n+hs), Q.bq.sub_cancel(l0, s, 1n+hs))