law pl_r_miss_step

lawful-bytes@0.1.1.0 · proof_list.bend:170

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

170law pl_r_miss_step:
171  for +x: U32
172  for +t: List<&2, U32>
173  for +c: U32
174  for +r: Nat
175  for +z: Bool
176  for +k: Nat
177  for +hz: {U32.is_eq(x, c) == z : Bool}
178  for +hk: {Nat.is_lt(k, Bool.pick(Nat, z, 0n, 1n+r)) == True{} : Bool}
179  for ih: @k2: Nat -> {Nat.is_lt(k2, r) == True{} : Bool} -> {D.has(t, k2, c) == False{} : Bool}
180  {D.has(Con{x, t}, k, c) == False{} : Bool}