def bitw.fls_le

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

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

385def bitw.fls_le(n: Nat, w: Word(n)) -> {Nat.is_le(A.bitw.fls(n, w), n) == True{} : Bool}:
386  match n:
387    case 0n:
388      {==}
389    case 1n+ +p:
390      match w:
391        case WCon{b, +t}:
392          bitw.fls_le.h(A.bitw.fls(p, t), b, p, bitw.fls_le(p, t))