def encode_double

stelliferous@0.0.2.0 · proofs/word_arithmetic.bend:113

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

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