law first2_miss

lawful-bytes@0.1.1.0 · LAWS.bend:387

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

387law first2_miss:
388  for xs: List<&2, U32>
389  for from: Nat
390  for to: Nat
391  for c1: U32
392  for c2: U32
393  for k: Nat
394  for hk1: {Nat.is_le(from, k) == True{} : Bool}
395  for hk2: {Nat.is_lt(k, D.first2(xs, from, to, c1, c2)) == True{} : Bool}
396  {D.has2(xs, k, c1, c2) == False{} : Bool}