law pl_r_hit_step

lawful-bytes@0.1.1.0 · proof_list.bend:130

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

130law pl_r_hit_step:
131  for +x: U32
132  for +t: List<&2, U32>
133  for +c: U32
134  for +r: Nat
135  for +p: Nat
136  for +z: Bool
137  for +hz: {U32.is_eq(x, c) == z : Bool}
138  for +hlt: {Nat.is_lt(Bool.pick(Nat, z, 0n, 1n+r), 1n+p) == True{} : Bool}
139  for ih: {Nat.is_lt(r, p) == True{} : Bool} -> {D.has(t, r, c) == True{} : Bool}
140  {D.has(Con{x, t}, Bool.pick(Nat, z, 0n, 1n+r), c) == True{} : Bool}