TraversalMapReadback.outside_indexed: def of stelliferous@0.0.2.0 Import: import stelliferous@0.0.2.0/proofs/traversal_map_readback.bend as TraversalMapReadback Lines 56-80 of stelliferous@0.0.2.0/proofs/traversal_map_readback.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/traversal_map_readback.bend&start_line=56&end_line=80 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/storage_readback.bend as StorageReadback import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds import stelliferous@0.0.2.0/proofs/nat_order.bend as Order import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison import stelliferous@0.0.2.0/proofs/nat_interval.bend as Interval def outside_indexed(~Element: Data,~Context: Data,~operation: Context -> U32 -> Element -> Element,count: Nat,+position: Nat,+query: U32,+context: Context,+input: Tree.Tree,+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(position,count),U32.to_nat(capacity)) == True{} : Bool}, +query_inside: {U32.is_lt(query,capacity) == True{} : Bool},+separate: Interval.Outside) -> {Tree.read(Element,run_indexed(~Element,~Context,~operation,count,U32.from_nat(position),context,input),query) == Tree.read(Element,input,query) : Element}: match count: case 0n: {==} case 1n+ +rest: +value = operation(context,U32.from_nat(position),Tree.read(Element,input,U32.from_nat(position))) +written = Tree.write(Element,input,U32.from_nat(position),value) +position_inside = Order.room_index(position,rest,U32.to_nat(capacity),room) +different = { %Equal.sym(Bool,U32.is_eq(U32.from_nat(position),query),Nat.is_eq(U32.to_nat(U32.from_nat(position)),U32.to_nat(query)),Comparison.eq(U32.from_nat(position),query)) : {_ == False{} : Bool} %Equal.sym(Nat,U32.to_nat(U32.from_nat(position)),position,Bounds.roundtrip(position,capacity,capacity_ok,Bounds.strict_le(position,U32.to_nat(capacity),position_inside))) : {Nat.is_eq(_,U32.to_nat(query)) == False{} : Bool} %Order.equal_symmetric(U32.to_nat(query),position) : {_ == False{} : Bool} Interval.outside_head(position,rest,U32.to_nat(query),separate) : {U32.is_eq(U32.from_nat(position),query) == False{} : Bool}} %Equal.sym(U32,(U32.from_nat(position) + 1 : U32),U32.from_nat(1n+position),Bounds.add_one(U32.from_nat(position))) : {Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,_,context,written),query) == Tree.read(Element,input,query) : Element} Equal.trans(Element,Tree.read(Element,run_indexed(~Element,~Context,~operation,rest,U32.from_nat(1n+position),context,written),query),Tree.read(Element,written,query),Tree.read(Element,input,query), outside_indexed(~Element,~Context,~operation,rest,1n+position,query,context,written,depth,capacity, Equal.trans(U32,Tree.capacity(Element,written),Tree.capacity(Element,input),capacity,StorageReadback.write_capacity(~Element,input,U32.from_nat(position),value),capacity_equal), Shape.write(Element,depth,input,U32.from_nat(position),value,balanced),limit,capacity_ok,Order.advance_room(position,rest,U32.to_nat(capacity),room),query_inside, Interval.outside_tail(position,rest,U32.to_nat(query),separate)), unchanged_full(~Element,depth,input,U32.from_nat(position),query,value,capacity,capacity_equal,balanced,limit,address_inside(position,capacity,capacity_ok,position_inside),query_inside,different)) Uses (34): 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=Equal.trans 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_eq 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.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=U32.is_eq 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.is_lt 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/nat_interval.bend&name=Outside https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_interval.bend&name=outside_head https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_interval.bend&name=outside_tail https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=advance_room https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=equal_symmetric https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=room_index 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/nat_to_u32_bounds.bend&name=roundtrip https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=strict_le https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_readback.bend&name=write_capacity 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_shape.bend&name=write 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/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_map_readback.bend&name=address_inside 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/proofs/traversal_map_readback.bend&name=unchanged_full https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_comparison.bend&name=eq