WordMultiplication.encoded_double: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/word_multiplication.bend as WordMultiplication
Lines 58-64 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=58&end_line=64

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

def encoded_double(+a: Nat,+n: Nat) -> {WordArithmetic.encode(Nat.double(a),1n+n) == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}:
  %Equal.sym(Word(1n+n),WordArithmetic.encode(Nat.double(a),1n+n),Word.shl(1n+n,WordArithmetic.encode(a,1n+n)),WordArithmetic.encode_double(a,
      1n+n)) : {_ == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}
  %Equal.sym(Word(1n+n),Word.shl(1n+n,WordArithmetic.encode(a,1n+n)),WCon{False{},truncate(n,WordArithmetic.encode(a,1n+n))},shift(n,
      WordArithmetic.encode(a,1n+n))) : {_ == WCon{False{},WordArithmetic.encode(a,n)} : Word(1n+n)}
  %truncate_encode(a,n) : {WCon{False{},truncate(n,WordArithmetic.encode(a,1n+n))} == WCon{False{},_} : Word(1n+n)}
  {==}

Uses (12):
  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.shl
  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_double
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=shift
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=truncate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_multiplication.bend&name=truncate_encode