You wrote:
\lnot (Enabled<<A>>_v)' denotes a step that disables <<A>>_v
A step is a pair of states. The formula \lnot (Enabled<<A>>_v)' is an
action formula, meaning it is a predicate on steps. This predicate is
true for a pair of states <<s, t>> iff <<A>>_v is disabled in state t.
"Denotes" means gives a name to or to designate. The only way to
denote a step is to say what its two states are, which means to say
what values each of them assign to variables. By "state" we usually
mean the state of a system, which assigns a values to each of the
system's variables. One can denote a step by an action formula like
the following, which assumes that the system's variables are x, y,
and z:
/\ x = 7
/\ y = {"a"}
/\ z = <<1, 2>>
/\ x' = 42
/\ y' = {}
/\ z' = <<1, 2, 3>>
\lnot (Enabled<<A>>_v)' is not such a formula, and it does not denote
a step.
If this isn't enough to help you understand the definition of TNext(t),
you may have jumped into Chapter 9 without a proper understanding of
the first few chapters of the book.
Cheers,
Leslie