777   This allows us to prove a version of Arden's Lemma on the level of equations.

   777   This allows us to prove a version of Arden's Lemma on the level of equations.

   778 

   778 

   779   \begin{lmm}\label{ardenable}

   779   \begin{lmm}\label{ardenable}

   780   Given an equation @{text "X = rhs"}.

   780   Given an equation @{text "X = rhs"}.

   781   If @{text "X = \<Union>\<calL> ` rhs"},

   781   If @{text "X = \<Union>\<calL> ` rhs"},

   784   @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.

   784   @{text "X = \<Union>\<calL> ` (Arden X rhs)"}.

   785   \end{lmm}

   785   \end{lmm}

   786   

   786   

   787   \noindent

   787   \noindent

   788   Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,

   788   Our @{text ardenable} condition is slightly stronger than needed for applying Arden's Lemma,

  1096 

  1096 

  1097   \noindent

  1097   \noindent

  1098   Much more interesting, however, are the inductive cases. They seem hard to solve 

  1098   Much more interesting, however, are the inductive cases. They seem hard to solve 

  1099   directly. The reader is invited to try. 

  1099   directly. The reader is invited to try. 

  1100 

  1100 

  1101   Our first proof will rely on some

  1104   Our first proof will rely on some

  1102   \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will 

  1105   \emph{tagging-functions} defined over strings. Given the inductive hypothesis, it will 

  1103   be easy to prove that the \emph{range} of these tagging-functions is finite. 

  1106   be easy to prove that the \emph{range} of these tagging-functions is finite. 

  1104   The range of a function @{text f} is defined as 

  1107   The range of a function @{text f} is defined as 

  1105   

  1108