~/jendhub

def bitw.ctz_ffs

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

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

440def bitw.ctz_ffs(n: Nat, w: Word(n)) -> {A.bitw.ctz(n, w) == bitw.ctz_spec(n, A.bitw.ffs(n, w)) : Nat}:
441  match n:
442    case 0n:
443      {==}
444    case 1n+ +p:
445      match w:
446        case WCon{True{}, t}:
447          {==}
448        case WCon{False{}, +t}:
449          bitw.ctz_ffs.h(p, A.bitw.ctz(p, t), A.bitw.ffs(p, t), bitw.ctz_ffs(p, t))

Uses (8)

Used by (1)