def bitw.ffs_set.h

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

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

219def bitw.ffs_set.h(p: Nat, -t: Word(p), m: Nat, ih: {bitw.at1(p, t, m) == nat.pos(m) : Bool}) -> {bitw.at1(1n+p, WCon{False{}, t}, A.bitw.ffs.step(False{}, m)) == nat.pos(A.bitw.ffs.step(False{}, m)) : Bool}:
220  match m:
221    case 0n:
222      {==}
223    case 1n+k:
224      ih