hypo-withTests-ndet.tex

   1 \subsection{ðÒÏÓÔÙÅ ÍÏÄÅÌÉ}
   2 \label{sec:simple-models}
   3
   4 úÄÅÓØ ÍÙ ÒÁÓÓÍÏÔÒÉÍ ËÌÁÓÓ ÍÏÄÅÌÅÊ \KAT, ÏÓÎÏ×ÁÎÎÙÈ ÎÁ ÛËÁÌÁÈ ëÒÉÐËÅ, ×
   5 ÎÅËÏÔÏÒÏÍ ÓÍÙÓÌÅ <<ÅÓÔÅÓÔ×ÅÎÎÏ>> ÕÞÉÔÙ×ÁÀÝÉÅ ÎÁËÌÁÄÙ×ÁÅÍÙÅ ÕÓÌÏ×ÉÑ
   6 (××ÉÄÕ ÐÏÓÔÕÌÁÔÏ× Ï ÓÅÍÁÎÔÉËÅ ÐÒÏÇÒÁÍÍ).
   7
   8 íÙ ÐÒÅÄÌÏÖÉÍ ÔÁËÉÅ ÍÏÄÅÌÉ ÄÌÑ ÓÏÞÅÔÁÎÉÊ ÍÏÎÏÉÄÎÙÈ ÕÓÌÏ×ÉÊ É ÕÓÌÏ×ÉÊ
   9 ÓÄ×ÉÇÏ× (ÎÁÛÅ ÉÓÓÌÅÄÏ×ÁÎÉÅ ÓÆÏËÕÓÉÒÏ×ÁÎÏ ÉÍÅÎÎÏ ÎÁ ÔÁËÉÈ ÓÌÕÞÁÑÈ).
  10
  11 îÁÓ ÂÕÄÅÔ ÉÎÔÅÒÅÓÏ×ÁÔØ ×ÏÐÒÏÓ Ï ÔÏÍ, ÎÁÓËÏÌØËÏ ÉÈ ÍÏÖÎÏ ÓÞÉÔÁÔØ
  12 <<ÂÁÚÉÓÎÙÍÉ>> ÍÏÄÅÌÑÍÉ ÄÌÑ ÛÉÒÏËÉÈ ËÌÁÓÓÏ× \KAT (\KAT, \KATc, \RKAT,
  13 ÏÇÒÁÎÉÞÅÎÎÙÈ ÄÏÐÏÌÎÉÔÅÌØÎÙÍÉ ÏÇÒÁÎÉÞÅÎÉÑÍÉ),
  14 \te ÔÁËÉÍÉ, ÎÁ ËÏÔÏÒÙÈ ÄÏÓÔÁÔÏÞÎÏ ÐÒÏ×ÅÒÉÔØ ×ÅÒÎÏÓÔØ ÒÁ×ÅÎÓÔ×Á ÄÌÑ
  15 ÔÏÇÏ, ÞÔÏÂÙ ÕÂÅÄÉÔØÓÑ × ÔÏÍ, ÞÔÏ ÏÎÏ ×ÅÒÎÏ ×Ï ×Ó£Í ËÌÁÓÓÅ. (ëÁË ÜÔÏ
  16 ÂÙÌÏ × ÓÌÕÞÁÅ Ó ÌÅÎÔÁÍÉ ÄÌÑ Á×ÔÏÍÁÔÏ×\T ÓÍ.~òÁÚÄÅÌ~\ref{sec:tapes}.)
  17
  18 \subsubsection{õÄÏ×ÌÅÔ×ÏÒÑÀÝÉÅ ÍÏÎÏÉÄÎÙÍ ÕÓÌÏ×ÉÑÍ}
  19
  20 ðÕÓÔØ $\Sigma$ É $T$\T ËÏÎÅÞÎÙÅ ÁÌÆÁ×ÉÔÙ (<<ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×>> É
  21 <<ÂÁÚÏ×ÙÈ ÔÅÓÔÏ×>>).
  22
  23 %% ðÕÓÔØ $\mo M = (Q_{\mo M}; \cdot, 1_{\mo M})$\T
  24 %% ÎÅËÏÔÏÒÙÊ ÍÏÎÏÉÄ Ó ÐÏÒÏÖÄÁÀÝÉÍÉ ÜÌÅÍÅÎÔÁÍÉ $\Sigma$.
  25
  26 ðÕÓÔØ
  27 $\Emonoid \in \MoEqua_{\Sigma}$\T ÍÏÎÏÉÄÎÙÅ ÕÓÌÏ×ÉÑ, $\mo M_0 = \mo
  28 M_0(\Sigma, \Emonoid)$\T ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÊ Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ (Ó
  29 ÐÏÒÏÖÄÁÀÝÉÍÉ ÜÌÅÍÅÎÔÁÍÉ $\Sigma$ É ÓÏÏÔÎÏÛÅÎÉÑÍÉ $\Emonoid$).
  30 %÷ Î£Í ÓÏÂÌÀÄÁÅÔÓÑ ÚÁËÏÎ ÌÅ×ÏÇÏ ÓÏËÒÁÝÅÎÉÑ.
  31
  32 \begin{definition}\label{def:SIMPLET-under-E}
  33   $\Result_{\mo M_0}(\xi) \eqdef \relReg_{\kf F_{\mo M_0}(\xi)}$
  34
  35   $\SIMPLET_{\Sigma,T}(\Emonoid) \eqdef \{
  36    \Result_{\mo M_0}(\xi) \mid \xi \text{\T ÐÒÏÉÚ×ÏÌØÎÁÑ ÏÃÅÎËÁ}
  37   \}$,
  38   ÇÄÅ $\mo M_0$\T ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÊ $\Emonoid$ Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ.
  39 \end{definition}
  40
  41 \begin{definition}
  42   âÕÄÅÍ ÇÏ×ÏÒÉÔØ, ÞÔÏ ÛËÁÌÁ ëÒÉÐËÅ~$\kf F$
  43   ÎÁÄ~$\Sigma, T$ ÕÄÏ×ÌÅÔ×ÏÒÑÅÔ
  44   ÕÓÌÏ×ÉÑÍ $\Phi$, ÅÓÌÉ ÏÓÎÏ×ÁÎÎÁÑ ÎÁ ÎÅÊ ÒÅÌÑÃÉÏÎÎÁÑ ÍÏÄÅÌØ \KAT
  45   $\relReg_{\kf F}$ ÕÄÏ×ÌÅÔ×ÏÒÑÅÔ $\Phi$.
  46 \end{definition}
  47 \begin{remark}
  48   ìÀÂÁÑ  $\kf F_{\mo M}(\xi)$ ÕÄÏ×ÌÅÔ×ÏÒÑÅÔ $\Emonoid$.
  49 \end{remark}
  50 \begin{proposition}\label{prop:RELT-SIMPLET}
  51   åÓÌÉ ×ÅÒÎÏ, ÞÔÏ ×Ï ×ÓÑËÉÊ ÏÔÒÅÚÏË ÌÀÂÏÊ
  52   ÛËÁÌÙ ëÒÉÐËÅ ÎÁÄ~$\Sigma$, ÕÄÏ×ÌÅÔ×ÏÒÑÀÝÅÊ $\Emonoid$,
  53   ÍÏÖÎÏ ÇÏÍÏÍÏÒÆÎÏ
  54   ×ÌÏÖÉÔØ ÎÅËÏÔÏÒÙÊ ÏÔÒÅÚÏË $\kf F_{\mo M_0}$ (ÔÁË, ÞÔÏÂÙ ËÏÎÃÙ ÐÅÒÅÛÌÉ
  55   × ËÏÎÃÙ), ÔÏ
  56   $$
  57   \SIMPLET_{\Sigma,T}(\Emonoid) \models s =t
  58   \iff
  59   (\RELT_{\Sigma,T}|\Emonoid)  \models s =t
  60   $$
  61 \end{proposition}
  62 \begin{proof}
  63   óÐÒÁ×Á ÎÁÌÅ×Ï ÔÒÉ×ÉÁÌØÎÏ ($\SIMPLET$ ÓÏÓÔÏÉÔ ÉÚ ÒÅÌÑÃÉÏÎÎÙÈ ÍÏÄÅÌÅÊ,
  64   ÏÓÎÏ×ÁÎÎÙÈ ÎÁ ÛËÁÌÁÈ ëÒÉÐËÅ).
  65
  66   óÌÅ×Á ÎÁÐÒÁ×Ï. ðÒÅÄÐÏÌÏÖÉÍ, ÞÔÏ ÌÅ×ÁÑ ÞÁÓÔØ ×ÅÒÎÁ, Á ÐÒÁ×ÁÑ ÞÁÓÔØ\T
  67   ÎÅÔ:
  68   ÎÁÛÌÁÓØ ÛËÁÌÁ
  69   ëÒÉÐËÅ $\kf F'(\xi') = (Q', m')$ ÎÁÄ $\Sigma,T$, ÕÄÏ×ÌÅÔ×ÏÒÑÀÝÁÑ $\Emonoid$, ÔÁËÁÑ,
  70   ÞÔÏ
  71   $$
  72   \relReg_{\kf F'} \models s \neq t,
  73   $$
  74   \te ÓÕÝÅÓÔ×ÕÅÔ $(u', v') \in Q' \times Q'$, ÔÁËÁÑ, ÞÔÏ ÌÉÂÏ $(u',v')
  75   \in \relI{s}_{\kf F'}$ É $(u',v') \notin \relI{t}_{\kf F'}$,
  76   ÌÉÂÏ ÎÁÏÂÏÒÏÔ. (òÁÓÓÍÏÔÒÉÍ
  77   ÔÏÌØËÏ ÐÅÒ×ÙÊ ×ÁÒÉÁÎÔ.)
  78   ôÏÇÄÁ ÓÏÇÌÁÓÎÏ ÕÓÌÏ×ÉÀ ÎÁÊÄ£ÔÓÑ ÏÔÒÅÚÏË $[u,v]$ × $\kf F_{\mo M_0}$,
  79   ×ËÌÁÄÙ×ÁÀÝÉÊÓÑ × ÏÔÒÅÚÏË $[u', v']$ ÇÏÍÏÍÏÒÆÉÚÍÏÍ $h$. ôÏÇÄÁ ÐÏÌÏÖÉÍ
  80   $\xi(w) = \xi' (h(w))$ (Á ×ÎÅ ÏÔÒÅÚËÁ $[u,v]$ ÏÎÁ ÍÏÖÅÔ ÐÒÉÎÉÍÁÔØ
  81   ËÁËÉÅ ÕÇÏÄÎÏ ÚÎÁÞÅÎÉÑ). ôÏÇÄÁ $(u',v')
  82   \in \relI{s}_{\kf F_{\mo M_0}}$ É $(u',v') \notin \relI{t}_{\kf F_{\mo
  83       M_0}}$, ÞÔÏ ÐÒÏÔÉ×ÏÒÅÞÉÔ ÐÒÅÄÐÏÌÏÖÅÎÉÀ.
  84 \end{proof}
  85 \begin{remark}
  86   õÓÌÏ×ÉÅ õÔ×ÅÒÖÄÅÎÉÑ~\ref{prop:RELT-SIMPLET} ×ÅÒÎÏ ÄÌÑ $\Emonoid =
  87   \emptyset$\T
  88   ÓÌÕÞÁÑ Ó×ÏÂÏÄÎÏÇÏ ÍÏÎÏÉÄÁ: × Î£Í ÏÔÒÅÚËÉ ÉÍÅÀÔ ËÒÁÊÎÅ ÐÒÏÓÔÏÊ ×ÉÄ, ÌÉÎÅÊÎÙÊ.
  89 \end{remark}
  90 \begin{question}
  91   äÌÑ ËÁËÉÈ ÅÝ£ ÍÏÎÏÉÄÏ× ÜÔÏ ×ÅÒÎÏ? ÷ÅÒÎÏ ÌÉ ÄÌÑ Ó×ÏÂÏÄÎÏÇÏ
  92   ËÏÍÍÕÔÁÔÉ×ÎÏÇÏ? äÌÑ ËÁËÉÈ ÞÁÓÔÉÞÎÏ ËÏÍÍÕÔÁÔÉ×ÎÙÈ ÜÔÏ ×ÅÒÎÏ?
  93
  94   (ðÒÏÂÌÅÍÁ, ËÁË ÍÏÖÎÏ ÐÏÎÑÔØ, × ÎÅÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ $\kf F'$.)
  95 \end{question}
  96 ïÔ ÏÔ×ÅÔÁ ÎÁ ÜÔÏÔ ×ÏÐÒÏÓ ÚÁ×ÉÓÉÔ ÔÏ, ÎÁÓËÏÌØËÏ ÍÏÖÎÏ ÐÅÒÅÎÅÓÔÉ ÎÁ
  97 ÓÌÕÞÁÊ \KAT õÔ×.~\ref{prop:SIMPLE-REL}.
  98
  99 \subsubsection{õÄÏ×ÌÅÔ×ÏÒÑÀÝÉÅ ÍÏÎÏÉÄÎÙÍ ÕÓÌÏ×ÉÑÍ É ÕÓÌÏ×ÉÑÍ ÓÄ×ÉÇÏ×}
 100 ðÕÓÔØ $E = \Emonoid \wedge \Esh$, ÇÄÅ
 101 $\Emonoid \in \MoEqua_{\Sigma}$\T ÍÏÎÏÉÄÎÙÅ ÕÓÌÏ×ÉÑ,
 102 $\Esh \in \Shifts_{\Sigma,T}$\T ÕÓÌÏ×ÉÑ ÓÄ×ÉÇÏ×,
 103 $\mo M_0 = \mo
 104 M_0(\Sigma, \Emonoid)$\T ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÊ Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ (Ó
 105 ÐÏÒÏÖÄÁÀÝÉÍÉ ÜÌÅÍÅÎÔÁÍÉ $\Sigma$ É ÓÏÏÔÎÏÛÅÎÉÑÍÉ $\Emonoid$).
 106 %÷ Î£Í ÓÏÂÌÀÄÁÅÔÓÑ ÚÁËÏÎ ÌÅ×ÏÇÏ ÓÏËÒÁÝÅÎÉÑ.
 107
 108 \begin{definition}
 109   $\SIMPLET_{\Sigma,T}(E) \eqdef \{
 110    \Result_{\mo M_0}(\xi) \mid \kf F_{\mo M_0}(\xi) \text{
 111    ÕÄÏ×ÌÅÔ×ÏÒÑÅÔ } \Esh
 112   \}$,
 113   ÇÄÅ $\mo M_0$\T ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÊ $\Emonoid$ Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ.
 114 \end{definition}
 115
 116 \begin{proposition}\label{prop:RELT-SIMPLET-sh}
 117   åÓÌÉ ×ÅÒÎÏ, ÞÔÏ ×Ï ×ÓÑËÉÊ ÏÔÒÅÚÏË ÌÀÂÏÊ
 118   ÛËÁÌÙ ëÒÉÐËÅ ÎÁÄ~$\Sigma$, ÕÄÏ×ÌÅÔ×ÏÒÑÀÝÅÊ $\Emonoid$,
 119   ÍÏÖÎÏ ÇÏÍÏÍÏÒÆÎÏ
 120   ×ÌÏÖÉÔØ ÎÅËÏÔÏÒÙÊ ÏÔÒÅÚÏË $\kf F_{\mo M_0}$ (ÔÁË, ÞÔÏÂÙ ËÏÎÃÙ ÐÅÒÅÛÌÉ
 121   × ËÏÎÃÙ), ÔÏ
 122   $$
 123   \SIMPLET_{\Sigma,T}(\Emonoid \wedge \Esh) \models s =t
 124   \iff
 125   (\RELT_{\Sigma,T}|\Emonoid \wedge \Esh)  \models s =t
 126   $$
 127 \end{proposition}
 128 \begin{proof}
 129   ä-×Ï õÔ×.~\ref{prop:RELT-SIMPLET-sh} ÒÁÂÏÔÁÅÔ É × ÜÔÏÍ ÓÌÕÞÁÅ.
 130 \end{proof}
 131
 132 \subsubsection{ðÒÏÞÉÅ ×ÉÄÙ ÕÓÌÏ×ÉÊ}
 133
 134 \begin{question}
 135   íÏÖÎÏ ÐÒÅÄÌÏÖÉÔØ ÔÁËÉÅ <<ÅÓÔÅÓÔ×ÅÎÎÙÅ>> ÐÒÏÓÔÙÅ ÍÏÄÅÌÉ ÄÌÑ ÅÝ£
 136   ËÁËÏÇÏ-ÔÏ ×ÉÄÁ ÕÓÌÏ×ÉÊ?
 137 \end{question}
 138
 139
 140 %% \subsection{üÌÉÍÉÎÁÃÉÑ ÐÏÓÙÌÏË (ÄÏÐÕÝÅÎÉÊ)}
 141 %% \label{sec:withTests-elimination}
 142
 143
 144 %% \subsubsection{<<ðÏÞÔÉ ÎÅÚÁ×ÉÓÉÍÁÑ>> ÜÌÉÍÉÎÁÃÉÑ ÄÏÐÕÝÅÎÉÊ ×ÉÄÁ $pa =
 145 %%   a$.}
 146 %% \cite{KA-modular-elimination}, \cite{KAT-elimination}
 147
 148 \subsection{õÎÉ×ÅÒÓÁÌØÎÙÅ ÍÏÄÅÌÉ (ËÁÎÄÉÄÁÔÙ × Ó×ÏÂÏÄÎÙÅ)}
 149 \label{sec:hypo-plain-freeModels}
 150
 151 %\todo{[ïÐÒ?]}
 152
 153
 154 \subsubsection{õÎÉ×ÅÒÓÁÌØÎÁÑ ÍÏÄÅÌØ ÄÌÑ $\SIMPLET$ Ó ÍÏÎÏÉÄÎÙÍÉ ÕÓÌÏ×ÉÑÍÉ}
 155
 156 ÷ çÌÁ×Å~\ref{cha:free-withTests} ÂÙÌÏ ÐÏËÁÚÁÎÏ, ËÁË ÕÄÁ£ÔÓÑ ÐÏÓÔÒÏÉÔØ
 157 Ó×ÏÂÏÄÎÕÀ ÁÌÇÅÂÒÕ ×~\KATc (Ë ÔÏÍÕ ÖÅ, Ñ×ÌÑÀÝÕÀÓÑ
 158 Ó×ÏÂÏÄÎÏÊ ÁÌÇÅÂÒÏÊ, Ó ÏÄÎÏÊ ÓÔÏÒÏÎÙ, × \RKAT, Á Ó ÄÒÕÇÏÊ ÓÔÏÒÏÎÙ, É ×
 159 \KAT).
 160 íÙ  ÚÁÉÎÔÅÒÅÓÏ×ÁÎÙ × ÐÏÓÔÒÏÅÎÉÉ Ó×ÏÂÏÄÎÙÈ ÁÌÇÅÂÒ ×
 161 ÐÏÄËÌÁÓÓÁÈ $\KATc|E$, $\RKAT|E$, $\KAT|E$,
 162 ÏÇÒÁÎÉÞÅÎÎÙÈ ÄÏÐÏÌÎÉÔÅÌØÎÏ ÎÁËÌÁÄÙ×ÁÅÍÙÍÉ ÔÒÅÂÏ×ÁÎÉÑÍÉ $E$\T
 163 Ë ÔÁËÉÍ ÁÌÇÅÂÒÁÍ ÏÂÒÁÝÅÎÏ ÎÁÛÅ ×ÎÉÍÁÎÉÅ × ÜÔÏÊ çÌÁ×Å ËÁË Ë ÏÓÎÏ×Å
 164 ÎÁÛÉÈ ÉÓÓÌÅÄÏ×ÁÎÉÊ ÐÒÏÂÌÅÍÙ ÜË×-ÔÉ ÐÒÏÇÒÁÍÍ.
 165
 166 %\todo{[ÇÄÅ-ÎÂ ÎÁÐÉÓÁÔØ, ÞÅÍ ×ÏÏÂÝÅ ÃÅÎÎÁ Ó×ÏÂÏÄÎÁÑ ÁÌÇÅÂÒÁ]}
 167
 168 ðÏÐÒÏÂÕÅÍ Õ×ÉÄÅÔØ Ó×ÑÚØ ÍÅÖÄÕ
 169 Ó×ÏÂÏÄÎÏÊ ÁÌÇÅÂÒÏÊ~$\Reg_{\Sigma,T}$ ×~\KATc (guarded strings
 170 (\tD{ÎÁÓÙÝÅÎÎÙÅ ÓÔÒÏËÉ}{def:gs}))
 171 É Ó×ÏÂÏÄÎÏÊ ÁÌÇÅÂÒÏÊ~$\Reg_\Sigma$  ×~\KA\T (ÓÔÒÏËÉ) × ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÅÍ
 172 ÓÌÕÞÁÅ ÂÅÚ ÔÅÓÔÏ×
 173 É ÏÂÏÂÝÉÔØ ÜÔÕ Ó×ÑÚØ ÎÁ ÎÁÛ ÂÏÌÅÅ ÓÌÏÖÎÙÊ ÓÌÕÞÁÊ.
 174
 175 ÷ çÌÁ×Å~\ref{cha:hypo-plain} ÂÙÌ ××ÅÄ£Î ÏÂÝÉÊ ÓÐÏÓÏÂ ÐÏÓÔÒÏÅÎÉÑ
 176 Ó×ÏÂÏÄÎÏÊ ÁÌÇÅÂÒÙ × ÐÏÄËÌÁÓÓÅ $\KAc|E$, ÏÇÒÁÎÉÞÅÎÎÏÍ
 177 \tD{ÍÏÎÏÉÄÎÙÍÉ}{def:monoid-assumptions} ÕÓÌÏ×ÉÑÍÉ\T ÐÒÉÍÅÎÅÎÉÅ
 178 ÆÕÎËÔÏÒÁ~$\REG$ ÉÚ
 179 ËÁÔÅÇÏÒÉÉ ÍÏÎÏÉÄÏ× × ËÁÔÅÇÏÒÉÀ $\KAc$ Ë Ó×ÏÂÏÄÎÏÍÕ ÍÏÎÏÉÄÕ × ËÌÁÓÓÅ
 180 ÍÏÎÏÉÄÏ×, ÏÇÒÁÎÉÞÅÎÎÏÍ ÚÁÄÁÎÎÙÍÉ ÕÓÌÏ×ÉÑÍÉ.
 181 ÷ ÞÁÓÔÎÏÓÔÉ, ËÌÁÓÓÉÞÅÓËÁÑ $\Reg_{\Sigma} = \REG \Sigma^*$.
 182
 183 \todo{[Õ ÎÁÓ -- GUARD ÉÚ ÍÏÎÏÉÄÏ×, REG = GUARD * forgetKAT, ÏÂÏÇÁÔÉÍ
 184   ÄÅÊÓÔ×ÉÅ REG.]}
 185
 186 %% REGT?
 187
 188 %% ×ÏÚÍÏÖÎÏ, ÔÏ, ÞÔÏ ÍÙ ÓÄÅÌÁÅÍ -- ÐÒÏÓÔÏÅ ÓÌÅÄÓÔ×ÉÅ ÕÓÔÁÎÏ×ÌÅÎÎÙÈ ×
 189 %% õÎÉ×ÅÒÓÁÌØÎÏÊ ÁÌÇÅÂÒÅ É ôÅÏÒÉÉ ËÁÔÅÇÏÒÉÊ ÏÂÝÉÈ Ó×ÏÊÓÔ×. ÓÍ. × ÞÁÓÔÎÏÓÔÉ ×
 190 %% ÐÒÉÍÅÎÅÎÉÉ Ë KAT \cite{KAT-free-construction} (ÇÄÅ ÕÓÔÁÎÁ×ÌÉ×ÁÅÔÓÑ
 191 %% ÉÚÏÍÏÒÆÉÚÍ ÍÅÖÄÕ ÓÔÒÕËÔÕÒÁÍÉ, ÐÏÌÕÞÅÎÎÙÍÉ × ÒÅÚÕÌØÔÁÔÅ ÏÂÝÉÈ
 192 %% ËÏÎÓÔÒÕËÃÉÊ õá É ôë, É $\Reg_{\Sigma,T}$ (guarded strings)
 193 %% × \KAT, ÐÏÓÔÒÏÅÎÎÙÍÉ × \cite{KAT??}.
 194
 195 %% îÏ
 196
 197 %% ÏÂÝÉÍÉ ÍÅÔÏÄÁÍÉ ÁÌÇÅÂÒÙ -- ÔÏÌØËÏ ÓÕÝÅÓÔ×Ï×ÁÎÉÅ ÉÌÉ × ×ÉÄÅ, ÉÍÅÀÝÅÍ
 198 %% ÍÁÌÏ ÏÔÎ-Ñ Ë ÎÁÛÅÍÕ ÐÏÎÉÍÁÎÉÀ ÜÔÉÈ ÓÔÒÕËÔÕÒ É ÉÈ ÎÁÚÎÁÞÅÎÉÀ -- ÁÎÁÌÉÚÕ
 199 %% ÐÒÏÇÒÁÍÍ
 200
 201 %% ËÏÎËÒÅÔÎÙÊ ×ÉÄ -- ÐÏÚ×ÏÌÑÅÔ ÌÕÞÛÅ ÉÈ ÐÒÅÄÓÔÁ×ÌÑÔØ É ÒÁÓÓÕÖÄÁÔØ
 202
 203 %% ËÏÎËÒÅÔÎÙÊ ×ÉÄ -- ÄÁ£Ô ×ÏÚÍÏÖÎÏÓÔØ ÐÏÌÕÞÁÔØ ÄÒÕÇÉÅ ÒÅÚÕ-ÔÙ, ÎÁÐÒÉÍÅÒ,
 204 %% ...
 205
 206 %% ÎÅÉÚ×ÅÓÔÎÙÊ ÒÅÚÕÌØÔÁÔ Ï RKAT|E = KATc|E ÄÌÑ ÉÓÓÌÅÄÏ×ÁÎÎÙÈ ËÌÁÓÓÏ× KAT
 207 %% -- ÐÏÈÏÖÅ ÎÁ ÉÚ×ÅÓÔÎÙÊ ÒÅÚÕÌØÔÁÔ × ÐÒÏÓÔÏÍ ÓÌÕÞÁÅ, ÐÏËÁÚÙ×ÁÅÔ, ÞÔÏ ÍÙ
 208 %% ÂÌÉÚËÉ Ë ÎÅÍÕ (× ÏÔÌÉÞÉÅ ÏÔ ÓÌÕÞÁÅ× ..., ÇÄÅ ÜÔÏ ÎÅ ÔÁË)
 209 %% (×ÁÖÎÏ: RKAT ÞÁÝÅ ÉÓÐ-ÓÑ ÄÌÑ ÏÐÉÓÁÎÉÑ ÓÅÍÁÎÔÉË ÐÒÏÇÒÁÍÍ, KATc
 210 %% ÄÏÐÕÓËÁÅÔ ÂÏÌØÛÅ Ó×ÏÂÏÄÙ × ÔÏÍ, ÏÔ ÞÅÇÏ ÍÙ ÁÂÓÔÒÁÇÉÒÕÅÍÓÑ. ÷ KATc
 211 %% ÒÁÓÓÕÖÄÁÔØ ÐÒÏÝÅ (ÓÍ ....). üÔÏÔ ÆÁËÔ ÐÏËÁÚÙ×ÁÅÔ, ÞÔÏ ÐÒÅÉÍÕÝÅÓÔ×Ï Õ
 212 %% ÎÁÓ ÓÏ×ÍÅÝÁÀÔÓÑ. ï ÓÒÁ×ÎÅÎÉÉ RKAT É KATc ÓÍ ....)
 213
 214 %% ÏÂÝÉÊ ÓÐÏÓÏÂ ÐÏÌÕÞÅÎÉÑ ÉÚ ÍÏÎÏÉÄÏ× -- ËÁË REG
 215
 216 %% ÍÏÖÎÏ ÐÙÔÁÔØÓÑ ÒÁÓÐÒÏÓÔÒÁÎÉÔØ É ÎÁ ÄÒÕÇÉÅ ÓÌÕÞÁÉ ÜÔÏ ÐÏÓÔÒÏÅÎÉÅ -- ÓÍ
 217 %% ÓÌÅÄ ÒÁÚÄÅÌ ....
 218
 219 %% ËÏÎËÒ ×ÉÄ -- ÍÏÖÎÏ ÓÔÒÏÉÔØ ÁÌÇÏÒÉÔÍÙ ÐÒÏ×ÅÒËÉ ÜË×-ÔÉ (×ÁÖÎÏ!)
 220 %% (ÓÍ. ....)
 221
 222 %% ÔÏ, ËÁË ÍÙ ÜÔÏ ÄÅÌÁÅÍ --- ÓÏÏÔÎ-Å: ÓÏ×ÍÅÓÔÎÁÑ ÔÒÁÓÓÁ (ÐÏÌÕÞÅÎÎÁÑ
 223 %% ÓÉÎÔÁËÓÉÞÅÓËÉ, ÓÏ×ÍÅÓÔÎÏÓÔØ ×Ù×ÏÄÉÔÓÑ; ÍÙ ÒÁÎØÛÅ × ÄÏË-×ÁÈ É
 224 %% ÁÌÇÏÒÉÔÍÁÈ ÒÁÓÓÕÖÄÁÌÉ Ï ÎÉÈ, ÐÅÒ×ÙÍ ÛÁÇÏÍ ÐÅÒÅÈÏÄÉÌÉ ÏÔ ``ÐÅÒÅÂÏÒÁ''
 225 %% ÍÏÄÅÌÅÊ Ë ÐÅÒÅÂÏÒÕ ÔÒÁÓÓ --- ÁÎÁÌÏÇ: ÏÔ ÓÅÍÁÎÔÉÞ. ×ÅÒÎÏÓÔÉ Ë
 226 %% ×Ù×ÏÄÉÍÏÓÔÉ; ÔÁË ÂÙÌÏ ÕÄÏÂÎÅÅ) --
 227 %% ÓÅÍÁÎÔÉËÁ -- ÜÌÅÍÅÎÔ Ó×. ÍÏÄÅÌÉ --
 228 %% ÍÏÖÎÏ ÒÅÁÌÉÚÏ×ÁÔØ × ÂÁÚÉÓÎÙÈ. (×ÏÔ ËÁË ÉÓÐ-ÓÑ ÎÁÛÅ ÐÒÅÖÎÅÅ
 229 %% ÕÍÅÎÉÅ. ôÅÐÅÒØ ÜÔÁ ÔÏÞËÁ ÚÒÅÎÉÑ ÏÔÒÁÖÅÎÁ ÔÕÔ.)
 230
 231 %% ÏÂ ÕÓÔÒÏÊÓÔ×Å ÍÏÄÅÌÅÊ, ÉÈ ÓÏÏÔÎÏÛÅÎÉÉ -- ÎÁÂÏÒ ÐÒÏÓÔÙÈ (ÂÁÚÉÓÎÙÈ),
 232 %% ÅÓÔÅÓÔ×ÅÎÎÙÈ ÄÌÑ ÁÎÁÌÉÚÁ ÐÒÏÇÒÁÍÍ ÍÏÄÅÌÅÊ ÓÏÏÔ×. Ó×ÏÂÏÄÎÏÊ (É ÄÌÑ
 233 %% Á×ÔÏÍÁÔÏ× ÔÁË ÂÙÌÏ ....). üÔÏ ÄÅÌÁÅÔ ÉÓÓÌÅÄÏ×ÁÎÉÑ, ÐÒÏ×ÅÄ£ÎÎÙÅ ÔÏÌØËÏ
 234 %% × ÎÉÈ (...) ÚÎÁÞÉÍÙÍÉ É ÐÒÉ ÎÁÉÂÏÌÅÅ ÏÂÝÅÊ (ÄÌÑ ÎÁÓ) ÐÏÓÔÁÎÏ×ËÅ
 235 %% ÚÁÄÁÞÉ. æÏÒÍÁÌØÎÏ ÐÏÄÔ×ÅÒÖÄÁÅÔ ÎÅÓÌÕÞÁÊÎÏÓÔØ, ÞÔÏ ÏÎÉ ÂÙÌÉ ×ÙÂÒÁÎÙ.
 236
 237 %% É ÜÔÏ ÔÏÖÅ -- × ÐÏÍÏÝØ ÒÁÓÓÕÖÄÅÎÉÑÍ Ï ÍÏÄÅÌÑÈ -- ÍÏÖÎÏ ÒÁÓÓÕÖÄÁÔØ
 238 %% ÔÏÌØËÏ Ï ÔÁËÉÈ.
 239
 240 %% ðÏÞÅÍÕ ÎÅ ÍÏÇÌÉ ÎÁ ÎÉÈ (ÐÒÏÓÔÙÈ) ÕÓÐÏËÏÉÔØÓÑ? åÓÔØ ÍÅÔÏÄÙ (Eilenberg ÄÌÑ dmta,
 241 %% ÓÍ. ...), ÒÅÚÕÌØÔÁÔÙ, ÐÏÌÕÞÅÎÎÙÅ ÐÒÉ ÉÓÐÏÌØÚÏ×ÁÎÉÉ ÍÏÄÅÌÅÊ ÔÁËÏÇÏ ÒÏÄÁ
 242 %% (Ó×.), ÐÏÜÔÏÍÕ ÅÓÌÉ ÍÙ ÉÈ ÐÙÔÁÅÍÓÑ ÒÁÓÐÒÏÓÔÒÁÎÉÔØ, ÎÁÄÏ ÐÏÎÑÔØ, ÞÔÏ
 243 %% ÓÏÏÔ×. ÜÔÏÍÕ × ÎÁÛÅÍ ÓÌÕÞÁÅ. ðÏËÁ ÐÏÌÎÁÑ ÑÓÎÏÓÔØ ÎÅ ÄÏÓÔÉÇÎÕÔÁ. ó
 244 %% ÏÄÎÏÊ ÓÔÏÒÏÎÙ, $xy = 0$, ÞÅÇÏ ÔÁÍ ÎÅÔ, ÎÏ Ó ÄÒÕÇÏÊ ÓÔÏÒÏÎÙ, ÅÓÔØ ÓÔÁÎÄ
 245 %% ÓÏÏÔ×-Å (ÐÒÉÍÅÒ ÄÌÑ 2 tape), ËÏÔÏÒÏÅ ÄÁ£Ô ÎÁÍ£Ë ÎÁ ÔÏ, ËÁË ÍÏÖÎÏ
 246 %% ×Ó£-ÔÁËÉ ÕÓÔÁÎÏ×ÉÔØ ÒÁÚÕÍÎÏÅ ÓÏÏÔ×-Å ÍÅÖÄÕ ÔÅÍ ÓÌÕÞÁÅÍ (HK) É ÎÁÛÉÍ.
 247
 248
 249 \paragraph{$\REGT$.}
 250 ðÕÓÔØ $\Sigma$, $T$\T ËÏÎÅÞÎÙÅ ÁÌÆÁ×ÉÔÙ (<<ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ×>> É
 251 <<ÂÁÚÏ×ÙÈ ÔÅÓÔÏ×>>).
 252 ðÕÓÔØ $\mo M = (Q_{\mo M}; \cdot, 1_{\mo M})$\T
 253 ÎÅËÏÔÏÒÙÊ ÍÏÎÏÉÄ Ó ÐÏÒÏÖÄÁÀÝÉÍÉ ÜÌÅÍÅÎÔÁÍÉ $\Sigma$
 254 (ÎÅÏÂÑÚÁÔÅÌØÎÏ \tD{Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ, ÐÏÒÏÖÄ£ÎÎÙÊ
 255   $\Sigma$}{def:free-monoid}).
 256
 257 ðÕÓÔØ $\mo M$\T ÍÏÎÏÉÄ Ó ÌÅ×ÙÍ ÓÏËÒÁÝÅÎÉÅÍ.
 258
 259 \begin{definition}\label{def:lframe}
 260 \tING{ûËÁÌÏÊ ëÒÉÐËÅ Ó ÐÒÅÄÅÌÏÍ, ÏÓÎÏ×ÁÎÎÏÊ ÎÁ ÍÏÎÏÉÄÅ $\mo M$}
 261 ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ ÐÁÒÕ~$(\xi, u)$, ÔÁËÕÀ, ÞÔÏ $u \in Q_{\mo
 262   M}$, $\xi\colon Q_{\mo M} \times T \to \{ \False, \True \}$.
 263
 264 $\LFrames(\Sigma, T, \mo M)$\T ÍÎÏÖÅÓÔ×Ï ×ÓÅÈ \tDJust{ÛËÁÌ ëÒÉÐËÅ Ó
 265   ÐÒÅÄÅÌÏÍ, ÏÓÎÏ×ÁÎÎÙÈ ÎÁ}~$\mo M$.
 266 \end{definition}
 267
 268 ðÏÓÔÒÏÉÍ ÎÁ ÏÓÎÏ×Å~$\LFrames(\Sigma, T, \mo M)$ ÓÔÒÕËÔÕÒÕ \KAT.
 269
 270 óÎÁÞÁÌÁ ÏÐÒÅÄÅÌÉÍ ÞÁÓÔÉÞÎÏ ÏÐÒÅÄÅÌ£ÎÎÕÀ
 271 ÏÐÅÒÁÃÉÀ \tING{ÎÁÌÏÖÅÎÉÑ} Ä×ÕÈ ÛËÁÌ ëÒÉÐËÅ Ó
 272 ÐÒÅÄÅÌÏÍ:
 273 \begin{equation}
 274   \label{eq:frCo}
 275   (\xi_1, u_1) \frCo (\xi_2, u_2)
 276   \eqdef
 277   \begin{cases}
 278     (\xi_1, u_1 u_2)
 279     & \text{ ÅÓÌÉ }
 280     \xi_1(u_1 w) = \xi_2(w)
 281       \text{ ÄÌÑ ×ÓÅÈ $w \in \mo M$,}
 282     \\
 283     \text{ÎÅÏÐÒÅÄÅÌÅÎÏ}
 284     & \text{ÉÎÁÞÅ.}
 285   \end{cases}
 286 \end{equation}
 287
 288 ïÐÉÛÅÍ ÁÌÇÅÂÒÕ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ, ÜÌÅÍÅÎÔÁÍÉ ËÏÔÏÒÏÊ ÂÕÄÕÔ
 289 ÍÎÏÖÅÓÔ×Á ÛËÁÌ ëÒÉÐËÅ Ó ÐÒÅÄÅÌÏÍ.
 290
 291 ûËÁÌÁ ëÒÉÐËÅ Ó ÐÒÅÄÅÌÏÍ\dÅÄÉÎÉÃÅÊ\T ÜÔÏ ÛËÁÌÁ ëÒÉÐËÅ Ó ÐÒÅÄÅÌÏÍ ×ÉÄÁ
 292 $(\xi, 1_{\mo M})$. (ïÎÉ ÎÁÈÏÄÑÔÓÑ ×Ï ×ÚÁÉÍÎÏ ÏÄÎÏÚÎÁÞÎÏÍ ÓÏÏÔ×ÅÔÓÔ×ÉÉ
 293 Ó ÏÃÅÎËÁÍÉ ÎÁ $Q_{\mo M}$.) éÈ ÍÎÏÖÅÓÔ×Ï ÏÂÏÚÎÁÞÉÍ $\ILFrames(\Sigma,
 294 T, \mo M)$.
 295
 296 ðÕÓÔØ $K = 2^{\LFrames(\Sigma, T, \mo M)}$, $B = 2^{\ILFrames(\Sigma,
 297   T, \mo M)}$.
 298
 299 \begin{definition}
 300   äÌÑ
 301   $D, E \in K,
 302   \bt{C} \in B $:
 303   \begin{align}
 304     \n{\bt C} &\eqdef \ILFrames(\Sigma, T, \mo M) \setminus \bt C\\
 305     \label{eq:fr-set-concat}
 306     D \frCo E &\eqdef \{ \sigma \frCo \tau \mid
 307     \sigma \in D,\, \tau \in E,\, \sigma \frCo \tau \text{ ÓÕÝÅÓÔ×ÕÅÔ}\};\\
 308     \label{eq:fr-set-star}
 309     D^*  &\eqdef \bigcup_{n \in \bbN \cup \{ 0 \}} D^n,
 310   \end{align}
 311   ÇÄÅ
 312   \begin{align*}
 313     D^0 &\eqdef \ILFrames(\Sigma, T, \mo M),
 314     &
 315     D^{n+1} &\eqdef D \frCo D^n.
 316   \end{align*}
 317 \end{definition}
 318
 319 \begin{proposition}\label{prop:all-fr-KAT}
 320   óÔÒÕËÔÕÒÁ~$(K, B;
 321   \cup, \frCo, {}^*, \nP, \emptyset, \ILFrames(\Sigma, T, \mo M) )$\T
 322   *\dÎÅÐÒÅÒÙ×ÎÁÑ \KAT.
 323 \end{proposition}
 324 \begin{proof}
 325   ðÏ×ÔÏÒÑÅÔ ÓÔÁÎÄÁÒÔÎÙÅ ÄÏËÁÚÁÔÅÌØÓÔ×Á ÁÎÁÌÏÇÉÞÎÙÈ õÔ×ÅÒÖÄÅÎÉÊ:
 326   õÔ×.~\ref{prop:all-gs-KAT}, \ref{prop:all-Mo-KA},
 327   \ref{prop:all-str-KA}.
 328
 329   %\todo{[ÏÐÉÓÁÔØ ÔÏÎËÏÓÔÉ]}
 330 \end{proof}
 331
 332 \subparagraph{ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ.}
 333
 334 ïÐÒÅÄÅÌÉÍ $F_{\Sigma,T,\mo M}\colon \Sigma \cup T \to K$:
 335 \begin{align}
 336   F_{\Sigma,T,\mo M}(a)
 337   &\eqdef \{ (\xi, a) \mid
 338   \xi\text{\T ÏÃÅÎËÁ $T$ ÎÁ $Q_{\mo M}$}
 339   \}
 340   \text{ ÄÌÑ } a \in \Sigma\\
 341   F_{\Sigma,T,\mo M}(p)
 342   &\eqdef \{ (\xi, 1_{\mo M}) \mid
 343   \xi(1_{\mo M}, p) = 1
 344   \}
 345   \text{ ÄÌÑ } p \in T.
 346 \end{align}
 347 îÁ ×Ó£ $\RExp_{\Sigma,T}$ $F_{\Sigma,T,\mo M}$ ÐÒÏÄÏÌÖÁÅÔÓÑ ÇÏÍÏÍÏÒÆÎÏ.
 348
 349 ðÏ ÁÎÁÌÏÇÉÉ Ó ÂÏÌÅÅ ÐÒÏÓÔÙÍÉ ÓÌÕÞÁÑÍÉ,
 350 \begin{definition}
 351 íÎÏÖÅÓÔ×Ï ÛËÁÌ Ó ÐÒÅÄÅÌÏÍ $D \subseteq \LFrames(\Sigma, T, \mo M)$
 352 ÂÕÄÅÍ ÎÁÚÙ×ÁÔØ \tING{ÒÅÇÕÌÑÒÎÙÍ}, ÅÓÌÉ $D = F_{\Sigma,T,\mo M}(s)$ ÄÌÑ
 353 ÎÅËÏÔÏÒÏÇÏ ÒÅÇÕÌÑÒÎÏÇÏ ×ÙÒÁÖÅÎÉÑ $s \in \RExp_{\Sigma,T}$.
 354
 355 ïÂÒÁÚ $\RExp_{\Sigma,T}$ ÐÒÉ ÉÎÔÅÒÐÒÅÔÁÃÉÉ $F_{\Sigma,T,\mo M}$ ÂÕÄÅÍ
 356 ÏÂÏÚÎÁÞÁÔØ $\Cons_{\Sigma,T,\mo M}$ ÉÌÉ
 357 $\Cons_{\Sigma,T,E_{\mword{monoid}}}$, ÇÄÅ $E_{\mword{monoid}}$\T
 358 ÍÎÏÖÅÓÔ×Ï ÏÐÒÅÄÅÌÑÀÝÉÈ ÓÏÏÔÎÏÛÅÎÉÊ ÄÌÑ ÍÏÎÏÉÄÁ. ðÏÓÌÅÄÎÅÅ
 359 ÏÂÏÚÎÁÞÅÎÉÅ ÓÏÏÔ×ÅÔÓÔ×ÕÅÔ Ó×ÏÂÏÄÎÏÍÕ ÍÏÎÏÉÄÕ $\mo M$, ÐÏÒÏÖÄ£ÎÎÏÍÕ
 360 $\Sigma$ Ó ÏÐÒÅÄÅÌÑÀÝÉÍÉ ÓÏÏÔÎÏÛÅÎÉÑÍÉ $E_{\mword{monoid}}$.
 361 \end{definition}
 362
 363 \begin{proposition}
 364   $\Cons_{\Sigma,T,E_{\mword{monoid}}}$ ÉÚÏÍÏÒÆÎÁ ÎÅËÏÔÏÒÏÊ
 365   ÒÅÌÑÃÉÏÎÎÏÊ ÍÏÄÅÌÉ ÉÚ $(\RELT | \Emonoid)$.
 366 \end{proposition}
 367 \begin{proof}
 368 %\todo{[??]}
 369 ôÁË ÖÅ, ËÁË É Ä-×Ï ÁÎÁÌÏÇÉÞÎÏÇÏ ÕÔ×-Ñ Ï $\Reg_{\Sigma,T}$.
 370 \end{proof}
 371
 372 %\input lframes-rem
 373
 374 \paragraph{õÎÉ×ÅÒÓÁÌØÎÁÑ ÍÏÄÅÌØ ÐÏ ÏÔÎÏÛÅÎÉÀ Ë $\SIMPLET$.}
 375 \begin{proposition}
 376   $$
 377   \Cons_{\Sigma,T,E_{\mword{monoid}}} \models s = t
 378   \iff
 379   \SIMPLET(\Emonoid) \models s = t.
 380   $$
 381 \end{proposition}
 382
 383 üÔÏ ÇÏÒÁÚÄÏ ÂÏÌÅÅ ÓÌÁÂÏÅ õÔ×ÅÒÖÄÅÎÉÅ, ÞÅÍ õÔ×ÅÒÖÄÅÎÉÅ Ï ÔÏÍ, ÞÔÏ ÜÔÏ
 384 Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ × $\KATc | \Emonoid$. ðÒÅÄÌÏÖÉÍ ×ÏÚÍÏÖÎÙÊ ÐÕÔØ
 385 ÄÏËÁÚÁÔÅÌØÓÔ×Á ÔÁËÏÇÏ ÂÏÌÅÅ ÓÉÌØÎÏÇÏ õÔ×ÅÒÖÄÅÎÉÑ (×ÏÚÍÏÖÎÏ, ÄÌÑ
 386 ÎÅËÏÔÏÒÙÈ ×ÉÄÏ× ÕÓÌÏ×ÉÊ ÏÎ ÂÕÄÅÔ ÒÁÂÏÔÁÔØ.)
 387
 388 $$
 389 \gs(F(s)) \eqdef \{ \sigma \in \GS(\Sigma,T) \mid F(\sigma) \subseteq
 390 F(s) \}
 391 $$
 392 \begin{remark}
 393   åÓÌÉ $\Emonoid = \emptyset$, ÔÏ $\gs(F(s)) = G(s)$.
 394 \end{remark}
 395 ðÒÅÄÌÁÇÁÅÔÓÑ ÎÁÊÔÉ ÎÅÏÂÈÏÄÉÍÙÅ É ÄÏÓÔÁÔÏÞÎÙÅ ÕÓÌÏ×ÉÑ ÄÌÑ ÔÏÇÏ, ÞÔÏÂÙ
 396 ÂÙÌ ×ÅÒÅÎ ÁÎÁÌÏÇ ìÅÍÍÙ~\ref{lem:I-sup-G}: ÄÌÑ ÌÀÂÏÊ $I\map \Sigma \cup
 397 T \to \ka T$, ÇÄÅ $\ka T \in \KATc$,
 398 $$
 399 I(s) = \sup_{\sigma \in \gs(F(s))} I(\sigma).
 400 $$
 401
 402
 403 %% $op(\sigma)$
 404
 405 %% $\sigma \le op(\sigma)$
 406
 407 %% ïÂÏÂÝÅÎÉÅ $p \le 1$.
 408
 409 %% (ðÏÓÍÏÔÒÉÍ ÎÁ ÜÔÏ Ó ÔÏÞËÉ ÚÒÅÎÉÑ ÎÁÛÅÊ ÓÅÍÁÎÔÉËÉ.
 410 %% ðÒÏ ÎÅ£ ÍÙ ÎÁÄÅÅÍÓÑ, ÞÔÏ ÏÎÁ Ó×., É ÚÎÁÞÉÔ, ×Ù×ÏÄÉÍÙÅ ÓÏÏÔÎ-Ñ ÉÍÅÀÔ
 411 %% <<ÏÂßÑÓÎÅÎÉÅ>> Ó ÔÏÞËÉ ÚÒÅÎÉÑ ÓÅÍÁÎÔÉËÉ. íÏÖÎÏ ÏÇÒÁÎÉÞÉÔØÓÑ ÔÏÌØËÏ
 412 %% ÎÁÛÅÊ Ó×. (ÐÏËÁ ÅÝ£ ÎÅ ÕÓÔÁÎÏ×ÌÅÎÏ) ÍÏÄÅÌØÀ. üÔÏ -- ÄÅÍÏÎÓÔÒÁÃÉÑ ÔÏÇÏ,
 413 %% ÞÅÍ ÏÎÁ ÍÏÖÅÔ ÂÙÔØ ÐÏÌÅÚÎÁ. ï ÓÏÏÔÎÏÛÅÎÉÉ ×Ù×ÏÄÁ É ÓÅÍÁÎÔÉÞÅÓËÏÊ
 414 %% ×ÅÒÎÏÓÔÉ -- ÓÍ. ....
 415
 416 %% ÷ÅÒÎ£ÍÓÑ Ë \eqref{??}:
 417 %% ÌÅ×ÁÑ ÞÁÓÔØ ÂÏÌÅÅ ÓÐÅÃÉÆÉÞÎÁ, Ó ÔÏÞËÉ ÚÒÅÎÉÑ
 418 %% ÏÇÒÁÎÉÞÅÎÉÑ ÏÃÅÎÏË, ÐÏÌÕÞÁÀÝÉÈÓÑ × ÉÎÔÅÒÐÒÅÔÁÃÉÉ)
 419
 420 \subsection{éÔÏÇÉ}
 421
 422
 423 \begin{itemize}
 424 \item
 425 \KAndetAnsws
 426
 427 \item
 428
 429 \todo{$\KAT \supset \KATc \supset \RKAT \ni \Reg_{\Sigma,T}$
 430 simple?}
 431
 432 $\EOf\KAT = \EOf \KATc = \EOf \RKAT
 433 \Over{$\Sigma,T$}{=} \EOf \Reg_{\Sigma,T} = \EOf \SIMPLET_{\Sigma,T}$
 434 \todo{[simple ??]},
 435 $\Reg_{\Sigma,T}$\T Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ, ÐÏÌÕÞÁÅÔÓÑ ËÁË $\REGT \Sigma^*$.
 436
 437 òÁÚÒÅÛÉÍÁ, \PSPACE{}\dÐÏÌÎÁ \todo{[???]}.
 438
 439
 440 \item
 441 \todo{[??]: $\HOf \KA \subset \HOf \KAc \subset \HOf \RKA$}
 442
 443 \todo{[îÅÒÁÚÒÅÛÉÍÙ.]}
 444
 445
 446 \item thClasses
 447
 448 \item $\Emonoid \in \MoEqua$
 449
 450 \todo{[??]: $\EOf (\KAT|\Emonoid) \Qm{\subseteq}
 451   \EOf (\KATc|\Emonoid) \Qm{\subseteq}
 452   \EOf (\RKAT|\Emonoid)
 453   \Over{$\Sigma,T$}{\Qm{\subseteq}}
 454   \EOf \Cons_{\Sigma, T, \Emonoid}
 455   = \EOf (\SIMPLET|\Emonoid)_{\Sigma,T}$},
 456 $\Cons_{\Sigma, T, \Emonoid}$ ÐÏÌÕÞÁÅÔÓÑ ËÁË $\REGT \mo
 457   M_0({\Emonoid})$.
 458
 459   ëÏÇÄÁ ÒÁÚÒÅÛÉÍÁ, ÓÌÏÖÎÏÓÔØ?
 460   \begin{itemize}
 461   \item
 462     commm?
 463   \end{itemize}
 464
 465 \end{itemize}
 466
 467
 468 %%% Local Variables:
 469 %%% mode: latex
 470 %%% TeX-master: "main"
 471 %%% End: