law bt_bidx
lawful-bytes@0.1.1.0 · proof_fast_w2.bend:336
import lawful-bytes@0.1.1.0/proof_fast_w2.bend as ProofFastW2
import Base
import lawful-bytes@0.1.1.0/fast.bend as FA
336law bt_bidx:
337 for +e0: Bool
338 for +e1: Bool
339 for +e2: Bool
340 for +e3: Bool
341 for +h: {Nat.is_lt(R4(e0, e1, e2, e3), 4n) == True{} : Bool}
342 {U32.to_nat(U32.add(U32.add(FA.b2u(Bool.and(Bool.not(e0), True{})), FA.b2u(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), True{})))), FA.b2u(Bool.and(Bool.not(e0), Bool.and(Bool.not(e1), Bool.and(Bool.not(e2), True{})))))) == R4(e0, e1, e2, e3) : Nat}