 It should be noted that it follows from (TRL1–2) that \(\TRL_s(t) = \TRL_s(\next_s(t)) = \TRL_s(\next_{s}^2(t)) = \ldots\) and in general that \(\next_{s}^n(t) \in \TRL_s(t)\) for any natural number \(n\). In addition, it should be mentioned that since the branching-time system is backwards linear, there is no need to specify the chronicle in \(back(t)\).