def right_stays_in_child

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:114

import Base
import stelliferous@0.0.2.0/proofs/nat_order.bend as Order

114def right_stays_in_child(+depth: Nat,+index: U32,+limit: {Nat.is_le(1n+depth,30n) == True{} : Bool},+bound: {U32.is_lt(index,capacity(1n+depth)) == True{} : Bool},
115  +choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) -> {U32.is_lt((index - capacity(depth) : U32),capacity(depth)) == True{} : Bool}:
116  right_stays_in_child_full(depth,index,Order.successor(1n+depth,30n,limit),bound,choice)