def bitw.fls_high.s

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

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

320def bitw.fls_high.s(-p: Nat, -t: Word(p), m: Nat, b: Bool, -j: Nat, ih: {Bool.and(bitw.above(j, m), A.bitw.test(p, t, j)) == False{} : Bool}) -> {Bool.and(bitw.above(1n+j, A.bitw.fls.step(m, b)), A.bitw.test(1n+p, WCon{b, t}, 1n+j)) == False{} : Bool}:
321  match m:
322    case 0n:
323      match b:
324        case True{}:
325          ih
326        case False{}:
327          ih
328    case 1n+k:
329      ih