~/jendhub

law p32

lawful-words@0.1.0.0 · proof_bytes.bend:1452

import lawful-words@0.1.0.0/proof_bytes.bend as ProofBytes
import Base

1452law p32:
1453  for +a: Nat
1454  for +m: Nat
1455  for +ha: {Nat.pow(2n, 8n) == a : Nat}
1456  for +hm: {Nat.pow(2n, 32n) == m : Nat}
1457  {m == Nat.mul(Nat.mul(Nat.mul(a, a), a), a) : Nat}

Uses (6)

Used by (1)