WordArithmetic.encode_double: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
Lines 113-116 of stelliferous@0.0.2.0/proofs/word_arithmetic.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&start_line=113&end_line=116

import Base
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition

def encode_double(+a: Nat,+width: Nat) -> {encode(Nat.double(a),width) == Word.shl(width,encode(a,width)) : Word(width)}:
  %Addition.double(a) : {encode(_,width) == Word.shl(width,encode(a,width)) : Word(width)}
  %encode_add(a,a,width) : {_ == Word.shl(width,encode(a,width)) : Word(width)}
  double_word(width,encode(a,width))

Uses (8):
  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.shl
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=double
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&name=double_word
  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=encode_add