TraversalBatchRefinement.state_after: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as TraversalBatchRefinement
Lines 34-52 of stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&start_line=34&end_line=52

import Base
import stelliferous@0.0.2.0/traversal_array.bend as Traversal
import stelliferous@0.0.2.0/traversal_loop.bend as Loop
import stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend as ArrayLaws
import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as MapReadback
import stelliferous@0.0.2.0/proofs/storage_tree_model.bend as Tree
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition

# The whole state after count steps of the model map.
def state_after(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+count: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>) ->
  {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),count,Traversal.State{Unit{},input,U32.from_nat(start),context}) ==
    Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input),U32.from_nat(Nat.add(start,count)),context} :
    ModelState(~Element,~Context)}:
  match count:
    case 0n:
      %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) :
        {Traversal.State{Unit{},input,U32.from_nat(start),context} == Traversal.State{Unit{},input,U32.from_nat(_),context} : ModelState(~Element,~Context)}
      {==}
    case 1n+ +rest:
      +written = Tree.write(Element,input,U32.from_nat(start),map(context,U32.from_nat(start),Tree.read(Element,input,U32.from_nat(start))))
      %Equal.sym(Nat,Nat.add(start,1n+rest),1n+Nat.add(start,rest),Addition.successor_right(start,rest)) :
        {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),rest,Traversal.State{Unit{},written,(U32.from_nat(start) + 1 : U32),context}) ==
          Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,rest,(U32.from_nat(start) + 1 : U32),context,written),U32.from_nat(_),context} : ModelState(~Element,~Context)}
      %Equal.sym(U32,(U32.from_nat(start) + 1 : U32),U32.from_nat(1n+start),Bounds.add_one(U32.from_nat(start))) :
        {Loop.run(~ModelState(~Element,~Context),~ArrayLaws.model_map_step(~Element,~Context,~map),rest,Traversal.State{Unit{},written,_,context}) ==
          Traversal.State{Unit{},MapReadback.run_indexed(~Element,~Context,~map,rest,_,context,written),U32.from_nat(1n+Nat.add(start,rest)),context} : ModelState(~Element,~Context)}
      state_after(~Element,~Context,~map,rest,1n+start,context,written)

Uses (18):
  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=Nat.add
  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=Base/base.bend&name=U32.from_nat
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Unit
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=add_one
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=successor_right
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=zero_right
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=read
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_tree_model.bend&name=write
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=model_map_step
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&name=ModelState
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=run_indexed
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=State
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_loop.bend&name=run