TraversalBatchRefinement.mapped: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend as TraversalBatchRefinement
Lines 116-126 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=116&end_line=126

import Base
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/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition

# A batch from the original tree is the map of its positions.
def mapped(~Element: Data,~Context: Data,~map: Context -> U32 -> Element -> Element,+count: Nat,+start: Nat,+context: Context,+input: Tree.Tree<Element>,
  +depth: Nat,+capacity: U32,+capacity_equal: {Tree.capacity(Element,input) == capacity : U32},+balanced: Shape.Balanced(Element,depth,input),
  +limit: {Nat.is_le(depth,31n) == True{} : Bool},+capacity_ok: {U32.is_le(capacity,2147483648) == True{} : Bool},
  +room: {Nat.is_le(Nat.add(start,count),U32.to_nat(capacity)) == True{} : Bool}) ->
  {batch(~Element,~Context,~map,count,U32.from_nat(start),context,input,input) == MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input) : Tree.Tree<Element>}:
  %Addition.zero_right(start) :
    {batch(~Element,~Context,~map,count,U32.from_nat(_),context,input,input) == MapReadback.run_indexed(~Element,~Context,~map,count,U32.from_nat(start),context,input) : Tree.Tree<Element>}
  continued(~Element,~Context,~map,count,0n,start,context,input,depth,capacity,capacity_equal,balanced,limit,capacity_ok,
    %Equal.sym(Nat,Nat.add(start,0n),start,Addition.zero_right(start)) : {Nat.is_le(Nat.add(_,count),U32.to_nat(capacity)) == True{} : Bool}
    room)

Uses (16):
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Bool
  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=Nat.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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=U32.is_le
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32.to_nat
  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_shape.bend&name=Balanced
  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=capacity
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&name=batch
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_batch_refinement.bend&name=continued
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&name=run_indexed