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

import Base
import stelliferous@0.0.2.0/traversal_loop.bend as Loop

# A single commuting step lifts to every count. RuntimeState may own arrays;
# only the model is duplicated in the proof. No runtime array is cloned.
def iteration_refines_model(
  ~RuntimeState: Type,~ModelState: Data,
  ~runtime_step: RuntimeState -> RuntimeState,~model_step: ModelState -> ModelState,
  ~represent: ModelState -> RuntimeState,
  ~step_matches: @+state: ModelState -> {runtime_step(represent(state)) == represent(model_step(state)) : RuntimeState},
  +count: Nat,+state: ModelState
) -> {Loop.run(~RuntimeState,~runtime_step,count,represent(state)) == represent(Loop.run(~ModelState,~model_step,count,state)) : RuntimeState}:
  match count:
    case 0n: {==}
    case 1n+ +rest:
      %Equal.sym(RuntimeState,runtime_step(represent(state)),represent(model_step(state)),step_matches(state)) :
        {Loop.run(~RuntimeState,~runtime_step,rest,_) == represent(Loop.run(~ModelState,~model_step,rest,model_step(state))) : RuntimeState}
      iteration_refines_model(~RuntimeState,~ModelState,~runtime_step,~model_step,~represent,~step_matches,rest,model_step(state))

Uses (3):
  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=stelliferous@0.0.2.0/traversal_loop.bend&name=run