WordMultiplication.word_roundtrip: law of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_multiplication.bend as WordMultiplication
Lines 66-69 of stelliferous@0.0.2.0/proofs/word_multiplication.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&start_line=66&end_line=69

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

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

Uses (11):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.double
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Con
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.Nil
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.inc
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&name=encode
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=encoded_double