law notM

lawful-fields@0.1.1.0 · proof_num.bend:44

import lawful-fields@0.1.1.0/proof_num.bend as ProofNum

import Base

44law notM:
45  for +M: Nat
46  for +hm: {Nat.pow(2n, 32n) == M : Nat}
47  {U32.to_nat(U32.not(0)) == Nat.sub(Nat.sub(M, 1n), U32.to_nat(0)) : Nat}

Uses (6)

Used by (1)

lawful-fields@0.1.1.0/proof_num:QM