Store entfernen

gegeben eine $\phi$ Formel mit Teilausdruck store(a, i, e),

ersetze diesen durch a' und füge Constraints hinzu:

select(a', i) = e $\wedge$ $\forall$j $\neq$ i : select(a', j) = select(a', i).

da es sich um quantorenfreie Formeln handelt: j läuft über alle Index-Ausdrücke, die in der Formel vorkommen.