Error in the UNITY substitution rule for subscripted operators

UNITY, introduced by Chandy and Misra [ChM88], is a programming logic intended to reason about temporal properties of distributed programs. Despite the fact that UNITY does not have the full power of, for example, linear temporal logic, it enjoys popularity due to its simplicity. There was however a serious problem with the Substitution Rule. The logic is incomplete without the rule, and with the rule it is inconsistent. Latterly Beverly Sanders introduced the concept of strongest invariant and proposed a new definition for UNITY [San91] that fixes the problem with the Substitution Rule. For the benefit of program union, she also introduced the concept of subscripted properties and claimed a generalized version of Substitution Rule for the subscripted properties. This report presents an example that shows that the latter claim is false. A proposal as how to fix this follows.