2030 \noindent |
2030 \noindent |
2031 holds for any strings @{text "s\<^isub>1"} and @{text |
2031 holds for any strings @{text "s\<^isub>1"} and @{text |
2032 "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} |
2032 "s\<^isub>2"}. Therefore @{text A} and the complement language @{term "-A"} |
2033 give rise to the same partitions. So if one is finite, the other is too, and |
2033 give rise to the same partitions. So if one is finite, the other is too, and |
2034 vice versa. As noted earlier, our algorithm for solving equational systems |
2034 vice versa. As noted earlier, our algorithm for solving equational systems |
2035 actually calculates the regular expression for the complement language. |
2035 actually calculates a regular expression for the complement language. |
2036 Calculating this regular expression via |
2036 Calculating such a regular expression via |
2037 automata using the standard method would be quite involved. It includes the |
2037 automata using the standard method would be quite involved. It includes the |
2038 steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text |
2038 steps: regular expression @{text "\<Rightarrow>"} non-deterministic automaton @{text |
2039 "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"} |
2039 "\<Rightarrow>"} deterministic automaton @{text "\<Rightarrow>"} complement automaton @{text "\<Rightarrow>"} |
2040 regular expression. Clearly not something you want to formalise in a theorem |
2040 regular expression. Clearly not something you want to formalise in a theorem |
2041 prover in which it is cumbersome to reason about automata. |
2041 prover in which it is cumbersome to reason about automata. |