def bitw.first_le_last

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

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

507def bitw.first_le_last(+n: Nat, +w: Word(n), +i: Nat, +k: Nat, e: {A.bitw.index(A.bitw.ffs(n, w)) == Some{i} : Maybe<&2, Nat>}, f: {A.bitw.index(A.bitw.fls(n, w)) == Some{k} : Maybe<&2, Nat>}) -> {Nat.is_le(i, k) == True{} : Bool}:
508  %bitw.index_some(A.bitw.ffs(n, w), i, e) : {Nat.is_le(_, 1n+k) == True{} : Bool}
509  %bitw.index_some(A.bitw.fls(n, w), k, f) : {Nat.is_le(A.bitw.ffs(n, w), _) == True{} : Bool}
510  bitw.ffs_le_fls(n, w)