def bitw.ctz_ffs.h

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

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

431def bitw.ctz_ffs.h(+p: Nat, c: Nat, m: Nat, ih: {c == bitw.ctz_spec(p, m) : Nat}) -> {1n+c == bitw.ctz_spec(1n+p, A.bitw.ffs.step(False{}, m)) : Nat}:
432  match m:
433    case 0n:
434      %ih : {1n+c == 1n+_ : Nat}
435      {==}
436    case 1n+k:
437      %ih : {1n+c == 1n+_ : Nat}
438      {==}