TraversalArrayRefinement.indexed_fold_refines_model: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as TraversalArrayRefinement
Lines 237-252 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=237&end_line=252

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

def indexed_fold_refines_model(~Runtime: Type,~Model: Data,~Context: Data,
  ~update: U32 -> Context -> Runtime -> Runtime,~model_update: U32 -> Context -> Model -> Model,
  ~represent: Model -> Runtime,
  ~step_matches: @+index: U32 -> @+context: Context -> @+state: Model ->
    {update(index,context,represent(state)) == represent(model_update(index,context,state)) : Runtime},
  +count: Nat,+index: U32,+context: Context,+state: Model) ->
  {Traversal.indexed_fold(~Runtime,~Context,~update,count,index,context,represent(state)) ==
    represent(Traversal.indexed_fold(~Model,~Context,~model_update,count,index,context,state)) : Runtime}:
  match count:
    case 0n: {==}
    case 1n+ +rest:
      %Equal.sym(Runtime,update(index,context,represent(state)),represent(model_update(index,context,state)),step_matches(index,context,state)) :
        {Traversal.indexed_fold(~Runtime,~Context,~update,rest,(index + 1 : U32),context,_) ==
          represent(Traversal.indexed_fold(~Model,~Context,~model_update,rest,(index + 1 : U32),context,model_update(index,context,state))) : Runtime}
      indexed_fold_refines_model(~Runtime,~Model,~Context,~update,~model_update,~represent,~step_matches,
        rest,(index + 1 : U32),context,model_update(index,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