law zb2_bidx

lawful-bytes@0.1.1.0 · proof_fast_word.bend:97

import Base
import lawful-bytes@0.1.1.0/fast.bend as FA

97law zb2_bidx:
98  for +v1: U32
99  for +v2: U32
100  for +h: {Nat.is_lt(Nat.min(P0(v1), P0(v2)), 4n) == True{} : Bool}
101  {U32.to_nat(FA.bidx(U32.or(FA.zb(v1), FA.zb(v2)))) == Nat.min(P0(v1), P0(v2)) : Nat}