def add_counted_stride
stelliferous@0.0.2.0 · proofs/loop_projection.bend:92
import stelliferous@0.0.2.0/proofs/loop_projection.bend as LoopProjection
import Base
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic
import stelliferous@0.0.2.0/proofs/word_arithmetic.bend as WordArithmetic
92def add_counted_stride(+position: U32,+stride: Nat,+count: Nat) ->
93 {((position + U32.from_nat(stride) : U32) + U32.from_nat(Nat.mul(count,stride)) : U32) ==
94 (position + U32.from_nat(Nat.mul(1n+count,stride)) : U32) : U32}:
95 Equal.trans(U32,((position + U32.from_nat(stride) : U32) + U32.from_nat(Nat.mul(count,stride)) : U32),
96 (position + (U32.from_nat(stride) + U32.from_nat(Nat.mul(count,stride)) : U32) : U32),
97 (position + U32.from_nat(Nat.mul(1n+count,stride)) : U32),Arithmetic.add_associative(position,U32.from_nat(stride),U32.from_nat(Nat.mul(count,stride))),
98 Equal.cong(U32,U32,value => (position + value : U32),(U32.from_nat(stride) + U32.from_nat(Nat.mul(count,stride)) : U32),
99 U32.from_nat(Nat.mul(1n+count,stride)),WordArithmetic.native_add(stride,Nat.mul(count,stride))))