The definition of deadend states is not clear in the literature. That's why in the VRS course, we distinguish between deadend and finally deadend states to make precise what we mean. However, that distinction has been only recently introduced, and was not there some years ago. At that time, "deadend state" has been derived from the context, i.e., temporal logics have trouble with finally deadend states, and also induction hast that problem. The computation shown above computes the finally deadend states, since the states that have no outgoing transition are clearly those that satisfy []false while the finally deadend states are those that satisfy A false.