equal
deleted
inserted
replaced
398 |
398 |
399 \noindent |
399 \noindent |
400 we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations |
400 we can prove for @{text "X\<^isub>2\<^isub>.\<^isub>.\<^isub>n"} that the following equations |
401 % |
401 % |
402 \begin{equation}\label{inv1} |
402 \begin{equation}\label{inv1} |
403 @{text "X\<^isub>i = L(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> L(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}. |
403 @{text "X\<^isub>i = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>q, CHAR c\<^isub>i\<^isub>q)"}. |
404 \end{equation} |
404 \end{equation} |
405 |
405 |
406 \noindent |
406 \noindent |
407 hold. Similarly for @{text "X\<^isub>1"} we can show the following equation |
407 hold. Similarly for @{text "X\<^isub>1"} we can show the following equation |
408 % |
408 % |
409 \begin{equation}\label{inv2} |
409 \begin{equation}\label{inv2} |
410 @{text "X\<^isub>1 = L(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> L(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> L(\<lambda>(EMPTY))"}. |
410 @{text "X\<^isub>1 = \<calL>(Y\<^isub>i\<^isub>1, CHAR c\<^isub>i\<^isub>1) \<union> \<dots> \<union> \<calL>(Y\<^isub>i\<^isub>p, CHAR c\<^isub>i\<^isub>p) \<union> \<calL>(\<lambda>(EMPTY))"}. |
411 \end{equation} |
411 \end{equation} |
412 |
412 |
413 \noindent |
413 \noindent |
414 The reason for adding the @{text \<lambda>}-marker to our equational system is |
414 The reason for adding the @{text \<lambda>}-marker to our equational system is |
415 to obtain this equation, which only holds in this form since none of |
415 to obtain this equation, which only holds in this form since none of |