~/jendhub

def bitw.fls_set.h

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

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

289def bitw.fls_set.h(p: Nat, -t: Word(p), m: Nat, b: Bool, ih: {bitw.at1(p, t, m) == nat.pos(m) : Bool}) -> {bitw.at1(1n+p, WCon{b, t}, A.bitw.fls.step(m, b)) == nat.pos(A.bitw.fls.step(m, b)) : Bool}:
290  match m:
291    case 0n:
292      match b:
293        case True{}:
294          {==}
295        case False{}:
296          {==}
297    case 1n+k:
298      ih

Uses (7)

Used by (1)