law run_hit

lawful-bytes@0.1.1.0 · proof_fast_find.bend:151

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

151# A hit inside xs: the first c of take(xs ++ ys, n) is at min(run, n).
152law run_hit:
153  for +xs: List<&2, U32>
154  for +ys: List<&2, U32>
155  for +n: Nat
156  for +c: U32
157  for +b: Bool
158  for +hb: {hd_eq(xs, c) == b : Bool}
159  for +h: {Nat.is_lt(D.run_len(xs, c), List.length(&2, U32, xs)) == True{} : Bool}
160  {D.run_len(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c) == Nat.min(D.run_len(xs, c), n) : Nat}