def double_parts

stelliferous@0.0.2.0 · proofs/u32_shift.bend:85

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

85def double_parts(+parts: WordEncoding.Split<31n,1n>) -> DoubleGoal(WordEncoding.join(31n,1n,parts)):
86  WordEncoding.Parts{+low,+high} = parts
87  bound =>
88    %Equal.sym(Word(1n),high,Word.zero(1n),WordEncoding.upper_zero(31n,0n,low,high,bound)) : {Word.to_nat(32n,Word.shl(32n,
89          WordEncoding.concat(31n,1n,low,_))) == Nat.double(Word.to_nat(32n,WordEncoding.concat(31n,1n,low,_))) : Nat}
90    %Equal.sym(Word(32n),WordEncoding.concat(31n,1n,low,Word.zero(1n)),Word.shr.pad(31n,low),U32Successor.concat_pad(31n,
91        low)) : {Word.to_nat(32n,Word.shl(32n,_)) == Nat.double(Word.to_nat(32n,_)) : Nat}
92    %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,
93        Word.shr.pad(31n,low))) : {Word.to_nat(32n,_) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat}
94    %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,
95        _) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat}
96    %U32Successor.pad_nat(31n,low) : {Nat.double(_) == Nat.double(Word.to_nat(32n,Word.shr.pad(31n,low))) : Nat}
97    {==}