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

import Base

# Concrete adapters must establish cost_per_step; it is not a heap-cost claim.
def iteration_result_and_work(
  ~State: Data,~step: State -> State,~cost: State -> Nat,
  ~width: Nat,
  ~cost_per_step: @+state: State -> {cost(state) == width : Nat},
  +count: Nat,+state: State
) -> {measured_iteration(~State,~step,~cost,count,state) == Measured{iterate(~State,~step,count,state),Nat.mul(count,width)} : Measured<State>}:
  match count:
    case 0n: {==}
    case 1n+ +rest:
      %cost_per_step(state) : {add_work(State,cost(state),measured_iteration(~State,~step,~cost,rest,step(state))) == add_work(State,_,
          Measured{iterate(~State,~step,rest,step(state)),Nat.mul(rest,width)}) : Measured<State>}
      %iteration_result_and_work(~State,~step,~cost,~width,~cost_per_step,rest,step(state)) : {add_work(State,cost(state),
          measured_iteration(~State,~step,~cost,rest,step(state))) == add_work(State,cost(state),_) : Measured<State>}
      {==}

Uses (6):
  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=stelliferous@0.0.2.0/proofs/loop_projection.bend&name=Measured
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/loop_projection.bend&name=add_work
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/loop_projection.bend&name=iterate
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/loop_projection.bend&name=measured_iteration