equal
deleted
inserted
replaced
535 @{term "[] \<notin> A"}. However we will need the following `reversed' |
535 @{term "[] \<notin> A"}. However we will need the following `reversed' |
536 version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \<cdot> X"} to |
536 version of Arden's Lemma (`reversed' in the sense of changing the order of @{term "A \<cdot> X"} to |
537 \mbox{@{term "X \<cdot> A"}}).\footnote{The details of the proof for the reversed Arden's Lemma |
537 \mbox{@{term "X \<cdot> A"}}).\footnote{The details of the proof for the reversed Arden's Lemma |
538 are given in the Appendix.} |
538 are given in the Appendix.} |
539 |
539 |
540 \begin{lmm}[(Reversed Arden's Lemma)]\label{arden}\mbox{}\\ |
540 \begin{lmm}[Reversed Arden's Lemma]\label{arden}\mbox{}\\ |
541 If @{thm (prem 1) reversed_Arden} then |
541 If @{thm (prem 1) reversed_Arden} then |
542 @{thm (lhs) reversed_Arden} if and only if |
542 @{thm (lhs) reversed_Arden} if and only if |
543 @{thm (rhs) reversed_Arden}. |
543 @{thm (rhs) reversed_Arden}. |
544 \end{lmm} |
544 \end{lmm} |
545 |
545 |