WordSubtraction.subtract_add: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_subtraction.bend as WordSubtraction
Lines 78-82 of stelliferous@0.0.2.0/proofs/word_subtraction.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_subtraction.bend&start_line=78&end_line=82

import Base

def subtract_add(+a: U32,+b: U32) -> {U32.sub(U32.add(a,b),b) == a : U32}:
  match a b:
    case U32{+x} U32{+y}:
      %undo(32n,x,y,False{},False{}) : {U32{Word.sub(32n,Word.add(32n,x,y),y)} == U32{_} : U32}
      {==}

Uses (7):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.sub
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_subtraction.bend&name=undo