 The last column of each line of the proof contains its condition, i.e., a set of abnormalities \(\mathrm{COND} \subseteq \Omega\) that encodes the assumptions used to derive the formula in the second column of the line: each \(\mathsf{ab} \in \mathrm{COND}\) is assumed to be false. The generic rule RU (rule unconditional) represents any inference that is licenced by LLL. The generic rule RC (rule conditional) follows scheme [‡] where \(\mathsf{ab}\) is pushed to the condition of the line. Sometimes there are good reasons to consider assumptions as violated in which case the corresponding lines are ✓-marked as retracted. This is clearly the case if the condition of a line is \(\mathrm{COND}\) while for a \(\{\mathsf{ab}_1, \dotsc, \mathsf{ab}_n\} \subseteq \mathrm{COND}\), \(\mathsf{ab}_1 \vee \mathsf{ab}_2 \vee \ldots \vee \mathsf{ab}_n\) is derived without defeasible steps (i.e., on the condition ∅). This means that (at least) one of the formulas in \(\mathrm{COND}\) is false. Thus, line 2 is marked as retracted when we reach line 4 of the proof. In view of this behavior, dynamic proofs are internally dynamic: even if no new premises are introduced, the addition of new lines may cause the retraction of previous lines of a proof. 