def bitw.ffs_low.z

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

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

237def bitw.ffs_low.z(m: Nat) -> {Bool.and(bitw.below(0n, A.bitw.ffs.step(False{}, m)), False{}) == False{} : Bool}:
238  match m:
239    case 0n:
240      {==}
241    case 1n+k:
242      {==}