Ensure that the write effects of different iterations of a foreach loop are disjoint

[reprogrammer]

DPJizer makes the write effects of a foreach loop disjoint across different iterations of the loop by ensuring the the loop index variable appears in every write effect. For example, given a DPJ foreach loop with index variable j and a write effect e = writes Pi7[idx3 <- j], DPJizer has to come up with a set of values for region variables that make j appear in e. In this simple case, either Pi7 should contain the RPL element [j] directly or Pi7 should contain the RPL element [idx3] so that [j] appears in the effect after applying the substitution [idx3 <- j].