U32Successor.word: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_successor.bend as U32Successor
Lines 140-142 of stelliferous@0.0.2.0/proofs/u32_successor.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/u32_successor.bend&start_line=140&end_line=142

import Base
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

def word(+w: Word(32n)) -> Goal(U32{w}):
  %WordEncoding.recover(31n,1n,w) : Goal(U32{_})
  parts(WordEncoding.split(31n,1n,w))

Uses (6):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_successor.bend&name=Goal
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_successor.bend&name=parts
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=recover
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=split