2438   about regular languages. The formalisation of derivatives and partial

  2438   about regular languages. The formalisation of derivatives and partial

  2439   derivatives shown in Section~\ref{derivatives} consists of 390 lines of

  2439   derivatives shown in Section~\ref{derivatives} consists of 390 lines of

  2440   code.  The closure properties in Section~\ref{closure} (except Theorem~\ref{subseqreg}) 

  2440   code.  The closure properties in Section~\ref{closure} (except Theorem~\ref{subseqreg}) 

  2441   can be established in

  2441   can be established in

  2442   190 lines of code. The Continuation Lemma and the non-regularity of @{text "a\<^sup>n b\<^sup>n"} 

  2442   190 lines of code. The Continuation Lemma and the non-regularity of @{text "a\<^sup>n b\<^sup>n"} 

  2444   The algorithm for solving equational systems, which we

  2444   The algorithm for solving equational systems, which we

  2445   used in the first direction, is conceptually relatively simple. Still the

  2445   used in the first direction, is conceptually relatively simple. Still the

  2446   use of sets over which the algorithm operates means it is not as easy to

  2446   use of sets over which the algorithm operates means it is not as easy to

  2447   formalise as one might hope. However, it seems sets cannot be avoided since

  2447   formalise as one might hope. However, it seems sets cannot be avoided since

  2448   the `input' of the algorithm consists of equivalence classes and we cannot

  2448   the `input' of the algorithm consists of equivalence classes and we cannot