def bq.hr_lt_pw

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

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

385# s < 2p: s - (1 + s / 2) < p
386def bq.hr_lt_pw(s: Nat, p: Nat, h: {Nat.is_lt(s, Nat.double(p)) == True{} : Bool}) -> {Nat.is_lt(Nat.sub(s, 1n+U.uq.half(s)), p) == True{} : Bool}:
387  match s:
388    case 0n:
389      match p:
390        case 0n:
391          Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
392        case 1n+pp:
393          {==}
394    case 1n+sp:
395      match sp:
396        case 0n:
397          match p:
398            case 0n:
399              Empty.absurd({Nat.is_lt(0n, 0n) == True{} : Bool}, bq.ft(h))
400            case 1n+pp:
401              {==}
402        case 1n+ +q:
403          match p:
404            case 0n:
405              Empty.absurd({Nat.is_lt(Nat.sub(q, U.uq.half(q)), 0n) == True{} : Bool}, bq.ft(h))
406            case 1n+ +pp:
407              U.uq.le_lt_trans(Nat.sub(q, U.uq.half(q)), 1n+Nat.sub(q, 1n+U.uq.half(q)), 1n+pp, bq.sub_step(q, U.uq.half(q)), bq.hr_lt_pw(q, pp, h))