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

import Base

# A read-only observation is preserved for every number of iterations.
def preserves_observation(
  ~State: Data,~Observation: Data,~step: State -> State,~observe: State -> Observation,
  ~preserved: @+state: State -> {observe(step(state)) == observe(state) : Observation},
  +count: Nat,+state: State
) -> {observe(iterate(~State,~step,count,state)) == observe(state) : Observation}:
  match count:
    case 0n: {==}
    case 1n+ +rest:
      %preserved(state) : {observe(iterate(~State,~step,rest,step(state))) == _ : Observation}
      preserves_observation(~State,~Observation,~step,~observe,~preserved,rest,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