Successor-state axiom ($F_{t+1}\leftrightarrow {\mathrm{Add}}_F(t)\vee (F_t\wedge \neg {\mathrm{Delete}}_F(t))$)

A logical equivalence characterizing exactly when a planning fluent is true after one step. Here ${\mathrm{Add}}_F$ and ${\mathrm{Delete}}_F$ are disjunctions of selected actions with the respective effects, under a suitable action-conflict policy. The persistence term excludes spontaneous changes and captures the relevant frame axiom. An implication from add effects alone would not constrain all other state changes.