~/jendhub

def bitw.ffs_low.s

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

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

244def bitw.ffs_low.s(-p: Nat, -t: Word(p), m: Nat, -j: Nat, ih: {Bool.and(bitw.below(j, m), A.bitw.test(p, t, j)) == False{} : Bool}) -> {Bool.and(bitw.below(1n+j, A.bitw.ffs.step(False{}, m)), A.bitw.test(1n+p, WCon{False{}, t}, 1n+j)) == False{} : Bool}:
245  match m:
246    case 0n:
247      ih
248    case 1n+k:
249      ih

Uses (8)

Used by (1)