law idx32

lawful-words@0.1.0.0 · proof_bytes.bend:414

import Base

414law idx32:
415  for +j: Nat
416  for +k: Nat
417  for +hj: {Nat.is_lt(j, 4n) == True{} : Bool}
418  for +hk: {Nat.is_lt(k, 8n) == True{} : Bool}
419  {Nat.is_lt(Nat.add(Nat.mul(8n, j), k), 32n) == True{} : Bool}