~/jendhub

law to_nat_not.m

lawful-words@0.1.0.0 · proof_u32.bend:1171

import lawful-words@0.1.0.0/proof_u32.bend as ProofU32
import Base

1171law to_nat_not.m:
1172  for +a: U32
1173  for +m: Nat
1174  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1175  {U32.to_nat(U32.not(a)) == Nat.sub(Nat.sub(m, 1n), U32.to_nat(a)) : Nat}

Uses (13)

Used by (1)