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.