LoopProjection.counter_progress: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/loop_projection.bend as LoopProjection
Lines 101-110 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=101&end_line=110

import Base
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic

def counter_progress(~State: Data,~step: State -> State,~position: State -> U32,~stride: Nat,
  ~advances: @+state: State -> {position(step(state)) == (position(state) + U32.from_nat(stride) : U32) : U32},
  +count: Nat,+state: State) ->
  {position(iterate(~State,~step,count,state)) == (position(state) + U32.from_nat(Nat.mul(count,stride)) : U32) : U32}:
  match count:
    case 0n: Equal.sym(U32,(position(state) + 0 : U32),position(state),Arithmetic.add_zero(position(state)))
    case 1n+ +rest:
      %add_counted_stride(position(state),stride,rest) : {position(iterate(~State,~step,rest,step(state))) == _ : U32}
      %advances(state) : {position(iterate(~State,~step,rest,step(state))) == (_ + U32.from_nat(Nat.mul(rest,stride)) : U32) : U32}
      counter_progress(~State,~step,~position,~stride,~advances,rest,step(state))

Uses (9):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Equal.sym
  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_zero
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/loop_projection.bend&name=add_counted_stride
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/loop_projection.bend&name=iterate