U32Shift.double_parts: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/u32_shift.bend as U32Shift
Lines 85-97 of stelliferous@0.0.2.0/proofs/u32_shift.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&start_line=85&end_line=97

import Base
import stelliferous@0.0.2.0/proofs/u32_successor.bend as U32Successor
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
import stelliferous@0.0.2.0/proofs/word_encoding.bend as WordEncoding

def double_parts(+parts: WordEncoding.Split<31n,1n>) -> DoubleGoal(WordEncoding.join(31n,1n,parts)):
  WordEncoding.Parts{+low,+high} = parts
  bound =>
    %Equal.sym(Word(1n),high,Word.zero(1n),WordEncoding.upper_zero(31n,0n,low,high,bound)) : {Word.to_nat(32n,Word.shl(32n,
          WordEncoding.concat(31n,1n,low,_))) == Nat.double(Word.to_nat(32n,WordEncoding.concat(31n,1n,low,_))) : Nat}
    %Equal.sym(Word(32n),WordEncoding.concat(31n,1n,low,Word.zero(1n)),Word.shr.pad(31n,low),U32Successor.concat_pad(31n,
        low)) : {Word.to_nat(32n,Word.shl(32n,_)) == Nat.double(Word.to_nat(32n,_)) : Nat}
    %Equal.sym(Word(32n),Word.shl(32n,Word.shr.pad(31n,low)),Word.shl.put(32n,False{},Word.shr.pad(31n,low)),WordArithmetic.shift_put(32n,
        Word.shr.pad(31n,low))) : {Word.to_nat(32n,_) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat}
    %Equal.sym(Word(32n),Word.shl.put(32n,False{},Word.shr.pad(31n,low)),WCon{False{},low},put_pad(31n,False{},low)) : {Word.to_nat(32n,
        _) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat}
    %U32Successor.pad_nat(31n,low) : {Nat.double(_) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat}
    {==}

Uses (20):
  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=Base/base.bend&name=Word.shl.put
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.shr.pad
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.to_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Word.zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=DoubleGoal
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_shift.bend&name=put_pad
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_successor.bend&name=concat_pad
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_successor.bend&name=pad_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&name=shift_put
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=Split
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=concat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=join
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_encoding.bend&name=upper_zero