law first_le_last

bend-osdev-algo@0.1.0.0 · LAWS.bend:91

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

91law first_le_last:
92  for x: U32
93  for i: Nat
94  for k: Nat
95  for e: {A.bits32.first_set(x) == Some{i} : Maybe<&2, Nat>}
96  for f: {A.bits32.last_set(x) == Some{k} : Maybe<&2, Nat>}
97  {Nat.is_le(i, k) == True{} : Bool}