Proving that no finite automaton can recognize a Dyck language I was reading up on finite automata and I came across an interesting fact near the end of the Wikipedia page.


  The classic example of a simply described language that no DFA can
  recognize is bracket or Dyck language, i.e., the language that
  consists of properly paired brackets such as word "(()())".
  Intuitively, no DFA can recognize the Dyck language because DFAs are
  not capable of counting: [...]


Although it is very intuitive the argument they gave, I was wondering if there were a formal proof I could read for this, or if simple enough, reconstruct.

I tried Googling around for a proof, but I think I am missing some sort of a keyword in my search because nothing useful is coming up, it this proof trivial or intuitive enough that no papers have been published on it?
Consider a Dyck language $L$ with $k$ types of parentheses, one of them $()$. If $L$ were regular then $L \cap (^*)^*$ would be regular, but this is just the well-known non-regular language $a^nb^n$ (with $a,b$ replaced by $(,)$).

There are many ways to prove that $L' = \{a^nb^n : n \geq 0\}$ isn't regular. Here is one. Suppose that $A$ is a DFA recognizing $L'$, with states $Q$, initial state $q_0$, accepting states $F$, and transition function $\delta$. Let $q(i) = \delta(q_0,a^i)$. If $i &lt; j$ then $q(i) \neq q(j)$, since otherwise $\delta(q_0,a^ib^i) = \delta(q_0,a^jb_i)$ although the former is in $F$ while the latter isn't. This implies the absurd conclusion that $Q$ must be infinite.