def unchanged

stelliferous@0.0.2.0 · proofs/traversal_map_readback.bend:158

import Base
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/nat_order.bend as Order

158def unchanged(~Element: Data,+depth: Nat,+input: Tree.Tree<Element>,+position: U32,+query: U32,+value: Element,+capacity: U32,
159  +capacity_equal: {Tree.capacity(Element,input) == capacity : U32},balanced: Shape.Balanced(Element,depth,input),limit: {Nat.is_le(depth,30n) == True{} : Bool},
160  position_inside: {U32.is_lt(position,capacity) == True{} : Bool},query_inside: {U32.is_lt(query,capacity) == True{} : Bool},different: {U32.is_eq(position,query) == False{} : Bool}) ->
161  {Tree.read(Element,Tree.write(Element,input,position,value),query) == Tree.read(Element,input,query) : Element}:
162  unchanged_full(~Element,depth,input,position,query,value,capacity,capacity_equal,balanced,Order.successor(depth,30n,limit),position_inside,query_inside,different)