Lately I have been working on formalizing APL. One of the core problems related to the formalization of APL is how indexing into various arrays that have been derived from other arrays works. In particular, one of the more interesting aspects is the relation between what is known as an