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

import Base

def iteration_matches_denotation(
  ~Observation: Data,~State: Data,
  ~Index: Data,
  ~step: State -> State,
  ~project: Index -> State -> Observation,
  ~denote: Index -> Nat -> State -> Observation,
  ~at_zero: @+index: Index -> @+state: State -> {project(index,state) == denote(index,0n,state) : Observation},
  ~after_step: @+index: Index -> @+count: Nat -> @+state: State -> {denote(index,count,step(state)) == denote(index,1n+count,state) : Observation},
  +count: Nat,+index: Index,+state: State
) -> {project(index,iterate(~State,~step,count,state)) == denote(index,count,state) : Observation}:
  match count:
    case 0n: at_zero(index,state)
    case 1n+ +rest:
      %after_step(index,rest,state) : {project(index,iterate(~State,~step,rest,step(state))) == _ : Observation}
      iteration_matches_denotation(~Observation,~State,~Index,~step,~project,~denote,~at_zero,~after_step,rest,index,step(state))

Uses (2):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/loop_projection.bend&name=iterate