def bitw.ffs_le_fls
bend-osdev-algo@0.1.0.0 · PROOF.bend:411
import bend-osdev-algo@0.1.0.0/PROOF.bend as PROOF
import Base
import bend-osdev-algo@0.1.0.0/algo.bend as A
411def bitw.ffs_le_fls(n: Nat, w: Word(n)) -> {Nat.is_le(A.bitw.ffs(n, w), A.bitw.fls(n, w)) == True{} : Bool}:
412 match n:
413 case 0n:
414 {==}
415 case 1n+ +p:
416 match w:
417 case WCon{True{}, t}:
418 bitw.ffs_le_fls.t(A.bitw.fls(p, t))
419 case WCon{False{}, +t}:
420 bitw.ffs_le_fls.f(A.bitw.ffs(p, t), A.bitw.fls(p, t), bitw.ffs_le_fls(p, t))