Our exit game defines a set of “exitable outputs” given a transaction$ t. For example, spent outputs are not exitable in our rules. We formally define the properties that this game must satisfy. We call these properties “safety” and “liveness”, because they’re largely analogous.
The safety rule, in English, says “if an output was exitable at some time and is not spent in a later transaction, then it must still be exitable”. If we didn’t have this condition, then it might be possible for a user to receive money but not be able to spend or exit from it later.
The liveness rule basically says that “if an output was exitable at some time and is spent later, then immediately after that spend, either it’s still exitable or all of the spend’s outputs are exitable, but not both”.
The second part probably makes sense - if something is spent, then all the resulting outputs should be exitable. The first case is special - if the spend is invalid, then the outputs should not be exitable and the input should still be exitable. So a short way to describe “liveness” is that all “canonical” transactions should impact the set of exitable transactions.