law word_roundtrip

stelliferous@0.0.2.0 · proofs/word_multiplication.bend:66

import Base
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic

66law word_roundtrip:
67  for +n: Nat
68  for +w: Word(n)
69  {WordArithmetic.encode(Word.to_nat(n,w),n) == w : Word(n)}