law pl_r_miss

lawful-bytes@0.1.1.0 · proof_list.bend:191

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

191# Before the end of the run, no c.
192law pl_r_miss:
193  for +zs: List<&2, U32>
194  for +n: Nat
195  for +c: U32
196  for +k: Nat
197  for +hk: {Nat.is_lt(k, D.run_len(List.take(&2, U32, zs, n), c)) == True{} : Bool}
198  {D.has(zs, k, c) == False{} : Bool}