def step_total
stelliferous@0.0.2.0 · proofs/binary_division.bend:91
import stelliferous@0.0.2.0/proofs/binary_division.bend as BinaryDivision
import Base
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison
91def step_total(+bit: Bool,+b: Nat,+prev: Quotient) -> {total(step(bit,b,prev),b) == Comparison.digit(bit,total(prev,b)) : Nat}:
92 Quotient{+q,+r} = prev
93 %Equal.sym(Nat,total(branch(Nat.is_ge(Comparison.digit(bit,r),b),Nat.double(q),Comparison.digit(bit,r),b),b),
94 Nat.add(Nat.mul(Nat.double(q),b),Comparison.digit(bit,r)),branch_total(Nat.is_ge(Comparison.digit(bit,r),b),Nat.double(q),
95 Comparison.digit(bit,r),b,{==})) : {_ == Comparison.digit(bit,Nat.add(Nat.mul(q,b),r)) : Nat}
96 digit_total(bit,q,r,b)