thys2/Paper/Paper.thy
changeset 463 421397f267b9
parent 462 d9b672c4c0ac
child 464 e6248d2c20c2
equal deleted inserted replaced
462:d9b672c4c0ac 463:421397f267b9
   966      %
   966      %
   967      \def\xll{\xrightarrow{\_\backslash{} [a, a, a]}}%%
   967      \def\xll{\xrightarrow{\_\backslash{} [a, a, a]}}%%
   968      %
   968      %
   969      \begin{equation}\label{derivex}
   969      \begin{equation}\label{derivex}
   970      (a + aa)^* \quad\xll\quad
   970      (a + aa)^* \quad\xll\quad
   971       \underbrace{\mbox{$(\ONE + \ONE{}a) \cdot (a + aa)^*$}}_{r} \;+\;
   971       \underbrace{\mbox{$(\ONE + a) \cdot (a + aa)^*$}}_{r} \;+\;
   972      ((a + aa)^* + \underbrace{\mbox{$(\ONE + \ONE{}a) \cdot (a + aa)^*$}}_{r})
   972      ((a + aa)^* + \underbrace{\mbox{$(\ONE + a) \cdot (a + aa)^*$}}_{r})
   973      \end{equation}
   973      \end{equation}
   974 
   974 
   975      \noindent This is a simpler derivative, but unfortunately we
   975      \noindent This is a simpler derivative, but unfortunately we
   976      cannot make any further simplifications. This is a problem because
   976      cannot make any further simplifications. This is a problem because
   977      the outermost alternatives contains two copies of the same
   977      the outermost alternatives contains two copies of the same