3 imports "../Myhill" "LaTeXsugar"

     3 imports "../Myhill" "LaTeXsugar" 

   502   the \emph{arden-operation}, which takes an equivalence class @{text X} and

   502   the \emph{arden-operation} for an equation of the form @{text "X = rhs"}:

   503   a rhs of an equation.

   503   

   504 

   504   \begin{center}

   505   \begin{center}

   505   \begin{tabular}{rc@ {\hspace{2mm}}r@ {\hspace{1mm}}l}

   506   @{thm arden_op_def}

   506   @{thm (lhs) Arden_def} & @{text "\<equiv>"}~~\mbox{} & \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "let"}}\\ 

   507   \end{center}

   507    & & @{text "rhs' ="} & @{term "rhs - {Trn X r | r. Trn X r \<in> rhs}"} \\

   508 

   508    & & @{text "r' ="}   & @{term "STAR (\<Uplus> {r. Trn X r \<in> rhs})"}\\

   509   \noindent

   509    & &  \multicolumn{2}{@ {\hspace{-2mm}}l}{@{text "in"}~~@{term "append_rhs_rexp rhs' r'"}}\\ 

   510   The term left of $\triangleright$ deletes all terms of the form @{text "(X, r)"};

   510   \end{tabular}

   511   the term on the right calculates first the combinded regular expressions for all

   511   \end{center}

   512   @{text r} in the @{text "(X, r)"}, forms the star and appends it to the remaining

   512 

   513   terms in the @{text rhs}. It can be easily seen that this operation mimics Arden's

   513   \noindent

   514   lemma on the level of equations.

   514   We first delete all terms of the form @{text "(X, r)"} from @{text rhs};

   515   

   515   then we calculate the combinded regular expressions for all @{text r} coming 

   516   from the deleted @{text "(X, r)"}, and take the @{const STAR} of it;

   517   finally we append this regular expression to @{text rhs'}. It can be easily seen 

   518   that this operation mimics Arden's lemma on the level of equations.

   519   

   520 

   521   \begin{center}

   522   @{thm Subst_def}

   523   \end{center}