def bq.half_lt_pw

bend-osdev-algo@0.1.0.0 · proof_bsearch.bend:361

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

361# s < 2p: s / 2 < p
362def bq.half_lt_pw(s: Nat, p: Nat, h: {Nat.is_lt(s, Nat.double(p)) == True{} : Bool}) -> {Nat.is_lt(U.uq.half(s), p) == True{} : Bool}:
363  match s:
364    case 0n:
365      match p:
366        case 0n:
367          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
368        case 1n+pp:
369          {==}
370    case 1n+sp:
371      match sp:
372        case 0n:
373          match p:
374            case 0n:
375              Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
376            case 1n+pp:
377              {==}
378        case 1n+q:
379          match p:
380            case 0n:
381              Empty.absurd({Nat.is_lt(1n+U.uq.half(q), 0n) == True{} : Bool}, bq.ft(h))
382            case 1n+pp:
383              bq.half_lt_pw(q, pp, h)