def bitw.fls_le.h

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

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

374def bitw.fls_le.h(m: Nat, b: Bool, +p: Nat, ih: {Nat.is_le(m, p) == True{} : Bool}) -> {Nat.is_le(A.bitw.fls.step(m, b), 1n+p) == True{} : Bool}:
375  match m:
376    case 0n:
377      match b:
378        case True{}:
379          nat.le_zero(p)
380        case False{}:
381          {==}
382    case 1n+k:
383      ih