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

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/storage_tree_model.bend as Tree

def copy_traversal_refines_storage(~Element: Data,+count: Nat,
  +state: Traversal.State<&2,&2,Tree.Tree<Element>,Tree.Tree<Element>,Traversal.Offsets>) ->
  {Traversal.run(~Array<Element>,~Element,~Traversal.Offsets,~Traversal.source_offset(~Element),~Traversal.destination_offset,count,
      represent(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),state)) ==
    represent(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),
      Loop.run(~Traversal.State<&2,&2,Tree.Tree<Element>,Tree.Tree<Element>,Traversal.Offsets>,
        ~model_step(~Tree.Tree<Element>,~Element,~Traversal.Offsets,~sample_offset(~Element),~Traversal.destination_offset),count,state)) :
    Traversal.State<&1,&1,Array<Element>,Array<Element>,Traversal.Offsets>}:
  traversal_refines_model(~Array<Element>,~Tree.Tree<Element>,~Element,~Traversal.Offsets,~pack_tree(~Element),
    ~Traversal.source_offset(~Element),~sample_offset(~Element),~Traversal.destination_offset,~offset_read_refines_storage(~Element),count,state)

Uses (15):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Array
  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/storage_tree_model.bend&name=Tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=model_step
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=offset_read_refines_storage
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=pack_tree
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=represent
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=sample_offset
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_array_refinement.bend&name=traversal_refines_model
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=Offsets
  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_array.bend&name=destination_offset
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=run
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_array.bend&name=source_offset
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/traversal_loop.bend&name=run