# proving an automaton language for the language over $\{a,b\}^{*}$ : $w\in L$ if $aa$ is not an infix of $w$ ($aa$ doesn't appear in $w$)

I built the next automaton:

I have problem to prove $L = L(q_0)\cup L(q_1)$, (when $L(q)$ denotes words $w$ such that $\hat{\delta}(q_0,w) = q$ at a given DFA) because semantically $L(q_0)$ is the language of words over $\{a,b\}^*$ which don't start with $a$, and $L(q_1)$ is the language of words which start with $a$ (by the way, one could also say $L(q_0)$ are the words which don't end in $a$ and $L(q_1)$ are the words which end with $a$).I failed to understand why $L(q_0)\cup L(q_1) = L$.

My second question, Is it "valid" to prove that $L(q_2) = L^c$, generally speaking, does it valid to prove $\bigcup_{q\in F^c} L(q) = L^c$ in order to prove $L(A)= L$ ? (when $F$ is the set of finite states of an automaton A)

• You should improve your question a bit. First of all in your title you want to "prove an automaton"? You pro want to prove that your automaton is correct for the language $L$. Second, $\in$ or $\notin$ should not be confused with "is an infix of" or "is not an infix of", respectively. Finally, the notation $L(q)$ seems weird, it was not clear to me if it is the set of words that run on the DFA starting at $q$ or ending in $q$. – ttnick Aug 8 '18 at 15:23
• So you want to prove that $L(\mathcal{A}) = \{w \in \{a, b\}^\ast \mid aa \text{ is not an infix of } w\} =: L$. You can do this via induction, and you actually have some sort of induction hypothesis stated in your question: Show that for every word $w \in \{a, b\}^\ast$ with run $(r_0, \ldots, r_n)$ it holds that: $r_n = q_0$ if $w$ does not contain $aa$ and the last symbol was not $a$, $r_n = q_1$ if $w$ does not contain $aa$ and the last symbol was $a$, $r_n = q_2$ if $w$ does contain $aa$. – ttnick Aug 8 '18 at 15:29
• As you have stated you can also prove that $L^C$, i.e. the langauage of all words containing $aa$ is actually accepted by the same automaton, just with accepting and non-accepting states flipped, but this does not simplifies the induction above. – ttnick Aug 8 '18 at 15:29
• There is an automatic way to prove what you want. Complement your automaton so that it generates $\Sigma^*aa\Sigma^*$, then use known algorithms to show that your automaton indeed generates $\Sigma^*aa\Sigma^*$ (convert the regular expression to an NFA and then to a DFA, compute the symmetric difference DFA, and show that no accepting state is reachable from the initial state using BFS/DFS). – Yuval Filmus Aug 9 '18 at 13:56
• It's not clear what you mean by a "semantic" proof. The semantic proof is to describe the languages of the states, i.e., $L(q_0),L(q_1),L(q_2)$. Then you need to prove that your semantic description is correct, by induction. Compare this to the purely syntactic proof in my preceding comment. – Yuval Filmus Aug 9 '18 at 13:57