StorageAddressBounds.sub_value: def of stelliferous@0.0.2.0
Import: import stelliferous@0.0.2.0/proofs/storage_address_bounds.bend as StorageAddressBounds
Lines 42-46 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=42&end_line=46

import Base
import stelliferous@0.0.2.0/proofs/word_power_of_two.bend as Power
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order
import stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend as Bounds
import stelliferous@0.0.2.0/proofs/bounded_u32_arithmetic.bend as Arithmetic

def sub_value(+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.to_nat((index - capacity(depth) : U32)) == Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth))) : Nat}:
  Arithmetic.subtract(index,capacity(depth),capacity(1n+depth),Power.native_power_bound(1n+depth,limit),right_order(depth,index,choice),
    Order.transitive(Nat.sub(U32.to_nat(index),U32.to_nat(capacity(depth))),U32.to_nat(index),U32.to_nat(capacity(1n+depth)),
      Order.sub_le(U32.to_nat(index),U32.to_nat(capacity(depth))),Bounds.strict_le(U32.to_nat(index),U32.to_nat(capacity(1n+depth)),Bounds.as_nat_lt(index,capacity(1n+depth),bound))))

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=Nat
  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.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/bounded_u32_arithmetic.bend&name=subtract
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=sub_le
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_order.bend&name=transitive
  https://jend.leeeet.dev/definition.txt?path=stelliferous@0.0.2.0/proofs/nat_to_u32_bounds.bend&name=as_nat_lt
  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_address_bounds.bend&name=capacity
  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/word_power_of_two.bend&name=native_power_bound