law pl_r2_miss_step

lawful-bytes@0.1.1.0 · proof_list.bend:398

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

398law pl_r2_miss_step:
399  for +x: U32
400  for +t: List<&2, U32>
401  for +c1: U32
402  for +c2: U32
403  for +r: Nat
404  for +z: Bool
405  for +k: Nat
406  for +hz: {(U32.is_eq(x, c1) || U32.is_eq(x, c2)) == z : Bool}
407  for +hk: {Nat.is_lt(k, Bool.pick(Nat, z, 0n, 1n+r)) == True{} : Bool}
408  for ih: @k2: Nat -> {Nat.is_lt(k2, r) == True{} : Bool} -> {D.has2(t, k2, c1, c2) == False{} : Bool}
409  {D.has2(Con{x, t}, k, c1, c2) == False{} : Bool}