law first_hit

lawful-bytes@0.1.1.0 · proof_list.bend:242

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

242# Below to, the answer holds c.
243law first_hit:
244  for +xs: List<&2, U32>
245  for +from: Nat
246  for +to: Nat
247  for +c: U32
248  for +hft: {Nat.is_le(from, to) == True{} : Bool}
249  for +ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
250  for +hlt: {Nat.is_lt(D.first(xs, from, to, c), to) == True{} : Bool}
251  {D.has(xs, D.first(xs, from, to, c), c) == True{} : Bool}