law first_miss

lawful-bytes@0.1.1.0 · proof_list.bend:272

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

272# No index from from up to the answer holds c.
273law first_miss:
274  for +xs: List<&2, U32>
275  for +from: Nat
276  for +to: Nat
277  for +c: U32
278  for +k: Nat
279  for +hk1: {Nat.is_le(from, k) == True{} : Bool}
280  for +hk2: {Nat.is_lt(k, D.first(xs, from, to, c)) == True{} : Bool}
281  {D.has(xs, k, c) == False{} : Bool}