StorageAddressBounds.right_stays_in_child_full: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as StorageAddressBounds
Lines 58-67 of stelliferous@0.0.2.0/proofs/storage_address_bounds.bend: https://jend.leeeet.dev/read.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&start_line=58&end_line=67

import Base
import stelliferous@0.0.2.0/proofs/storage_shape.bend as Shape
import stelliferous@0.0.2.0/proofs/natural_addition.bend as Addition
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/u32_comparison.bend as Comparison

def right_stays_in_child_full(+depth: Nat,+index: U32,+limit: {Nat.is_le(1n+depth,31n) == True{} : Bool},+bound: {U32.is_lt(index,capacity(1n+depth)) == True{} : Bool},
  +choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) -> {U32.is_lt((index - capacity(depth) : U32),capacity(depth)) == True{} : Bool}:
  %Equal.sym(Bool,U32.is_lt((index - capacity(depth) : U32),capacity(depth)),Nat.is_lt(U32.to_nat((index - capacity(depth) : U32)),U32.to_nat(capacity(depth))),Comparison.lt((index - capacity(depth) : U32),capacity(depth))) : {_ == True{} : Bool}
  %Equal.sym(Nat,U32.to_nat((index - capacity(depth) : U32)),Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth))),sub_value(depth,index,limit,bound,choice)) :
    {Nat.is_lt(_,U32.to_nat(capacity(depth))) == True{} : Bool}
  Order.sub_lt(U32.to_nat(index),U32.to_nat(capacity(depth)),U32.to_nat(capacity(depth)),right_order(depth,index,choice),
    %Equal.sym(Nat,U32.to_nat(capacity(depth)),Shape.extent(depth),capacity_value(depth,child_limit_full(depth,limit))) :
      {Nat.is_lt(U32.to_nat(index),Nat.add(_,_)) == True{} : Bool}
    %Equal.sym(Nat,Nat.add(Shape.extent(depth),Shape.extent(depth)),Nat.double(Shape.extent(depth)),Addition.double(Shape.extent(depth))) : {Nat.is_lt(U32.to_nat(index),_) == True{} : Bool}
    natural_bound(1n+depth,index,limit,bound))

Uses (22):
  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.double
  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=Nat.is_lt
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=Nat.sub
  https://jend.leeeet.dev/definition.txt?path=Base/base.bend&name=U32
  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.sub
  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_order.bend&name=sub_lt
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/natural_addition.bend&name=double
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=capacity
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=capacity_value
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=child_limit_full
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=natural_bound
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=right_order
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_address_bounds.bend&name=sub_value
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/storage_shape.bend&name=extent
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/u32_comparison.bend&name=lt