~/jendhub

law from_nat_add.m

lawful-words@0.1.0.0 · proof_u32.bend:437

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

437law from_nat_add.m:
438  for +x: Nat
439  for +y: Nat
440  for +m: Nat
441  for +hm: {Nat.pow(2n, 32n) == m : Nat}
442  {U32.from_nat(Nat.add(x, y)) == U32.add(U32.from_nat(x), U32.from_nat(y)) : U32}

Uses (14)

Used by (1)