Adequacy
In this handout we explicitly stated that AF need not be surjective (onto). Were we to require AF to be surjective, then we would require that every abstract state have some concrete representation, i.e., that AF is adequate. Requiring AF to be adequate makes very good sense since you might like to know that every abstract state you have modeled is implemented by some concrete state. Some refinement methods like VDM require that AF be adequate. And, in proving the correctnesss of an abstract data type, we usually require AF to be adequate for the concrete representation type.
As mentioned, we also do not require adequacy in the
sense
of having every state transition of A be implemented in terms
of one in C. Rather, we only require that every
state transition in C relate to some state transition of A.
(C cannot do anything not permitted by A.)
This laxity is in contrast to
how we defined whether one binary relation, 
,
satisfies another, 
; we required that for each input
related by , should be defined. This requirement gets
at the adequacy of viewed as an implementation of .
Taking this last point to an extreme, we do not even require that every action in A actually be ``implemented'' by some action (or sequence of actions) in C. In other words there can be state transitions, all associated with a particular action of A, that have no correspondence are not adequately represented) in C.
You will see later in the course when we cover Z and CSP that other state machine-based models impose different kinds of adequacy restrictions in defining a refinement/correctness relation between two machines.
Abstraction Relations
Some people prefer to use abstraction relations or abstraction mappings more generally than functions. There are examples where it is easier, more convenient, or more natural to map a concrete state to a set of abstract states. As mentioned, however, you would lose the substitution property of abstraction functions.
Auxiliary Variables
Sometimes it is not so straightforward to prove a concrete machine satisfies an abstract machine in terms of just the state variables of the concrete machine. In this case, you need to introduce auxiliary variables (sometimes called dummy variables or history variables in the literature). The need for auxiliary variables in such proofs is especially common for reasoning about concurrent programs.