law pl_r2_hit_step

lawful-bytes@0.1.1.0 · proof_list.bend:357

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

357law pl_r2_hit_step:
358  for +x: U32
359  for +t: List<&2, U32>
360  for +c1: U32
361  for +c2: U32
362  for +r: Nat
363  for +p: Nat
364  for +z: Bool
365  for +hz: {(U32.is_eq(x, c1) || U32.is_eq(x, c2)) == z : Bool}
366  for +hlt: {Nat.is_lt(Bool.pick(Nat, z, 0n, 1n+r), 1n+p) == True{} : Bool}
367  for ih: {Nat.is_lt(r, p) == True{} : Bool} -> {D.has2(t, r, c1, c2) == True{} : Bool}
368  {D.has2(Con{x, t}, Bool.pick(Nat, z, 0n, 1n+r), c1, c2) == True{} : Bool}