def right_order

stelliferous@0.0.2.0 · proofs/storage_address_bounds.bend:36

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

36def right_order(+depth: Nat,+index: U32,choice: {U32.is_lt(index,capacity(depth)) == False{} : Bool}) ->
37  {Nat.is_le(U32.to_nat(capacity(depth)),U32.to_nat(index)) == True{} : Bool}:
38  Order.ge_true(U32.to_nat(index),U32.to_nat(capacity(depth)),Order.comparison_not_less(Nat.cmp(U32.to_nat(index),U32.to_nat(capacity(depth))),
39    %Comparison.lt(index,capacity(depth)) : {_ == False{} : Bool}
40    choice))