TraversalArrayRefinement.indexed_fold_change_context: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as TraversalArrayRefinement
Lines 254-271 of stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&start_line=254&end_line=271

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal

# One bounded induction carries capacity, preserved sources and completed
# output values together. A strategy proves its local update obligation;
# it does not reimplement the whole output traversal proof.
def indexed_fold_change_context(~State: Data,~Outer: Data,~Inner: Data,
  ~project: Outer -> Inner,~outer_step: U32 -> Outer -> State -> State,~inner_step: U32 -> Inner -> State -> State,
  ~same_step: @+index: U32 -> @+context: Outer -> @+state: State ->
    {outer_step(index,context,state) == inner_step(index,project(context),state) : State},
  +count: Nat,+first: U32,+context: Outer,+state: State) ->
  {Traversal.indexed_fold(~State,~Outer,~outer_step,count,first,context,state) ==
    Traversal.indexed_fold(~State,~Inner,~inner_step,count,first,project(context),state) : State}:
  match count:
    case 0n: {==}
    case 1n+ +rest:
      %Equal.sym(State,outer_step(first,context,state),inner_step(first,project(context),state),same_step(first,context,state)) :
        {Traversal.indexed_fold(~State,~Outer,~outer_step,rest,(first + 1 : U32),context,_) ==
          Traversal.indexed_fold(~State,~Inner,~inner_step,rest,(first + 1 : U32),project(context),inner_step(first,project(context),state)) : State}
      indexed_fold_change_context(~State,~Outer,~Inner,~project,~outer_step,~inner_step,~same_step,
        rest,(first + 1 : U32),context,inner_step(first,project(context),state))

Uses (5):
  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=U32
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.add
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=indexed_fold