law run_none

lawful-bytes@0.1.1.0 · proof_fast_find.bend:219

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

219# No c in xs, and n stays within it.
220law run_none:
221  for +xs: List<&2, U32>
222  for +ys: List<&2, U32>
223  for +n: Nat
224  for +c: U32
225  for +b: Bool
226  for +hb: {hd_eq(xs, c) == b : Bool}
227  for +h: {D.run_len(xs, c) == List.length(&2, U32, xs) : Nat}
228  for +hn: {Nat.is_le(n, List.length(&2, U32, xs)) == True{} : Bool}
229  {D.run_len(List.take(&2, U32, List.append(&2, U32, xs, ys), n), c) == n : Nat}