def bitw.ffs_le_fls.f

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

import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A

394# ffs <= fls
395def bitw.ffs_le_fls.f(a: Nat, m: Nat, ih: {Nat.is_le(a, m) == True{} : Bool}) -> {Nat.is_le(A.bitw.ffs.step(False{}, a), A.bitw.fls.step(m, False{})) == True{} : Bool}:
396  match a m:
397    case 0n _:
398      nat.le_zero(A.bitw.fls.step(m, False{}))
399    case 1n+i 0n:
400      Empty.absurd({Nat.is_le(2n+i, 0n) == True{} : Bool}, absurd.ft(ih))
401    case 1n+i 1n+k:
402      ih