LoopProjection.add_counted_stride: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/loop_projection.bend as LoopProjection
Lines 92-99 of stelliferous@0.0.2.0/proofs/loop_projection.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/loop_projection.bend&start_line=92&end_line=99

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

def add_counted_stride(+position: U32,+stride: Nat,+count: Nat) ->
  {((position + U32.from_nat(stride) : U32) + U32.from_nat(Nat.mul(count,stride)) : U32) ==
    (position + U32.from_nat(Nat.mul(1n+count,stride)) : U32) : U32}:
  Equal.trans(U32,((position + U32.from_nat(stride) : U32) + U32.from_nat(Nat.mul(count,stride)) : U32),
    (position + (U32.from_nat(stride) + U32.from_nat(Nat.mul(count,stride)) : U32) : U32),
    (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))),
    Equal.cong(U32,U32,value => (position + value : U32),(U32.from_nat(stride) + U32.from_nat(Nat.mul(count,stride)) : U32),
      U32.from_nat(Nat.mul(1n+count,stride)),WordArithmetic.native_add(stride,Nat.mul(count,stride))))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.cong
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.trans
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.mul
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend&name=add_associative
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/word_arithmetic.bend&name=native_add