BoundedU32Arithmetic.native_roundtrip: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as BoundedU32Arithmetic
Lines 18-24 of stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend&start_line=18&end_line=24

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

def native_roundtrip(+a: U32) -> {U32.from_nat(U32.to_nat(a)) == a : U32}:
  match a:
    case U32{+w}:
      %Equal.sym(U32,U32.from_nat(Word.to_nat(32n,w)),U32{WordArithmetic.encode(Word.to_nat(32n,w),32n)},
        WordArithmetic.native_encoding(Word.to_nat(32n,w))) : {_ == U32{w} : U32}
      %Equal.sym(Word(32n),WordArithmetic.encode(Word.to_nat(32n,w),32n),w,Multiplication.word_roundtrip(32n,w)) : {U32{_} == U32{w} : U32}
      {==}

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  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_arithmetic.bend&name=native_encoding
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=word_roundtrip