def AP.index_lt

bend-osdev-array@0.1.0.1 · PROOF.bend:1198

import Base
import bend-osdev-array@0.1.0.1/array.bend as A

1198def AP.index_lt(+d: Nat, +i: U32) -> {Nat.is_lt(A.Arrays.index(d, i), A.Arrays.slots(d)) == True{} : Bool}:
1199  %Equal.sym(U32, U32.sub(U32.shln(1, d), 1), U32{AP.lm(32n, d)}, AP.mask_lm(d)) : {Nat.is_lt(U32.to_nat(U32.and(i, _)), A.Arrays.slots(d)) == True{} : Bool}
1200  AP.u32_mask_lt(i, d)