law first2_hit

lawful-bytes@0.1.1.0 · LAWS.bend:376

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

376law first2_hit:
377  for xs: List<&2, U32>
378  for from: Nat
379  for to: Nat
380  for c1: U32
381  for c2: U32
382  for hft: {Nat.is_le(from, to) == True{} : Bool}
383  for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
384  for hlt: {Nat.is_lt(D.first2(xs, from, to, c1, c2), to) == True{} : Bool}
385  {D.has2(xs, D.first2(xs, from, to, c1, c2), c1, c2) == True{} : Bool}