369   holds, whereby @{text "\<calL> ` rs"} stands for the 

   369   holds, whereby @{text "\<calL> ` rs"} stands for the 

   370   image of the set @{text rs} under function @{text "\<calL>"}.

   370   image of the set @{text rs} under function @{text "\<calL>"}.

   371 *}

   371 *}

   372 

   372 

   373 

   373 

   375 

   375 

   376 text {*

   376 text {*

   377   The key definition in the Myhill-Nerode theorem is the

   377   The key definition in the Myhill-Nerode theorem is the

   378   \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two 

   378   \emph{Myhill-Nerode relation}, which states that w.r.t.~a language two 

   379   strings are related, provided there is no distinguishing extension in this

   379   strings are related, provided there is no distinguishing extension in this