law pl_r2_miss

lawful-bytes@0.1.1.0 · proof_list.bend:420

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

420law pl_r2_miss:
421  for +zs: List<&2, U32>
422  for +n: Nat
423  for +c1: U32
424  for +c2: U32
425  for +k: Nat
426  for +hk: {Nat.is_lt(k, D.run_len2(List.take(&2, U32, zs, n), c1, c2)) == True{} : Bool}
427  {D.has2(zs, k, c1, c2) == False{} : Bool}