Pushdown automaton accepting $\{a,b\}^*$ with twice as many $a$s as $b$s Design a pushdown automaton that can accept


  $$\{w|w\in\{a,b\}^*\text{ and $w$ has twice as many $a$s as $b$s}\} \, .$$


I have a solution as the following. The notation seems to follow "An Introduction to Formal Languages and Automaton" by  Peter Linz, where $\delta$ is the transition function with three arguments: current state, input, current stack top; $\lambda$ as the second argument of $\delta$ means empty string $\epsilon$ in some other textbooks, and $\lambda$ as the third argument of $\delta$ means the transition ignores the current stack top. The $\lambda$ on the right hand side means "pop the top element of the stack".



I have several confusions,

1) I am not sure what the right-hand side notation means. For example, does the right hand side of $\delta(q_1,a,A)=\{[q_2，A]\}$ means pushing an $A$ into the stack? Or it means the stack top stays $A$ without a new $A$ pushed to it? 

If this means "push", then what about $\delta(q_1,a,C)=\{[q_2，C]\}$? $C$ seems to mark the bottom of the stack. We push another $C$ to the stack when there is already a $C$ in it?

2) I think the solution might be wrong. I don't see why it accepts $aab$. Tracing this string, I think the transition is the following based on the design (if the big letter at the right-hand side means pushing a new symbol),

$q_0,\lambda \to_\lambda q_1,C\to_a q_2,CC \to_\lambda q_1,ACC \to_a q_2,AACC \to_\lambda q_1,AAACC \to_b q_1,AACC$

It is very strange and I feel very confused. Hope someone can help! Thank you!
When in doubt, one should always consult the definitions.

In this case, this is Definition 7.1 of the book by Peter Linz.

It states that $$\delta : Q \times (\Sigma \cup \{ \lambda \}) \times \Gamma \rightarrow \textrm{finite subsets of } Q \times \Gamma^*$$
Thus, $\delta(q,a,A) = \{[q_1,w_1], \ldots, [q_k,w_k\}$ means that when a pushdown automaton is in state $q$ and sees an $a$ on input (where $a$ may be an input or the empty string $\lambda$), then it can enter any one of the states $q_1$ to $q_k$ and replace $A$ by the corresponding string of stack symbols $w_i$.

Therefore, a pushdown automaton can push a string $w$ to the stack by reading $\lambda$ and replacing it by $w$. Or it can pop the top symbol $b$ by seeing $b$ on the stack and replacing it by $\lambda$.