 More generally, let \((!\varphi, M)^\#\) be the limit (i.e., the first fixed point) of M under repeatedly announcing \(\varphi\) as long as it still true. In any game tree, the fixed-point \((!\rat , M)^\#\) has \(\rat\) true throughout. Its nodes contain the actual play computed by the Backward Induction algorithm (van Benthem 2014).