def map_loop_refines_model

stelliferous@0.0.2.0 · proofs/traversal_array_refinement.bend:165

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
import stelliferous@0.0.2.0/proofs/loop_projection.bend as Projection

165def map_loop_refines_model(~Element: Data,~Context: Data,~map: Context -> Element -> Element,
166  +count: Nat,+state: Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>) ->
167  {Loop.run(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.map_step(~Element,~Context,~map),
168      count,represent_map(~Element,~Context,state)) ==
169    represent_map(~Element,~Context,Loop.run(~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,
170      ~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),count,state)) : Traversal.State<&2,&1,Unit,Array<Element>,Context>}:
171  Projection.iteration_refines_model(~Traversal.State<&2,&1,Unit,Array<Element>,Context>,~Traversal.State<&2,&2,Unit,Tree.Tree<Element>,Context>,
172    ~Traversal.map_step(~Element,~Context,~map),~model_map_step(~Element,~Context,~unindexed(~Element,~Context,~map)),~represent_map(~Element,~Context),
173    ~map_step_refines_model(~Element,~Context,~map),count,state)