def AP.slots_pos

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

import Base
import bend-osdev-array@0.1.0.1/array.bend as A
import bend-osdev-u32@0.1.0.0/LAWS_order.bend as UO

790def AP.slots_pos(d: Nat) -> {Nat.is_lt(0n, A.Arrays.slots(d)) == True{} : Bool}:
791  match d:
792    case 0n:
793      {==}
794    case 1n+ +p:
795      UO.nat_lt_le_trans(0n, 1n, Nat.double(A.Arrays.slots(p)), {==}, AP.dpos(A.Arrays.slots(p), AP.slots_pos(p)))