 A slightly more complex automaton, the pushdown automaton, has rudimentary memory resources in the form a of stack of symbols that can be pushed or popped from the top, enabling it to keep track to some extent of what went on at earlier steps. Another result by van Benthem is that the type \({\langle}1{\rangle}\) quantifiers accepted by pushdown automata are precisely those for which the corresponding binary relation between numbers is definable (with first-order means) in additive arithmetic, i.e., in the model \((N,+)\), where \(N = \{0,1,2,\ldots\}\). An example is \(Q^R\) (or its relativization most): we have \(Q^R(m,n) \Leftrightarrow m &lt; n\), and the right hand side is definable in \((N,+)\) by \(\exists x (x \neq 0 \wedge m + x =  n)\).[18]