law first_miss

lawful-bytes@0.1.1.0 · LAWS.bend:355

import Base
import lawful-bytes@0.1.1.0/defs.bend as D

355# No index from from up to the answer holds c.
356law first_miss:
357  for xs: List<&2, U32>
358  for from: Nat
359  for to: Nat
360  for c: U32
361  for k: Nat
362  for hk1: {Nat.is_le(from, k) == True{} : Bool}
363  for hk2: {Nat.is_lt(k, D.first(xs, from, to, c)) == True{} : Bool}
364  {D.has(xs, k, c) == False{} : Bool}