2.1 The programming language studied in this book is so simple that it suffices to use just stores as states of the run-time system; we do not need the extra power of having environments in addition to stores.

2.1.1 The discussion of the equality and disequality operations in this subsection is very technical. Because the details are not needed until later, you may just skim it, but you should read the notes for Section 1.6.3.

2.2 The semantics that we begin to define here is enormously more simple than what is usual in the literature, and has the additional advantages that it can be directly executed, so that programs can be run, and it also supports mechanical correctness proofs using OBJ.