law first2_range

lawful-bytes@0.1.1.0 · LAWS.bend:366

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

366law first2_range:
367  for xs: List<&2, U32>
368  for from: Nat
369  for to: Nat
370  for c1: U32
371  for c2: U32
372  for hft: {Nat.is_le(from, to) == True{} : Bool}
373  for ht: {Nat.is_le(to, List.length(&2, U32, xs)) == True{} : Bool}
374  {(Nat.is_le(from, D.first2(xs, from, to, c1, c2)) && Nat.is_le(D.first2(xs, from, to, c1, c2), to)) == True{} : Bool}