def padded_successor
stelliferous@0.0.2.0 · proofs/u32_successor.bend:121
import stelliferous@0.0.2.0/proofs/u32_successor.bend as U32Successor
import Base
121def padded_successor(+low: Word(31n)) -> {U32.to_nat(U32.add(U32{Word.shr.pad(31n,low)},1)) == 1n+U32.to_nat(U32{Word.shr.pad(31n,low)}) : Nat}:
122 %Equal.sym(Word(32n),Word.add(32n,Word.shr.pad(31n,low),Word.inc(32n,Word.zero(32n))),Word.inc(32n,Word.shr.pad(31n,low)),add_one(32n,
123 Word.shr.pad(31n,low))) : {Word.to_nat(32n,_) == 1n+Word.to_nat(32n,Word.shr.pad(31n,low)) : Nat}
124 %Equal.sym(Nat,Word.to_nat(32n,Word.shr.pad(31n,low)),Word.to_nat(31n,low),pad_nat(31n,low)) : {Word.to_nat(32n,Word.inc(32n,Word.shr.pad(31n,
125 low))) == 1n+_ : Nat}
126 inc_nat(31n,low)