80   ONE ("ONE" 999) and

    80   ONE ("ONE" 999) and

    81   ZERO ("ZERO" 999) and

    81   ZERO ("ZERO" 999) and

    82   pderivs_lang ("pdersl") and

    82   pderivs_lang ("pdersl") and

    83   UNIV1 ("UNIV\<^isup>+") and

    83   UNIV1 ("UNIV\<^isup>+") and

    84   Deriv_lang ("Dersl") and

    84   Deriv_lang ("Dersl") and

    85   deriv ("der") and

    86   deriv ("der") and

    86   derivs ("ders") and

    87   derivs ("ders") and

    87   pderiv ("pder") and

    88   pderiv ("pder") and

    88   pderivs ("pders") and

    89   pderivs ("pders") and

    89   pderivs_set ("pderss")

    90   pderivs_set ("pderss")

   371   (Brzozowski mentions this side-condition in the context of state complexity

   372   (Brzozowski mentions this side-condition in the context of state complexity

   372   of automata \cite{Brzozowski10}). Such side-conditions mean that if we

   373   of automata \cite{Brzozowski10}). Such side-conditions mean that if we

   373   define a regular language as one for which there exists \emph{a} finite

   374   define a regular language as one for which there exists \emph{a} finite

   374   automaton that recognises all its strings (see Definition~\ref{baddef}), then we

   375   automaton that recognises all its strings (see Definition~\ref{baddef}), then we

   375   need a lemma which ensures that another equivalent one can be found

   376   need a lemma which ensures that another equivalent one can be found

   377   lemmas make a formalisation of automata theory a hair-pulling experience.

   379   lemmas make a formalisation of automata theory a hair-pulling experience.

   378 

   380 

   379 

   381 

   380   In this paper, we will not attempt to formalise automata theory in

   382   In this paper, we will not attempt to formalise automata theory in

   381   Isabelle/HOL nor will we attempt to formalise automata proofs from the

   383   Isabelle/HOL nor will we attempt to formalise automata proofs from the