hypo-plain-ndet.tex

   1 \subsection{æÏÒÍÕÌÙ, ÔÅÏÒÉÉ, ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ: ÓÌÕÞÁÊ Ó
   2 ÓÅÍÁÎÔÉÞÅÓËÉÍÉ ÐÏÓÔÕÌÁÔÁÍÉ}
   3 \label{sec:hypo-theories}
   4
   5
   6 \paragraph{æÏÒÍÕÌÙ É ÔÅÏÒÉÉ ÏÓÏÂÏÇÏ ×ÉÄÁ.}
   7
   8 \tD{Horn\dÔÅÏÒÉÑ}{def:Horn-theory} ËÌÁÓÓÁ ÁÌÇÅÂÒ (ÉÌÉ ÁÌÇÅÂÒ Ó
   9 ÉÎÔÅÒÐÒÅÔÁÃÉÑÍÉ  × ÎÉÈ ÂÁÚÏ×ÙÈ ÓÉÍ×ÏÌÏ×)
  10 ÕÖÅ ÂÙÌÁ ÏÐÒÅÄÅÌÅÎÁ. íÙ ÂÕÄÅÍ ÕÄÅÌÑÔØ ×ÎÉÍÁÎÉÅ É
  11 ÓÐÅÃÉÁÌØÎÏÇÏ ×ÉÄÁ ÐÏÄÔÅÏÒÉÑÍ îÏrn\dÔÅÏÒÉÊ.
  12 \begin{definition}\label{def:Horn--thclass}
  13   ðÕÓÔØ $\Equa$ ÏÂÏÚÎÁÞÁÅÔ ËÌÁÓÓ ÔÅÏÒÉÊ, × ËÏÔÏÒÙÈ ÆÏÒÍÕÌÙ\T ÜÔÏ
  14   ÒÁ×ÅÎÓÔ×Á. ðÕÓÔØ $\thclass c \subseteq \Equa$, \te ÜÔÏ ÎÅËÏÔÏÒÙÊ
  15   ÐÏÄËÌÁÓÓ ÔÅÏÒÉÊ ÏÓÏÂÏÇÏ ×ÉÄÁ, ÓÏÓÔÏÑÝÉÈ ÉÚ ÆÏÒÍÕÌ\DÒÁ×ÅÎÓÔ×.
  16   ôÏÇÄÁ ÞÅÒÅÚ $\Horn(\thclass c)$ ÍÙ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ ÍÎÏÖÅÓÔ×Ï ×ÓÅÈ ÔÅÏÒÉÊ, ×
  17   ËÏÔÏÒÙÈ ÆÏÒÍÕÌÙ\T Horn\DÆÏÒÍÕÌÙ ÏÓÏÂÏÇÏ ×ÉÄÁ, Á ÉÍÅÎÎÏ,
  18   Horn\DÆÏÒÍÕÌÙ Ó ÐÏÓÙÌËÁÍÉ ÏÓÏÂÏÇÏ ×ÉÄÁ:
  19   $$
  20   E \implic s = t,
  21   $$
  22   ÇÄÅ $E \in \thclass c$, Á $s$ É $t$, ËÁË É × ÏÂÝÅÍ ÓÌÕÞÁÅ,\T ÔÅÒÍÙ.
  23 \end{definition}
  24
  25 \begin{definition}
  26 ëÌÁÓÓ ÔÅÏÒÉÊ, × ËÏÔÏÒÙÈ ÒÁÚÒÅÛÅÎÙ ÆÏÒÍÕÌÙ É ×ÉÄÁ~$\thclass c_1$, É
  27 ×ÉÄÁ~$\thclass c_2$, ÏÂÏÚÎÁÞÉÍ $\thclass c_1 \oplus \thclass c_2$:
  28 $$
  29 \thclass c_1 \oplus \thclass c_2
  30 \eqdef
  31 \{ \Phi_1 \cup \Phi_2 \mid \Phi_1 \in \thclass c_1,
  32 \Phi_2 \in \thclass c_2 \}.
  33 $$
  34 \end{definition}
  35
  36 ðÏ~ïÐÒÅÄÅÌÅÎÉÑÍ~\ref{def:EquaOf} É \ref{def:HornOf}, $\EOf\class C$\T ÜÔÏ
  37 ÔÅÏÒÉÑ ÒÁ×ÅÎÓÔ× ËÌÁÓÓÁ~$\class C$, $\HOf\class C$\T ÔÅÏÒÉÑ
  38 (ÕÎÉ×ÅÒÓÁÌØÎÙÈ) Horn-ÆÏÒÍÕÌ ËÌÁÓÓÁ~$\class C$. ôÁËÖÅ ÏÂÏÚÎÁÞÉÍ
  39 $\HOf_{\thclass c}\class C$ ÔÅÏÒÉÀ
  40 ÕÎÉ×ÅÒÓÁÌØÎÙÈ Horn-ÆÏÒÍÕÌ ËÌÁÓÓÁ~$\class C$, × ËÏÔÏÒÙÈ ÐÏÓÙÌËÉ ÉÍÅÀÔ
  41 ÓÐÅÃÉÁÌØÎÙÊ ×ÉÄ\T $\thclass c$ (ÔÁËÉÍ ÏÂÒÁÚÏÍ, $\HOf_{\thclass c}\class C \in
  42 \Horn(\thclass c)$).
  43
  44 ó ÉÓÐÏÌØÚÕÅÍÙÍÉ ÎÁÍÉ ÏÂÏÚÎÁÞÅÎÉÑÍÉ ËÌÁÓÓÏ× ÔÅÏÒÉÊ ÍÏÖÎÏ ÏÚÎÁËÏÍÉÔØÓÑ
  45 ×~ôÁÂÌ.~\ref{tab:thclasses} (ÔÕÄÁ ×ËÌÀÞÅÎÙ ÓÌÕÞÁÉ É ÑÚÙËÁ \KAT, Á ÎÅ
  46 ÔÏÌØËÏ \KA).
  47
  48 %% \newcommand*{\formulaType}{2}{
  49 %%   \begin{minipage}{8em}
  50 %%     #1\\
  51 %%     {\newcommand*{\formulaTypeParam}{##2}
  52 %%       \begin{mathdisplay}
  53 %%         \formulaTypeParam
  54 %%       \end{mathdisplay}}
  55 %%   \end{minipage}
  56 %% }
  57 %\newcommand*{\formulaType}[2]{#1 ${#2}$}
  58 %\newcommand*{\formulaType}[2]{\parbox{10em}{#1\\ ${#2}$}}
  59 \newcommand*{\formulaType}[2]{\begin{minipage}{11.8em}\smallskip #1\\ ${#2}$\smallskip \end{minipage}}
  60 \begin{table}[htbp]
  61   {\centering
  62   \begin{tabular}{l|cl}
  63     \multicolumn{1}{c|}{{\small\textbf{÷ÉÄ ÆÏÒÍÕÌ}}}
  64     &
  65     \multicolumn{2}{c}{\small\textbf{ëÌÁÓÓ ÔÅÏÒÉÊ Ó ÆÏÒÍÕÌÁÍÉ ÔÁËÏÇÏ
  66         ×ÉÄÁ}}\\
  67     &&{\small ÐÒÉÍÅÞÁÎÉÑ}\\
  68     \hline
  69     \hline
  70     \formulaType{\textbf{òÁ×ÅÎÓÔ×Á:} \eqref{eq:equa-formula}}{s = t}
  71     & \Equa
  72     &\parbox{10em}{\small \te
  73     $\Equa \eqdef \{ E \mid \text{$E$\T ÍÎÏÖÅÓÔ×Ï ÒÁ×ÅÎÓÔ×} \}$}
  74     \\
  75     \hline
  76     \formulaType{ÍÏÎÏÉÄÎÙÅ}{\sigma = \tau}
  77     & \MoEqua
  78     &{\small(${\MoEqua \subset \Equa}$)}
  79     \\
  80     \hline
  81     \formulaType{ÓÏÈÒÁÎÑÀÝÉÅ ÄÌÉÎÕ}{a_1 \dotsm a_k = b_1 \dotsm b_k}
  82     & \ConservEqua
  83     &{\small(${\ConservEqua \subset \MoEqua}$)}
  84     \\
  85     \hline
  86     \formulaType{ÕÓÌ-Ñ ËÏÍÍÕÔÁÔÉ×ÎÏÓÔÉ}{ab = ba}
  87     & \Commut
  88     &{\small(${\Commut \subset \ConservEqua}$)}
  89     \\
  90     \hline
  91     \formulaType{ÕÓÌ-Ñ ÎÅÓËÏÌØËÉÈ ÌÅÎÔ}{\text{\sm \eqref{eq:multitape-commut}}}
  92     & \MTape
  93     &{\small(${\MTape \subset \Commut}$)}
  94     \\
  95     \hline
  96     \formulaType{ÕÓÌ-Ñ ÁÎÎÉÇÉÌÑÃÉÉ}{s = 0}
  97     & \Annihil
  98     &{\small(${\Annihil \subset \Equa}$)}\\
  99     \hline
 100     \formulaType{ÕÓÌ-Ñ ÍÏÎÏÔÏÎÎÏÓÔÉ}{pa\n{p} = 0}
 101     & \Monot
 102     & {\small(${\Monot \subset \Shifts}$)}\\
 103     \hline
 104     \formulaType{ÕÓÌ-Ñ ÓÄ×ÉÇÁ}{
 105 %%       \begin{aligned}
 106 %%         pa\n{p} &= 0\\
 107 %%         \n{p}ap &= 0
 108 %%       \end{aligned}}
 109         pa\n{p} = 0 \text{ ÉÌÉ }  \n{p}ap = 0
 110       }
 111     & \Shifts
 112     &{\small(${\Shifts \subset \Annihil}$)}\\
 113     \hline\hline
 114     \formulaType{\textbf{Horn\dÆÏÒÍÕÌÙ:} \eqref{eq:Horn-formula}}%
 115     {E \implic s = t, \text{ ÇÄÅ } E \in \Equa}
 116     & \Horn\\
 117     \hline
 118     \formulaType{Horn\dÆÏÒÍÕÌÙ Ó ÐÏÓÙÌËÁÍÉ ×ÉÄÁ~$\thclass c \subseteq \Equa$}%
 119     {E \implic s = t, \text{ ÇÄÅ } E \in \thclass c}
 120     & $\Horn(\thclass c)$
 121     &\parbox{10em}{\small ÔÅÍ ÓÁÍÙÍ: $\Horn = \Horn(\Equa)$}
 122   \end{tabular}}
 123
 124   {\footnotesize
 125     ïÐÒÅÄÅÌÅÎÉÑ ÒÁ×ÅÎÓÔ× É Horn\dÆÏÒÍÕÌ ÎÅ ÐÒÉ×ÑÚÁÎÙ Ë ËÏÎËÒÅÔÎÏÍÕ
 126     ÑÚÙËÕ (ÓÉÇÎÁÔÕÒÁ ËÁËÁÑ ÕÇÏÄÎÏ);
 127     ÚÄÅÓØ $r$, $s$, $t$\T ÍÅÔÁÐÅÒÅÍÅÎÎÙÅ ÐÏ ÔÅÒÍÁÍ ÜÔÏÇÏ ÑÚÙËÁ.
 128     äÌÑ ÎÁÓ ÖÅ ÏÂÙÞÎÏ ÜÔÏ ÂÕÄÅÔ ÑÚÙË ÁÌÇÅÂÒ \KA ÉÌÉ \KAT (ÒÅÇÕÌÑÒÎÙÈ
 129     ×ÙÒÁÖÅÎÉÊ ÂÅÚ ÔÅÓÔÏ× ÉÌÉ Ó ÔÅÓÔÁÍÉ).
 130
 131     ïÓÔÁÌØÎÙÅ ×ÉÄÙ ÆÏÒÍÕÌ ÕÞÉÔÙ×ÁÀÔ ÓÐÅÃÉÆÉËÕ ÒÅÇÕÌÑÒÎÙÈ
 132     ×ÙÒÁÖÅÎÉÊ.
 133
 134     $\sigma$, $\tau$\T ÍÅÔÁÐÅÒÅÍÅÎÎÙÅ ÐÏ ÔÅÒÍÁÍ × ÑÚÙËÅ Ó ÓÉÇÎÁÔÕÒÏÊ
 135     ÍÏÎÏÉÄÁ (\te $\cdot$, 1),
 136     $a$, $b$, \dots\T ÍÅÔÁÐÅÒÅÍÅÎÎÙÅ ÐÏ ÂÁÚÏ×ÙÍ ÏÐÅÒÁÔÏÒÁÍ
 137     (ÜÌÅÍÅÎÔÁÍ ÎÅËÏÔÏÒÏÇÏ ÏÐÒÅÄÅÌ£ÎÎÏÇÏ ÁÌÆÁ×ÉÔÁ $\Sigma$), $p$\T
 138     ÍÅÔÁÐÅÒÅÍÅÎÎÙÅ ÐÏ ÂÁÚÏ×ÙÍ ÔÅÓÔÁÍ (ÜÌÅÍÅÎÔÁÍ ÎÅËÏÔÏÒÏÇÏ ÏÐÒÅÄÅÌ£ÎÎÏÇÏ
 139     ÁÌÆÁ×ÉÔÁ $T$;
 140     ÔÁËÉÅ ÆÏÒÍÕÌÙ ÒÁÓÓÍÁÔÒÉ×ÁÀÔÓÑ × çÌÁ×Å~\ref{cha:hypo-withTests}).
 141
 142   }
 143   ëÏÇÄÁ ÎÕÖÎÏ, ÂÕÄÅÔ ÕËÁÚÙ×ÁÔØÓÑ ÉÓÐÏÌØÚÕÅÍÙÊ ÎÁÂÏÒ ÂÁÚÏ×ÙÈ ÓÉÍ×ÏÌÏ×, ÎÁÐÒÉÍÅÒ:
 144   $\MoEqua_{\Sigma}$ ÉÌÉ $\MoEqua_{\Sigma,T}$.
 145
 146   \caption{ëÌÁÓÓÙ ÔÅÏÒÉÊ\T ÐÏ ÔÏÍÕ, ËÁËÏÇÏ ×ÉÄÁ × ÎÉÈ ×ÈÏÄÑÔ ÆÏÒÍÕÌÙ}
 147   \label{tab:thclasses}
 148 \end{table}
 149
 150 \paragraph{îÅËÏÔÏÒÙÅ ÎÁÂÌÀÄÅÎÉÑ ÎÁÄ Ó×ÑÚÑÍÉ ÍÅÖÄÕ ÔÅÏÒÉÑÍÉ}
 151 \label{problems-connections}
 152
 153 \begin{remark}[<<ï Ó×ÑÚÉ ÐÒÏÂÌÅÍ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ 1\dÇÏ É 2\dÇÏ ÒÏÄÁ>>]
 154 \label{rem:answer-2-for-1}
 155   $$
 156   \text{$\HOf_{\thclass c}\class C$ ÒÁÚÒÅÛÉÍÁ}
 157   \implies
 158   \text{$\HOf_{\{ E \}}\class C$ ÒÁÚÒÅÛÉÍÁ ÄÌÑ ÌÀÂÏÇÏ $E \in \thclass
 159     c$}
 160   $$
 161 ($E$\T ËÏÎÅÞÎÙÊ ÎÁÂÏÒ ÒÁ×ÅÎÓÔ×).
 162 áÌÇÏÒÉÔÍ, ÒÅÛÁÀÝÉÊ ×ÔÏÒÕÀ ÐÒÏÂÌÅÍÕ, ÐÏÌÕÞÁÅÔÓÑ ÓÐÅÃÉÁÌÉÚÁÃÉÅÊ
 163 ÁÌÇÏÒÉÔÍÁ ÄÌÑ ÐÅÒ×ÏÊ.
 164 \end{remark}
 165
 166 \begin{definition}
 167 ðÕÓÔØ $\Gamma$\T ËÌÁÓÓ ÐÁÒ ÍÏÄÅÌÅÊ É ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ
 168 $\RExp_{\Sigma}$, $\Phi$\T ÎÁÂÏÒ ÕÓÌÏ×ÉÊ × ÑÚÙËÅ $\RExp_{\Sigma}$.
 169 ïÂÏÚÎÁÞÉÍ $\Gamma | \Phi$ ÐÏÄËÌÁÓÓ
 170 ÍÏÄÅÌÅÊ É ÉÎÔÅÒÐÒÅÔÁÃÉÊ, ÕÄÏ×ÌÅÔ×ÏÒÑÀÝÉÈ $\Phi$:
 171 $$
 172 \Gamma | \Phi \eqdef \{ (\stru K, I) \in \Gamma \mid \stru K,I \models \Phi \}.
 173 $$
 174 \end{definition}
 175
 176 (òÅÞØ ÉÍÅÎÎÏ ÏÂ \emph{ÁÌÇÅÂÒÁÈ ëÌÉÎÉ} ÄÌÑ ËÒÁÔËÏÓÔÉ, ×Ó£ ÏÓÔÁÎÅÔÓÑ × ÓÉÌÅ É
 177 ÄÌÑ ÑÚÙËÁ × ÌÀÂÏÊ ÄÒÕÇÏÊ ÓÉÇÎÁÔÕÒÅ.)
 178
 179 \begin{remark}[<<ï ÐÒÏÂÌÅÍÁ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ 1\dÇÏ ÒÏÄÁ>>]\label{rem:HOf-EOf-1}
 180   ðÕÓÔØ $\Gamma$\T ËÌÁÓÓ ÐÁÒ ÁÌÇÅÂÒ
 181   É ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÈ ÉÎÔÅÒÐÒÅÔÁÃÉÊ ÂÁÚÏ×ÙÈ ÓÉÍ×ÏÌÏ×.
 182   ôÏÇÄÁ
 183   $$
 184   \text{$\HOf_{\{ E \}}\Gamma$ ÒÁÚÒÅÛÉÍÁ}
 185   \iff
 186   \text{$\EOf ( \Gamma | E )$ ÒÁÚÒÅÛÉÍÁ},
 187   $$
 188   É ÒÁÚÒÅÛÁÅÔ ÉÈ ÐÏ ÓÕÔÉ ÏÄÉÎ É ÔÏÔ ÖÅ ÁÌÇÏÒÉÔÍ.
 189 \end{remark}
 190
 191 ëÁË ÇÏ×ÏÒÉÌÏÓØ ×Ï ÷×ÅÄÅÎÉÉ (òÁÚÄÅÌ~\ref{sec:intro-problems},
 192 ÓÔÒ.~\pageref{2-problems}), ÍÙ ÈÏÔÉÍ ÎÁÊÔÉ ÕÓÌÏ×ÉÑ ÎÁ ×ÉÄ
 193 ÓÅÍÁÎÔÉÞÅÓËÉÈ ÐÏÓÔÕÌÁÔÏ×,
 194 ÎÅÏÂÈÏÄÉÍÙÅ É ÄÏÓÔÁÔÏÞÎÙÅ ÄÌÑ ÒÁÚÒÅÛÉÍÏÓÔÉ ÐÒÏÂÌÅÍÙ ÜË×É×ÁÌÅÎÔÎÏÓÔÉ
 195 ÐÒÏÇÒÁÍÍ ÐÒÉ ÄÏÐÕÝÅÎÉÉ ÜÔÉÈ ÓÅÍÁÎÔÉÞÅÓËÉÈ ÐÏÓÔÕÌÁÔÏ×, É ÜÔÁ ÚÁÄÁÞÁ ÍÏÖÅÔ
 196 ÂÙÔØ ÕÔÏÞÎÅÎÁ Ä×ÕÍÑ ÏÂÒÁÚÁÍÉ:
 197 \begin{enumerate}
 198 \item ðÒÏÂÌÅÍÁ 1:
 199   \begin{quote}
 200     \emph{<<îÁ ×ÈÏÄ ÐÏÄÁÀÔÓÑ Ä×Å ÐÒÏÇÒÁÍÍÙ. ïÐÒÅÄÅÌÉÔØ,
 201       ÜË×É×ÁÌÅÎÔÎÙ ÌÉ ÏÎÉ ÐÒÉ ÄÏÐÕÝÅÎÉÑÈ $E$.>>}
 202   \end{quote}
 203   $E$\T ÎÅÉÚÍÅÎÎÙÊ ÎÁÂÏÒ ÄÏÐÕÝÅÎÉÊ ÄÌÑ ËÁÖÄÏÇÏ ÁÌÇÏÒÉÔÍÁ.
 204   ÷ÏÐÒÏÓ: ÐÒÉ ËÁËÉÈ $E$ ÐÒÏÂÌÅÍÁ ÒÁÚÒÅÛÉÍÁ, Á ÐÒÉ
 205   ËÁËÉÈ\T ÎÅÔ. ïÔ×ÅÔÏÍ ÍÏÖÅÔ ÂÙÔØ ÎÅËÏÔÏÒÙÊ ËÌÁÓÓ $\thclass c = \{
 206   E_1, E_2, \dotsc \}$   ÄÏÐÕÝÅÎÉÊ.
 207
 208   ðÏÌÎÙÍ ÏÔ×ÅÔÏÍ ÂÕÄÅÔ ÔÁËÏÊ ËÌÁÓÓ $\thclass c$, ÍÁËÓÉÍÁÌØÎÙÊ ÐÏ ×ÌÏÖÅÎÉÀ.
 209 \item ðÒÏÂÌÅÍÁ 2:
 210   \begin{quote}
 211     \emph{<<îÁ ×ÈÏÄ ÐÏÄÁÀÔÓÑ ÄÏÐÕÝÅÎÉÑ~$E$ ÉÚ ËÌÁÓÓÁ
 212       $\thclass c$ É Ä×Å ÐÒÏÇÒÁÍÍÙ.
 213       ïÐÒÅÄÅÌÉÔØ, ÜË×É×ÁÌÅÎÔÎÙ ÌÉ ÏÎÉ ÐÒÉ ÄÏÐÕÝÅÎÉÑÈ $E$.>>}
 214   \end{quote}
 215   $E$\T ÔÏÖÅ Ñ×ÌÑÅÔÓÑ ×ÈÏÄÎÙÍÉ ÄÁÎÎÙÍÉ ÁÌÇÏÒÉÔÍÁ.
 216   $\thclass c$\T ÎÅÉÚÍÅÎÎÙÊ  ÄÌÑ ËÁÖÄÏÇÏ ÁÌÇÏÒÉÔÍÁ, ÒÅÛÁÀÝÅÇÏ ÐÒÏÂÌÅÍÕ.
 217   ÷ÏÐÒÏÓ: ÐÒÉ ËÁËÉÈ $\thclass c$ ÐÒÏÂÌÅÍÁ ÒÁÚÒÅÛÉÍÁ?
 218   ïÔ×ÅÔ ÄÏÌÖÅÎ ÏÐÒÅÄÅÌÉÔØ ÎÅËÏÔÏÒÏÅ ÍÎÏÖÅÓÔ×Ï ËÌÁÓÓÏ× ÄÏÐÕÝÅÎÉÊ $\{\thclass
 219   c_1, \thclass c_2, \dotsc, \}$, ÄÌÑ ËÁÖÄÏÇÏ ÉÚ ËÏÔÏÒÏÇÏ ÍÙ
 220   ÐÏÌÕÞÁÅÍ ÒÁÚÒÅÛÉÍÕÀ ÐÒÏÂÌÅÍÕ.
 221
 222   ðÏÌÎÙÍ ÏÔ×ÅÔÏÍ ÂÕÄÅÔ ÚÁÄÁÎÉÅ ÍÎÏÖÅÓÔ×Á ×ÓÅÈ ËÌÁÓÓÏ× ÄÏÐÕÝÅÎÉÊ,
 223   ÄÌÑ ËÁÖÄÏÇÏ ÉÚ ËÏÔÏÒÏÇÏ ÍÙ
 224   ÐÏÌÕÞÁÅÍ ÒÁÚÒÅÛÉÍÕÀ ÐÒÏÂÌÅÍÕ.
 225
 226 \end{enumerate}
 227
 228 íÙ ÏÇÒÁÎÉÞÉ×ÁÅÍ ÏÂÌÁÓÔØ, × ËÏÔÏÒÏÊ ÎÁÓ ÜÔÉ ×ÏÐÒÏÓÙ ÉÎÔÅÒÅÓÕÀÔ,
 229 ÐÏÓÔÕÌÁÔÁÍÉ, ×ÙÒÁÖÁÀÝÉÍÉ <<ÞÁÓÔÉÞÎÕÀ ËÏÍÍÕÔÁÔÉ×ÎÏÓÔØ
 230 É ÏÂÏÂÝ£ÎÎÕÀ ÍÏÎÏÔÏÎÎÏÓÔØ ÏÐÅÒÁÔÏÒÏ×>>:
 231 $E \in \Comm \oplus \Shifts$ É, ÓÔÁÌÏ ÂÙÔØ,
 232 $\thclass c \subseteq \Comm \oplus \Shifts$.
 233
 234 ðÕÓÔØ ÍÙ ÏÇÒÁÎÉÞÉ×ÁÅÍ ÉÓÓÌÅÄÏ×ÁÎÉÑ ËÌÁÓÓÏÍ ÓÅÍÁÎÔÉË, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÍ
 235 ÐÏÄËÌÁÓÓÕ ÁÌÇÅÂÒ ëÌÉÎÉ $\class C \subseteq \KA$ (ÉÌÉ \KAT), ÎÁÐÒÉÍÅÒ,
 236 $\class C = \KA$, ÉÌÉ $\class C = \KAc$, ÉÌÉ $\class C = \RKA$.
 237
 238 \begin{enumerate}
 239 \item
 240 ðÏÌÎÙÊ ÏÔ×ÅÔ ÎÁ ×ÏÐÒÏÓ~1 ÄÌÑ ÎÁÓ:
 241 ÎÁÊÔÉ $\thclass c \subseteq \Comm \oplus \Shifts$, ÔÁËÏÊ,
 242 ÞÔÏ
 243 $$
 244 \HOf_{ \{ E \} } \class C \text{ ÒÁÚÒÅÛÉÍÁ }
 245 \iff
 246 E \in \thclass c.
 247 $$
 248 %
 249 \item
 250 ðÏÌÎÙÊ ÏÔ×ÅÔ ÎÁ ×ÏÐÒÏÓ~2 ÄÌÑ ÎÁÓ:
 251 ÎÁÊÔÉ $\thclass C = \{ \thclass c_1, \thclass c_2, \dotsc \}
 252 \subseteq 2^{\Comm \oplus \Shifts}$, ÔÁËÏÅ,
 253 ÞÔÏ
 254 $$
 255 \HOf_{ \thclass c } \class C \text{ ÒÁÚÒÅÛÉÍÁ }
 256 \iff
 257 \thclass c \in \thclass C.
 258 $$
 259 \end{enumerate}
 260
 261 úÁÍÅÞÁÎÉÅ~\ref{rem:answer-2-for-1} ÐÏËÁÚÙ×ÁÅÔ, ÞÔÏ ÏÔ×ÅÔ ÎÁ ×ÔÏÒÏÊ
 262 ×ÏÐÒÏÓ ÄÁ£Ô ÏÔ×ÅÔ É ÎÁ ÐÅÒ×ÙÊ (ÜÔÏ ÏÔÍÅÞÁÌÏÓØ É ×Ï ÷×ÅÄÅÎÉÉ).
 263 úÁÍÅÞÁÎÉÅ~\ref{rem:HOf-EOf-1}
 264 ÐÏËÁÚÙ×ÁÅÔ, ÞÔÏ ×ÏÐÒÏÓ~1 ÍÏÖÎÏ Ó×ÅÓÔÉ Ë ×ÏÐÒÏÓÕ ÏÂ ÕÓÌÏ×ÉÑÈ
 265 ÎÁ~$E$ ÒÁÚÒÅÛÉÍÏÓÔÉ $\EOf (\class C | E)$ (ÜÔÏÔ ×ÏÐÒÏÓ × ÔÁËÏÊ
 266 ÆÏÒÍÕÌÉÒÏ×ËÅ ÎÁÍ ÂÕÄÅÔ ÕÄÏÂÎÅÅ ÒÅÛÁÔØ: ÍÙ ÂÕÄÅÍ ÏÓÎÏ×Ù×ÁÔØ ÒÁÓÓÕÖÄÅÎÉÑ ÎÁ Ó×ÑÚÑÈ
 267 ÁÌÇÅÂÒ, ÐÒÉÎÁÄÌÅÖÁÝÉÈ ÜÔÏÍÕ ËÌÁÓÓÕ, ÍÅÖÄÕ ÓÏÂÏÊ,
 268 ÎÁÐÒÉÍÅÒ, ËÏÇÄÁ ÎÁÍ ÕÄÁÓÔÓÑ
 269 Å£ ÐÏÓÔÒÏÉÔØ,
 270 ÎÁ Ó×ÅÄÅÎÉÑÈ Ï Ó×ÏÂÏÄÎÏÊ ÁÌÇÅÂÒÅ × ËÌÁÓÓÅ).
 271
 272 \paragraph{ïÐÉÓÁÎÉÅ ÕÓÌÏ×ÉÊ ÓÐÅÃÉÁÌØÎÏÇÏ ×ÉÄÁ: ËÏÍÍÕÔÁÔÉ×ÎÏÓÔØ.}
 273 ðÕÓÔØ $\Ecomm \in \Commut_\Sigma$\T ÕÓÌÏ×ÉÑ ËÏÍÍÕÔÁÔÉ×ÎÏÓÔÉ.
 274 ëÁÖÄÏÍÕ ÎÁÂÏÒÕ ÕÓÌÏ×ÉÊ ËÏÍÍÕÔÁÔÉ×ÎÏÓÔÉ ×ÚÁÉÍÎÏ ÏÄÎÏÚÎÁÞÎÏ
 275 ÓÏÏÔ×ÅÔÓÔ×ÕÅÔ \tING{ÏÔÎÏÛÅÎÉÅ ÎÅÚÁ×ÉÓÉÍÏÓÔÉ}, ÉÌÉ
 276 \tING{ËÏÍÍÕÔÁÔÉ×ÎÏÓÔÉ},
 277 $\IndepBy{\Ecomm}$ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× $\Sigma$:
 278 $$
 279  a \IndepBy{\Ecomm} b
 280  \iff
 281  (ab = ba) \in \Ecomm.
 282 $$
 283 ïÂÒÁÔÎÏÅ ÓÏÏÔ×ÅÔÓÔ×ÉÅ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ $\Ecomm(\Indep)$.
 284
 285 \subsection{÷ÏÐÒÏÓÙ.}
 286 ÷ çÌÁ×ÁÈ~\ref{cha:hypo-plain}, \ref{cha:hypo-withTests}
 287 ÎÁ ÔÅÈÎÉÞÅÓËÏÍ ÕÒÏ×ÎÅ ÎÁÛÅÇÏ ÉÓÓÌÅÄÏ×ÁÎÉÑ ÎÁÓ ÉÎÔÅÒÅÓÕÀÔ ×Ó£ ÔÅ ÖÅ
 288 ×ÏÐÒÏÓÙ,
 289 ÞÔÏ ÂÙÌÉ ÕËÁÚÁÎÙ × ÐÒÅÄÙÄÕÝÉÈ çÌÁ×ÁÈ, ÔÏÌØËÏ × ÐÒÉÍÅÎÅÎÉÉ Ë Horn\DÔÅÏÒÉÑÍ
 290 ÁÌÇÅÂÒ ëÌÉÎÉ É ÁÌÇÅÂÒ ëÌÉÎÉ Ó ÔÅÓÔÁÍÉ, Á ÎÅ ÜË×ÁÃÉÏÎÁÌØÎÙÍ.
 291
 292 çÌÁ×ÎÙÍ ÏÂÒÁÚÏÍ ÎÁÍ ÓÔÏÉÔ ÓËÏÎÃÅÎÔÒÉÒÏ×ÁÔØ ×ÎÉÍÁÎÉÅ ÎÁ ÒÅÌÑÃÉÏÎÎÙÈ É
 293 ÔÒÁÓÓÏ×ÙÈ ÍÏÄÅÌÑÈ, \tk ÉÍÅÎÎÏ ÏÎÉ ÌÕÞÛÅ ×ÓÅÇÏ ÓÏÏÔ×ÅÔÓÔ×ÕÀÔ
 294 ÔÒÁÄÉÃÉÏÎÎÏ ÉÓÐÏÌØÚÕÅÍÙÍ ÓÐÏÓÏÂÁÍ ÏÐÉÓÁÎÉÑ ÓÅÍÁÎÔÉË ÐÒÏÇÒÁÍÍ. ÷ÎÅ ÜÔÉÈ
 295 ËÌÁÓÓÏ× ÍÏÄÅÌÅÊ ÍÎÏÇÉÅ ×ÏÐÒÏÓÙ ÔÒÅÂÕÀÔ ÄÒÕÇÉÈ ÍÅÔÏÄÏ× ÒÅÛÅÎÉÑ, ËÏÔÏÒÙÅ
 296 ÎÅ ×ÏÊÄÕÔ × ÎÁÛÅ ÉÓÓÌÅÄÏ×ÁÎÉÅ.
 297
 298 ãÅÌÉ ÎÁÛÅÇÏ ÏÓÎÏ×ÎÏÇÏ
 299 ÉÓÓÌÅÄÏ×ÁÎÉÑ ÏËÁÚÙ×ÁÀÔÓÑ × ÒÁÍËÁÈ $\Horn{(\Commut \oplus
 300 \Shifts)}$\dÔÅÏÒÉÊ ËÌÁÓÓÏ× ÁÌÇÅÂÒ ëÌÉÎÉ.\footnote{ëÁË ÕÖÅ ÏÔÍÅÞÁÌÏÓØ ÎÁ
 301   ÓÔÒ.~\pageref{monot-in-title}, × ÎÁÚ×ÁÎÉÉ ÒÁÂÏÔÙ ÉÓÐÏÌØÚÏ×ÁÎÏ ÂÏÌÅÅ
 302   ÐÒÉ×ÙÞÎÏÅ ÓÌÏ×Ï <<ÍÏÎÏÔÏÎÎÏÓÔØ>>, ÞÔÏ ÓÏÏÔ×ÅÔÓÔ×Ï×ÁÌÏ ÂÙ
 303   ÉÓÓÌÅÄÏ×ÁÎÉÀ ËÌÁÓÓÁ~$\Horn(\Commut \oplus \Shifts)$, ÎÏ ÎÁ ÓÁÍÏÍ ÄÅÌÅ
 304   ÉÍÅÅÔÓÑ × ×ÉÄÕ ÂÏÌÅÅ ÛÉÒÏËÁÑ ÚÁÄÁÞÁ ÄÌÑ ËÌÁÓÓÁ ÆÏÒÍÕÌ $\Shifts$\T
 305   ÏÂÏÂÝÁÀÝÉÈ $\Monot$.}
 306 ÷ ÜÔÏÊ ÇÌÁ×Å, ÒÁÂÏÔÁÑ Ó \KA, Á ÎÅ \KAT, ÍÙ ÓÍÏÖÅÍ ÐÏËÒÙÔØ ÔÏÌØËÏ
 307 ÓÌÕÞÁÊ $\Horn(\Commut)$
 308 É ÓÄÅÌÁÔØ ÎÁÂÌÀÄÅÎÉÑ, ×ÁÖÎÙÅ ÄÌÑ ÉÓÓÌÅÄÏ×ÁÎÉÑ × ÄÁÌØÎÅÊÛÅÍ
 309 ÓÌÕÞÁÑ $\Horn(\Commut \oplus \Shifts)$.
 310
 311 \paragraph{ðÅÒ×ÙÊ ×ÚÇÌÑÄ.}
 312
 313 éÔÁË \todo{?}:
 314 \begin{equation}
 315   \label{eq:KA-inclu}
 316   \HornOf\RKA \supsetneq \HornOf\KAc \supsetneq \HornOf\KA.
 317 \end{equation}
 318
 319
 320 \paragraph{ôÅÏÒÅÍÁ ëÌÉÎÉ.}
 321 é × ÜÔÏÍ ÓÌÕÞÁÅ, ôÅÏÒÅÍÁ ëÌÉÎÉ~\ref{th:KA-Kleene}
 322 ÎÁÍ ÏÐÑÔØ ÐÏÚ×ÏÌÑÅÔ ÎÅ ÄÅÌÁÔØ ÒÁÚÎÉÃÙ ×
 323 Horn\dÔÅÏÒÉÑÈ ÍÅÖÄÕ ÌÉÎÅÊÎÏÊ
 324 ÚÁÐÉÓØÀ <<ÎÅÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ>> ÐÒÏÇÒÁÍÍ É ÇÒÁÆÏ×ÙÍ ÐÒÅÄÓÔÁ×ÌÅÎÉÅÍ.
 325
 326
 327 %%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%%
 328 \subsection{íÏÎÏÉÄÎÙÅ ÒÁ×ÅÎÓÔ×Á × ËÁÞÅÓÔ×Å ÄÏÐÕÝÅÎÉÊ}
 329 \label{sec:monoid-hypo}
 330
 331 ÷ ÜÔÏÊ ÞÁÓÔÉ ÉÓÓÌÅÄÏ×ÁÎÉÑ ÎÁÍ ÕÄÁÓÔÓÑ ×Ï ÍÎÏÇÏÍ ÐÏ×ÔÏÒÉÔØ ÎÁ ÏÂÝÅÍ
 332 ÕÒÏ×ÎÅ
 333 ÓÉÓÔÅÍÕ ÒÅÚÕÌØÔÁÔÏ× ÄÌÑ ÞÁÓÔÎÏÇÏ ÓÌÕÞÁÑ ÏÔÓÕÔÓÔ×ÉÑ ÄÏÐÕÝÅÎÉÊ (ÄÒÕÇÉÍÉ
 334 ÓÌÏ×ÁÍÉ, ÐÒÉÓÕÔÓÔ×ÉÑ ÄÏÐÕÝÅÎÉÊ\DÍÏÎÏÉÄÎÙÈ ÒÁ×ÅÎÓÔ× $\Emonoid =
 335 \emptyset$),
 336 ÐÏÌÕÞÅÎÎÙÅ × òÁÚÄÅÌÅ~\ref{sec:free-plain-ndet}.
 337
 338 ÂÕÄÅÍ ÏÔÔÁÌËÉ×ÁÔØÓÑ ÏÔ ÏÐÒÅÄÅÌÅÎÉÑ É Ó×ÏÊÓÔ×
 339
 340
 341 \subsubsection{íÏÄÅÌÉ: ÓÅÍÅÊÓÔ×Á ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÎÁÄ ÍÏÎÏÉÄÁÍÉ}
 342 \label{sec:reg-over-mo}
 343 ïÂÏÂÝÉÍ ÐÏÓÔÒÏÅÎÉÅ
 344 ÓÅÍÅÊÓÔ×Á ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ËÏÎÅÞÎÙÈ ÓÔÒÏË $\Reg_\Sigma$\T \sm
 345 òÁÚÄÅÌ~\ref{sec:reg-sigma}.
 346
 347 óÎÁÞÁÌÁ ×ÓÐÏÍÎÉÍ ïÐÒÅÄÅÌÅÎÉÅ~\ref{def:reg-sigma} $\Reg_\Sigma$ É ÄÁÄÉÍ
 348 ÜË×É×ÁÌÅÎÔÎÏÅ ÅÍÕ ïÐÒÅÄÅÌÅÎÉÅ, ÏÔÔÁÌËÉ×ÁÀÝÅÅÓÑ × ÏÔÌÉÞÉÅ ÏÔ ÔÏÇÏ
 349 ÎÅÐÏÓÒÅÄÓÔ×ÅÎÎÏ ÏÔ ÎÉÖÅÌÅÖÁÝÅÇÏ ÍÏÎÏÉÄÁ ËÏÎÅÞÎÙÈ ÓÔÒÏË (ÂÅÚ ×Ï×ÌÅÞÅÎÉÑ
 350 × ÏÐÒÅÄÅÌÅÎÉÅ ÉÎÔÅÒÐÒÅÔÁÃÉÉ $R_\Sigma$).
 351
 352 \begin{definition}
 353 \label{def:reg-over-str}
 354 íÉÎÉÍÁÌØÎÁÑ ÐÏÄÁÌÇÅÂÒÁ
 355 ÁÌÇÅÂÒÙ ëÌÉÎÉ~$(2^{\Strs(\Sigma)}; \cup, \cdot, {}^*, \emptyset, \{ \eStr \} )$,
 356 ÓÏÄÅÒÖÁÝÁÑ ÜÌÅÍÅÎÔÙ ×ÉÄÁ $\{ x \}$ ÄÌÑ ×ÓÅÈ ÓÔÒÏË $x \in \Strs(\Sigma)$, ÎÁÚÙ×ÁÅÔÓÑ
 357 \tING{ÁÌÇÅÂÒÏÊ ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ×} ÎÁÄ~$\Strs(\Sigma)$ É ÏÂÏÚÎÁÞÁÅÔÓÑ
 358 $\REG \Strs(\Sigma)$ ÉÌÉ, ËÏÒÏÞÅ, $\Reg_{\Sigma}$.
 359
 360 ëÁÎÏÎÉÞÅÓËÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ $\Sigma$ × ÎÅÊ\T $R_\Sigma(a) \eqdef \{ a \}$.
 361 \end{definition}
 362
 363 ëÁË ÕÖÅ ÂÙÌÏ ÚÁÍÅÞÅÎÏ ÒÁÎØÛÅ,
 364 ÉÚ *\dÎÅÐÒÅÒÙ×ÎÏÓÔÉ ÁÌÇÅÂÒÙ ëÌÉÎÉ~$2^{\Strs(\Sigma)}$
 365 (õÔ×.~\ref{prop:all-str-cont})
 366 ÓÌÅÄÕÅÔ
 367 \begin{proposition}\label{prop:reg-over-str-cont}
 368   áÌÇÅÂÒÁ ëÌÉÎÉ $\REG \Strs(\Sigma)$ *\dÎÅÐÒÅÒÙ×ÎÁ.
 369 \end{proposition}
 370
 371 ïÐÒÅÄÅÌÅÎÉÅ~\ref{def:reg-over-str} É ×Ó£ ÐÒÏ×ÅÄ£ÎÎÏÅ ÐÏÓÔÒÏÅÎÉÅ ÌÅÇËÏ
 372 ÏÂÏÂÝÁÅÔÓÑ ÎÁ ÓÌÕÞÁÊ ÐÒÏÉÚ×ÏÌØÎÙÈ ÍÏÎÏÉÄÏ× ×ÍÅÓÔÏ $\Strs(\Sigma)$\T
 373 \cite[Section~2.2--2.3]{KA-complexity}:
 374
 375 ðÕÓÔØ $\mo M = (M; \cdot, 1_{\mo M})$\T ÍÏÎÏÉÄ. $2^{\mo M}$ ÏÂÒÁÚÕÅÔ
 376 *\dÎÅÐÒÅÒÙ×ÎÕÀ
 377 ÁÌÇÅÂÒÕ ëÌÉÎÉ (ÏÐÅÒÁÃÉÉ ÎÁ ÍÎÏÖÅÓÔ×ÁÈ ÜÌÅÍÅÎÔÏ× ÍÏÎÏÉÄÁ ÏÐÒÅÄÅÌÑÀÔÓÑ
 378 ÔÁË ÖÅ, ËÁË ÜÔÏ ÄÅÌÁÌÏÓØ ÄÌÑ ÍÎÏÖÅÓÔ× ÓÔÒÏË.) ïÔÏÂÒÁÖÅÎÉÅ $\rho_{\mo M}\colon x
 379 \mapsto \{ x \}$\T ÇÏÍÏÍÏÒÆÉÚÍ ÍÏÎÏÉÄÁ $\mo M$ × ÍÕÌØÔÉÐÌÉËÁÔÉ×ÎÙÊ
 380 ÍÏÎÏÉÄ $2^{\mo M}$. $\REG \mo M$\T ÍÉÎÉÍÁÌØÎÁÑ ÐÏÄÁÌÇÅÂÒÁ $2^{\mo M}$,
 381 ÓÏÄÅÒÖÁÝÁÑ ÏÂÒÁÚ~$\mo M$ ÐÒÉ ÏÔÏÂÒÁÖÅÎÉÉ~$\rho_{\mo M}$; ÏÎÁ
 382 ÎÁÚÙ×ÁÅÔÓÑ ÁÌÇÅÂÒÏÊ ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ× ÎÁÄ~$\mo M$.
 383
 384 $\REG$\T ÆÕÎËÔÏÒ ÉÚ ËÁÔÅÇÏÒÉÉ~\Mo ÍÏÎÏÉÄÏ× É ÉÈ ÇÏÍÏÍÏÒÆÉÚÍÏ× ×
 385 ËÁÔÅÇÏÒÉÀ~\KAc *\dÎÅÐÒÅÒÙ×ÎÙÈ ÁÌÇÅÂÒ ëÌÉÎÉ É ÉÈ ÇÏÍÏÍÏÒÆÉÚÍÏ×.
 386
 387 \todo{[ÎÁÐÉÓÁÔØ ÅÝ£?]}
 388
 389 ïÂÏÂÝÅÎÉÅ õÔ×.~\ref{prop:Reg-Rel-iso}:
 390 \begin{proposition}
 391   \label{prop:Cons-Rel-iso}
 392   ðÕÓÔØ $\mo M$\T ÍÏÎÏÉÄ Ó ÌÅ×ÙÍ ÓÏËÒÁÝÅÎÉÅÍ.
 393   ôÏÇÄÁ $\REG \mo M$ ÉÚÏÍÏÒÆÎÁ $\relReg_{\kf F_{\mo M}}$.
 394 \end{proposition}
 395 \begin{proof}
 396 ôÁË ÖÅ, ËÁË   õÔ×.~\ref{prop:Reg-Rel-iso}.
 397 \end{proof}
 398
 399 \subsubsection{ó×ÏÂÏÄÎÙÅ ÍÏÎÏÉÄÙ}
 400
 401 ðÕÓÔØ $\Emonoid \in \MoEqua_\Sigma$\T ËÏÎÅÞÎÙÊ ÎÁÂÏÒ ÍÏÎÏÉÄÎÙÈ ÒÁ×ÅÎÓÔ×.
 402 $\mo M_0(\Sigma, \Emonoid)$\T Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ, ÐÏÒÏÖÄ£ÎÎÙÊ~$\Sigma$, Ó
 403 ÓÏÏÔÎÏÛÅÎÉÑÍÉ $\Emonoid$, \te:
 404 $$
 405 \mo M_0(\Sigma, \Emonoid) \models \sigma = \tau
 406 \iff
 407 \Mo|\Emonoid \models \sigma = \tau.
 408 $$
 409 \todo{[ÏÎ ÓÕÝÅÓÔ×ÕÅÔ ÐÏ ÏÂÝÉÍ ÓÏÏÂÒÁÖÅÎÉÑÍ; ËÁËÉÍ?]}.
 410
 411 \begin{remark}
 412   $\Strs(\Sigma)$\T Ó×ÏÂÏÄÎÙÊ ÍÏÎÏÉÄ, ÐÏÒÏÖÄ£ÎÎÙÊ~$\Sigma$, ÂÅÚ
 413   ÓÏÏÔÎÏÛÅÎÉÊ, × ÎÁÛÉÈ ÏÂÏÚÎÁÞÅÎÉÑÈ, $\mo M_0(\Sigma, \emptyset)$.
 414   ïÔÎÙÎÅ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ ÅÇÏ $\Sigma^*$, ËÁË ÜÔÏ ÏÂÙÞÎÏ ÐÒÉÎÑÔÏ.
 415 \end{remark}
 416
 417 \begin{definition}
 418   $\Cons_{\Sigma,\Emonoid} \eqdef \REG \mo M_0(\Sigma, \Emonoid)$\T
 419   \tING{ÓÅÍÅÊÓÔ×Ï ÓÏ×ÍÅÓÔÎÙÈ Ó $\Emonoid$ ÒÅÇÕÌÑÒÎÙÈ ÍÎÏÖÅÓÔ×
 420     ÜÌÅÍÅÎÔÏ× ÍÏÎÏÉÄÁ}.
 421
 422   \tING{óÔÁÎÄÁÒÔÎÁÑ ÉÎÔÅÒÐÒÅÔÁÃÉÑ} \cite{KA-complexity}
 423   $R_{\mo M_0(\Sigma, \Emonoid)}\map \Sigma \to \Cons_{\Sigma,\Emonoid}$
 424   ÏÐÒÅÄÅÌÑÅÔÓÑ ÔÁË: $R_{\mo M_0(\Sigma, \Emonoid)}(a) = \{ [a]_{\mo M} \}$, ÇÄÅ
 425   $[a]_{\mo M}$\T
 426   ÜÌÅÍÅÎÔ $\mo M_0(\Sigma, \Emonoid)$, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÊ $a$.
 427 \end{definition}
 428 \begin{remark}
 429   $(\Reg_\Sigma, R_\Sigma) = (\Cons_{\Sigma,\emptyset}, R_{\Sigma,\Emonoid})$.
 430 \end{remark}
 431 äÁÌØÛÅ ÍÙ ÕÓÔÁÎÏ×ÉÍ, ÞÔÏ ÁÎÁÌÏÇÉÑ ÍÅÖÄÕ $\Reg_\Sigma$ É
 432 $\Cons_{\Sigma,\Emonoid}$ ÚÁÈÏÄÉÔ ÅÝ£ ÄÁÌØÛÅ\T
 433 $\Cons_{\Sigma,\Emonoid}$ Ñ×ÌÑÅÔÓÑ Ó×ÏÂÏÄÎÏÊ ÍÏÄÅÌØÀ × ËÌÁÓÓÅ
 434 $\KAc|\Emonoid$\T \sm ôÅÏÒÅÍÕ~\ref{th:cons-free}.
 435
 436 \begin{question}
 437   $\mo M_0(\Sigma, E)$ ×ÓÅÇÄÁ Ó ÌÅ×ÙÍ ÓÏËÒÁÝÅÎÉÅÍ?
 438
 439   ðÏ ËÒÁÊÎÅÊ ÍÅÒÅ, ÄÌÑ $E \in \Comm$\T ÄÁ.
 440 \end{question}
 441
 442 \subsubsection{ðÒÉÍÅÒ: ÍÎÏÇÏÌÅÎÔÏÞÎÙÅ Á×ÔÏÍÁÔÙ}
 443 %% îÁÐÏÍÉÎÁÎÉÅ ÏÐÒÅÄÅÌÅÎÉÑ:
 444 %% á×ÔÏÍÁÔÙ~\eqref{eq:2nfas} ÜË×É×ÁÌÅÎÔÎÙ × $\class C \subseteq \KA$:
 445 %% \begin{equation}
 446 %%   \label{eq:nfa-equiv-value}
 447 %%   \class C
 448 %%   \models
 449 %%   \smatrAny{I}' \smatrAny{M}'^* \transp{\smatrAny{F}'}
 450 %%   =
 451 %%   \smatrAny{I}'' \smatrAny{M}''^* \transp{\smatrAny{F}''}.
 452 %% \end{equation}
 453
 454 %% \todo{[ðÒÉÍÅÒÙ:]}
 455
 456 íÙ ÒÁÓÓÍÏÔÒÉÍ ÓÐÏÓÏÂ ×ÙÒÁÖÅÎÉÑ ÓÅÍÁÎÔÉËÉ \tING{(ÎÅÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÏÇÏ)
 457 ÍÎÏÇÏÌÅÎÔÏÞÎÏÇÏ Á×ÔÏÍÁÔÁ} (ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÅ ÍÎÏÇÏÌÅÎÔÏÞÎÙÅ Á×ÔÏÍÁÔÙ
 458 ÂÙÌÉ ××ÅÄÅÎÙ \cite{RS}).
 459
 460 <<ðÒÏÍÏÄÅÌÉÒÕÅÍ>> ÎÁÛÉÍÉ ÓÒÅÄÓÔ×ÁÍÉ $k$\dÌÅÎÔÏÞÎÙÅ
 461 Á×ÔÏÍÁÔÙ. óÎÁÞÁÌÁ ÍÙ ÐÒÅÄÌÏÖÉÍ ÓÅÍÁÎÔÉÞÅÓËÉÅ ÐÏÓÔÕÌÁÔÙ,
 462 ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÅ ÓÅÍÁÎÔÉËÅ $k$\dÌÅÎÔÏÞÎÙÈ Á×ÔÏÍÁÔÏ×, Á ÐÏÔÏÍ ÅÝ£ ÎÁÂÏÒ
 463 ÐÒÏÓÔÙÈ ÍÏÄÅÌÅÊ \KA, ÎÅÐÏÓÒÅÄÓÔ×ÅÎÎÏ ÏÔ×ÅÞÁÀÝÉÈ ÔÒÁÄÉÃÉÏÎÎÙÍ
 464 ÏÐÒÅÄÅÌÅÎÉÑÍ ÓÅÍÁÎÔÉËÉ $k$\dÌÅÎÔÏÞÎÙÈ Á×ÔÏÍÁÔÏ×.
 465
 466 ðÕÓÔØ ÉÓÐÏÌØÚÕÅÍÙÊ ÁÌÆÁ×ÉÔ~$\Sigma$ ÂÁÚÏ×ÙÈ ÏÐÅÒÁÔÏÒÏ× ÒÁÚÂÉÔ ÎÁ $k$
 467 ÞÁÓÔÅÊ\T ÐÏ ÞÉÓÌÕ ÌÅÎÔ:
 468 $\Sigma = {\Sigma_1 \cup \dotsb \cup \Sigma_k}$,
 469 $\Sigma_i \cap \Sigma_j = \emptyset \iff i \neq j$.
 470
 471 \paragraph{óÅÍÁÎÔÉÞÅÓËÉÅ ÐÏÓÔÕÌÁÔÙ: ÍÎÏÇÏÌÅÎÔÏÞÎÙÅ Á×ÔÏÍÁÔÙ.}
 472 óÅÍÁÎÔÉÞÅÓËÉÅ ÐÏÓÔÕÌÁÔÙ ÂÕÄÕÔ ÓÏÏÔ×ÅÔÓÔ×Ï×ÁÔØ ÄÏÐÕÝÅÎÉÑÍ~$E$\T ÕÓÌÏ×ÉÑÍ
 473 ËÏÍÍÕÔÁÔÉ×ÎÏÓÔÉ, ÚÁÄÁ×ÁÅÍÙÍ ÔÁËÉÍ ÏÔÎÏÛÅÎÉÅÍ~$\IndepBy{E}$
 474 ÎÅÚÁ×ÉÓÉÍÏÓÔÉ ÏÐÅÒÁÔÏÒÏ×:
 475 \begin{equation}
 476   \label{eq:multitape-commut}
 477   a \IndepBy{E} b \iff a \in \Sigma_i, b \in \Sigma_j, i \neq j.
 478 \end{equation}
 479
 480 ëÌÁÓÓ ×ÓÅÈ ÔÁËÉÈ ÎÁÂÏÒÏ× ÄÏÐÕÝÅÎÉÊ ÂÕÄÅÍ ÏÂÏÚÎÁÞÁÔØ
 481 $\MTape$. $\MTape(k)$\T ËÌÁÓÓ ÎÁÂÏÒÏ× ÄÏÐÕÝÅÎÉÊ, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÊ
 482 ÔÏÌØËÏ $k$\dÌÅÎÔÏÞÎÙÍ Á×ÔÏÍÁÔÁÍ; ÏÞÅ×ÉÄÎÏ, $\MTape(k) \subsetneq
 483 \MTape$.
 484
 485 îÁÓ ÍÏÖÅÔ ÉÎÔÅÒÅÓÏ×ÁÔØ ×ÏÐÒÏÓ Ï ÒÁÚÒÅÛÉÍÏÓÔÉ $\HOf_{\MTape} \class C$
 486 ÉÌÉ $\HOf_{\MTape(k)} \class C$ ÄÌÑ ÎÅËÏÔÏÒÏÇÏ~$k$ ËÁË ×ÏÐÒÏÓ Ï
 487 ÒÁÚÒÅÛÉÍÏÓÔÉ ðü ÍÎÏÇÏÌÅÎÔÏÞÎÙÈ Á×ÔÏÍÁÔÏ× ÐÒÉ ÔÁËÏÍ <<ÁËÓÉÏÍÁÔÉÞÅÓËÏÍ>>
 488 ÚÁÄÁÎÉÉ ÓÅÍÁÎÔÉËÉ; $\class C$ ÍÏÖÅÔ ÂÙÔØ, ÎÁÐÒÉÍÅÒ, $\KA$, $\KAc$,
 489 $\RKA$. äÁÌØÛÅ × ôÅÏÒÅÍÅ~\ref{th:REG-free} ÍÙ ÕÂÅÄÉÍÓÑ × ÔÏÍ, ÞÔÏ ÜÔÏ
 490 <<ÁËÓÉÏÍÁÔÉÞÅÓËÏÅ>> ÏÐÒÅÄÅÌÅÎÉÅ ÓÅÍÁÎÔÉËÉ ÍÎÏÇÏÌÅÎÔÏÞÎÙÈ Á×ÔÏÍÁÔÏ×
 491 ÓÏ×ÐÁÄ£Ô Ó ÏÐÒÅÄÅÌÅÎÉÅÍ ÎÁ ÏÓÎÏ×ÁÎÉÉ ËÏÎËÒÅÔÎÙÈ ÐÏÓÔÒÏÅÎÉÊ.
 492
 493 \begin{remark}
 494   $\MTape(1) = \{ \emptyset \}$, \tk × ÓÌÕÞÁÅ ÏÄÎÏÊ ÌÅÎÔÙ ÎÅÔ
 495   ÎÅÚÁ×ÉÓÉÍÙÈ ÏÐÅÒÁÔÏÒÏ×. üÔÏ ÓÌÕÞÁÊ çÌÁ×Ù~\ref{sec:free-plain}.
 496   $\HOf_{\MTape(1)} \class C = \EOf \class C$.
 497 \end{remark}
 498
 499
 500 \paragraph{<<ñÚÙË>>, ÒÁÓÐÏÚÎÁ×ÁÅÍÙÊ ÍÎÏÇÏÌÅÎÔÏÞÎÙÍ Á×ÔÏÍÁÔÏÍ\T
 501   <<ÇÌÏÂÁÌØÎÏÅ>> ÏÐÒÅÄÅÌÅÎÉÅ.}
 502 ðÕÓÔØ $E \in \MTape$ (ÕÓÌÏ×ÉÑ ÎÅÓËÏÌØËÉÈ ÌÅÎÔ) × ÁÌÆÁ×ÉÔÅ $\Sigma$,
 503 $\mo M_0 = \mo M_0(\Sigma, E)$.
 504 ïÂÒÁÔÉÍ ×ÎÉÍÁÎÉÅ ÎÁ $R_{\mo M_0}(s)$\T ÓÔÁÎÄÁÒÔÎÕÀ ÉÎÔÅÒÐÒÅÔÁÃÉÀ
 505 Á×ÔÏÍÁÔÎÏÇÏ ×ÙÒÁÖÅÎÉÑ~$s$ ×  $\REG \mo M_0$.
 506
 507 üÔÏ ÚÎÁÞÅÎÉÅ ÏÔÒÁÖÁÅÔ ÔÁËÏÅ ÔÒÁÄÉÃÉÏÎÎÏÅ <<ÇÌÏÂÁÌØÎÏÅ>> ÏÐÒÅÄÅÌÅÎÉÅ
 508 ÓÅÍÁÎÔÉËÉ $R'$ ÍÎÏÇÏÌÅÎÔÏÞÎÏÇÏ Á×ÔÏÍÁÔÁ ÎÁÄ $\Sigma$\T ÓÉÓÔÅÍÙ ÐÅÒÅÈÏÄÏ× $\au A$:
 509 \begin{multline}
 510   \label{eq:nfa-global-value}
 511   R'(\au A) \eqdef
 512   \bigcup_{\sigma \in \Trs(\au A)}
 513   \left\{ [\smatrAny{I}[\First(\sigma)] \Label(\sigma)
 514     \smatrAny{F}[\Last(\sigma)]]_{\mo M_0(\Sigma,E)} \right\}
 515   =
 516   \\
 517   =
 518   \sup_{\sigma \in \Trs(\au A)}
 519   R_{\Sigma,E} \left(\smatrAny{I}[\First(\sigma)] \Label(\sigma)
 520     \smatrAny{F}[\Last(\sigma)] \right).
 521 \end{multline}
 522 (\emph{<<çÌÏÂÁÌØÎÏÅ>>}, ÐÏÔÏÍÕ ÞÔÏ ÏÎÏ ÏÓÎÏ×ÁÎÏ ÎÁ ÇÌÏÂÁÌØÎÏÍ Ó×ÏÊÓÔ×Å
 523 ÓÉÓÔÅÍÙ ÐÅÒÅÈÏÄÏ×, ÐÒÅÄÓÔÁ×ÌÑÀÝÅÊ Á×ÔÏÍÁÔ; ×ÔÏÒÏÅ ×ÙÒÁÖÅÎÉÅ
 524 ×~\eqref{eq:nfa-global-value} ÄÁÎÏ ÐÏÌÎÏÓÔØÀ × ÔÅÒÍÉÎÁÈ ÏÐÅÒÁÃÉÊ \KA.)
 525
 526
 527 \paragraph{òÁÂÏÔÁ ÍÎÏÇÏÌÅÎÔÏÞÎÏÇÏ Á×ÔÏÍÁÔÁ ÎÁ ÂÅÓËÏÎÅÞÎÙÈ ÌÅÎÔÁÈ}
 528 ÷ ÜÔÏÍ É ÓÌÅÄÕÀÝÅÍ ÐÁÒÁÇÒÁÆÅ ÍÙ
 529 ÐÅÒÅÎÅÓ£Í ÎÁ ÓÌÕÞÁÊ ÎÅÓËÏÌØËÉÈ ÌÅÎÔ ÏÐÒÅÄÅÌÅÎÉÑ ÉÚ
 530 òÁÚÄÅÌÁ~\ref{sec:nfa-other-values}, ÄÁÎÎÙÅ ÄÌÑ Á×ÔÏÍÁÔÏ×, ÒÁÂÏÔÁÀÝÉÈ
 531 ÎÁ ÏÄÎÏÊ ÌÅÎÔÅ.
 532
 533 \begin{definition}
 534 ûËÁÌÁ ëÒÉÐËÅ $\kfITape^k(\omega_1, \dotsc, \omega_k)$,
 535 ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÁÑ $k$ ÂÅÓËÏÎÅÞÎÙÍ ÌÅÎÔÁÍ, ÎÁ
 536 ËÁÖÄÏÊ ÉÚ ËÏÔÏÒÙÈ ÚÁÐÉÓÁÎÁ Ó×ÏÑ  ÂÅÓËÏÎÅÞÎÁÑ ÓÔÒÏËÁ
 537 $\omega_j$ × ÁÌÆÁ×ÉÔÅ~$\Sigma_j$:
 538 $$
 539 \omega_j = a_{j,1} a_{j,2} \dotsm
 540 $$
 541 ÐÏÌÕÞÁÅÔÓÑ \tD{ÐÒÑÍÙÍ ÐÒÏÉÚ×ÅÄÅÎÉÅÍ}{def:kf-product}
 542 ÛËÁÌ, ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÈ ËÁÖÄÏÊ ÏÔÄÅÌØÎÏÊ ÌÅÎÔÅ:
 543 $$
 544 \kfITape^k(\omega_1, \dotsc, \omega_k) \eqdef
 545 \kfITape(\omega_1) \times \dotsb \times \kfITape(\omega_k).
 546 $$
 547
 548 $$
 549 \ITAPES^k_{\Sigma_1,\dotsc,\Sigma_k}
 550 \eqdef \{ (\relReg_{\kfITape^k(\omega_1, dotsc, \omega_k)}, \relIP)
 551 \mid \text{ ËÁÖÄÁÑ $\omega_j$\T ÂÅÓËÏÎÅÞÎÁÑ ÓÔÒÏËÁ ×~$\Sigma_j$} \}
 552 $$
 553 $$
 554 \ITAPES^k \eqdef \{ (\relReg_{\kfITape^k(\omega_1, dotsc, \omega_k)},
 555 \relIP)
 556 \mid \omega_j \text{\T ÂÅÓËÏÎÅÞÎÙÅ ÓÔÒÏËÉ} \}
 557 $$
 558 \end{definition}
 559
 560 <<çÌÏÂÁÌØÎÏÅ>> ÏÐÒÅÄÅÌÅÎÉÅ~\eqref{eq:mta-global-value}
 561 É ÎÁ <<ÂÅÓËÏÎÅÞÎÙÈ ÌÅÎÔÁÈ>>\T
 562 Ä×Á ÜË×É×ÁÌÅÎÔÎÙÈ ÓÐÏÓÏÂÁ ÏÐÒÅÄÅÌÅÎÉÑ ÓÅÍÁÎÔÉËÉ Á×ÔÏÍÁÔÁ:
 563 \begin{proposition}
 564   $$
 565   \ITAPES^k \models s = t
 566   \iff
 567   \Reg_{\Sigma, \Ecomm} \models s = t
 568   $$
 569   \todo{[$\Ecomm$ ÇÄÅ ÏÐÒ?]}
 570   (÷×ÉÄÕ ôÅÏÒÅÍÙ ëÌÉÎÉ~\ref{th:Kleene} ÔÕÔ ÎÁ ÓÁÍÏÍ ÄÅÌÅ ÎÅ×ÁÖÎÏ,
 571   ÉÍÅÅÍ ÌÉ ÍÙ × ×ÉÄÕ ÒÅÇÕÌÑÒÎÙÅ ÉÌÉ Á×ÔÏÍÁÔÎÙÅ ×ÙÒÁÖÅÎÉÑ ÎÁÄ $\Sigma$.)
 572 \end{proposition}
 573
 574 \paragraph{òÁÂÏÔÁ ÎÁ ËÏÎÅÞÎÙÈ ÌÅÎÔÁÈ.}
 575 \begin{definition}
 576 ðÕÓÔØ $\Sigma \cap \{ \Stop \} = \emptyset$.
 577 \tING{ûËÁÌÁ ëÒÉÐËÅ $\kfFTape^k(\sigma_1, \dotsc, \sigma_k)$,
 578 ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÁÑ ÌÅÎÔÁÍ, ÎÁ
 579 ËÏÔÏÒÙÈ ÚÁÐÉÓÁÎÙ ËÏÎÅÞÎÙÅ ÓÔÒÏËÉ $\sigma_j$ × ÁÌÆÁ×ÉÔÅ~$\Sigma_j$ :
 580 $$
 581 \sigma_j = a_{j,1} a_{j,2} \dotsm a_{j,n_j}
 582 $$
 583 Ó ÏÇÒÁÎÉÞÉÔÅÌÅÍ}
 584 ÐÏÌÕÞÁÅÔÓÑ ÐÒÑÍÙÍ ÐÒÏÉÚ×ÅÄÅÎÉÅÍ ÛËÁÌ ëÒÉÐËÅ,
 585 ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÉÈ ËÁÖÄÏÊ ÏÔÄÅÌØÎÏÊ ÌÅÎÔÅ Ó ÏÇÒÁÎÉÞÉÔÅÌÅÍ:
 586 $$
 587 \kfFTape^k(\sigma_1, \dotsc, \sigma_k)
 588 =
 589 \kfFTape(\sigma_1) \times \dotsb \times \kfFTape(\sigma_k).
 590 $$
 591 $$
 592 \Accepts^k(\sigma_1, \dotsc, \sigma_k) \eqdef
 593 (\relReg_{\kfFTape^k(\sigma_1, \dotsc, \sigma_k)}, \relIP)
 594 $$
 595 $$
 596 \FTAPES^k_{\Sigma_1, \dotsc, \Sigma_k}
 597 \eqdef \{  \Accepts^k(\sigma_1, \dotsc, \sigma_k)
 598 \mid \sigma_j \text{\T ËÏÎÅÞÎÁÑ ÓÔÒÏËÁ ×~$\Sigma_j$} \}
 599 $$
 600 $$
 601 \FTAPES^k \eqdef \{ \Accepts^k(\sigma_1, \dotsc, \sigma_k)
 602 \mid \sigma_j \text{\T ËÏÎÅÞÎÁÑ
 603   ÓÔÒÏËÁ × ÁÌÆÁ×ÉÔÅ ÂÅÚ $\Stop$} \}
 604 $$
 605 \end{definition}
 606
 607 ðÕÓÔØ $\Sigma \cap \{ \Stop \} = \emptyset$.
 608 \tING{á×ÔÏÍÁÔ ÎÁÄ~$\Sigma = \Sigma_1, \dotsc, \Sigma_k$ ÐÒÉÎÉÍÁÅÔ ÌÅÎÔÙ ÓÏ ÓÔÒÏËÁÍÉ}~$\sigma_1, \dotsc, \sigma_k$ ×
 609 ÜÔÉÈ ÁÌÆÁ×ÉÔÁÈ, ÅÓÌÉ ÄÌÑ ÓÏÏÔ×ÅÔÓÔ×ÕÀÝÅÇÏ ÜÔÏÍÕ Á×ÔÏÍÁÔÕ
 610 Á×ÔÏÍÁÔÎÏÇÏ ×ÙÒÁÖÅÎÉÑ~$s \in \AExp_\Sigma$:
 611 $$
 612 \Accepts^k(\sigma_1, \dotsc, \sigma_k) \models s \cdot \Stop \neq 0.
 613 $$
 614 ÷ ÜÔÏÍ ÓÌÕÞÁÅ $\relI{s \cdot \Stop}_{\kfFTape^k(\sigma_1, \dotsc, \sigma_k)} = (u,v)$, ÇÄÅ
 615 $u$ É~$v$\T <<ÐÅÒ×ÏÅ>> É <<ÐÏÓÌÅÄÎÅÅ>> ÓÏÓÔÏÑÎÉÅ ÛËÁÌÙ
 616 ëÒÉÐËÅ~$\kfFTape^k(\sigma_1, \dotsc, \sigma_k)$.
 617
 618 \todo{[ÔÝÁÔÅÌØÎÏ ÐÒÏ×ÅÒÉÔØ. ëÁË ÓÏÏÔÎÏÓÉÔÓÑ Ó \cite{RS}?]}
 619
 620 üÔÏ ÏÐÒÅÄÅÌÅÎÉÅ ÏÔÒÁÖÁÅÔ ÔÁËÏÅ ÔÒÁÄÉÃÉÏÎÎÏÅ ÏÐÒÅÄÅÌÅÎÉÅ ÓÅÍÁÎÔÉËÉ
 621 Á×ÔÏÍÁÔÁ, ÏÓÎÏ×ÁÎÎÏÅ ÎÁ ÒÁÓÓÍÏÔÒÅÎÉÉ ÒÁÂÏÔÙ Á×ÔÏÍÁÔÁ ÎÁ ËÁÖÄÏÍ
 622 ×ÏÚÍÏÖÎÏÍ ÎÁÂÏÒÅ ÉÚ $k$ ÌÅÎÔ:
 623 \begin{multline}
 624 \au A \text{ ÐÒÉÎÉÍÁÅÔ $\sigma_1, \dotsc, \sigma_k$ ÎÁ ÌÅÎÔÁÈ }
 625 \iffdef\\
 626 \iffdef
 627 \au A \text{ ÐÒÉ ÒÁÂÏÔÅ ÎÁ ÌÅÎÔÁÈ $\sigma_1, \dotsc, \sigma_k$ ÐÅÒÅÈÏÄÉÔ ÉÚ
 628   ÎÁÞÁÌØÎÏÇÏ ÓÏÓÔÏÑÎÉÑ × ËÏÎÅÞÎÏÅ.}
 629 \end{multline}
 630 é ÔÏÇÄÁ
 631 $$
 632 R''(\au A) \eqdef
 633 \{ \sigma \mid \au A \text{ ÐÒÉÎÉÍÁÅÔ ÌÅÎÔÙ $\sigma_1, \dotsc, \sigma_k$ } \}.
 634 $$
 635
 636 <<çÌÏÂÁÌØÎÏÅ>> ÏÐÒÅÄÅÌÅÎÉÅ~\eqref{eq:nfa-global-value}
 637 É ÎÁ <<ËÏÎÅÞÎÙÈ ÌÅÎÔÁÈ>>\T
 638 Ä×Á ÜË×É×ÁÌÅÎÔÎÙÈ ÓÐÏÓÏÂÁ ÏÐÒÅÄÅÌÅÎÉÑ ÓÅÍÁÎÔÉËÉ Á×ÔÏÍÁÔÁ:
 639
 640 \begin{proposition}[üË×É×ÁÌÅÎÔÎÏÓÔØ Ä×ÕÈ ÓÅÍÁÎÔÉË.]
 641   ðÕÓÔØ $\Sigma \cap \{ \Stop \} = \emptyset$.
 642   $$
 643   \FTAPES^k \models s \cdot \Stop = t \cdot \Stop
 644   \iff
 645   \Reg_{\Sigma,\Ecomm} \models s = t,
 646   $$
 647   ÇÄÅ $s$ É $t$ ÏÐÑÔØ\T Á×ÔÏÍÁÔÎÙÅ ÉÌÉ ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ ÎÁÄ~$\Sigma$.
 648 \end{proposition}
 649
 650
 651 \subsubsection{ó×ÏÂÏÄÎÙÅ ÍÏÄÅÌÉ}
 652 \label{sec:hypo-plain-freeModels}
 653
 654 \todo{[ÐÁÒÁ (ÁÌÇÅÂÒÁ, ÉÎÔÅÒÐÒ) -- ÍÏÄÅÌØ?]}
 655 ó×ÏÂÏÄÎÏÊ ÍÏÄÅÌØÀ × ËÌÁÓÓÅ ÁÌÇÅÂÒ $\class C$, ÐÏÒÏÖÄ£ÎÎÏÊ $\Sigma$,
 656 ÍÙ ÎÁÚÙ×ÁÅÍ ÔÁËÕÀ ÁÌÇÅÂÒÕ $\ka K_0 \in \class C$ É ÉÎÔÅÒÐÒÅÔÁÃÉÀ
 657 $I_0\colon Z_\Sigma \to \ka K_0$, ÞÔÏ
 658 $$
 659 \class C \models s = t
 660 \iff
 661 \ka K_0, I_0 \models s = t,
 662 $$
 663 ÇÄÅ $Z$\T ÍÎÏÖÅÓÔ×Ï ÔÅÒÍÏ× × ÓÉÇÎÁÔÕÒÅ ÜÔÏÇÏ ËÌÁÓÓÁ ÁÌÇÅÂÒ,
 664 $s, t \in Z_\Sigma$ (ÔÅÒÍÙ ÉÚ $Z$, ÉÓÐÏÌØÚÕÀÝÉÅ ÂÁÚÏ×ÙÅ ÓÉÍ×ÏÌÙ ÉÚ~$\Sigma$).
 665 íÙ ÏÂÙÞÎÏ ÒÁÓÓÍÁÔÒÉ×ÁÅÍ ËÌÁÓÓÙ ÁÌÇÅÂÒ ëÌÉÎÉ (ÐÏÄËÌÁÓÓÙ \KA)
 666 É ÒÅÇÕÌÑÒÎÙÅ ×ÙÒÁÖÅÎÉÑ ($\RExp_\Sigma$) × ËÁÞÅÓÔ×Å ÔÅÒÍÏ×
 667 ÉÌÉ ËÌÁÓÓÙ ÁÌÇÅÂÒ ëÌÉÎÉ ÍÁÔÒÉÃ, ÉÎÄÕÃÉÒÏ×ÁÎÎÙÈ ÁÌÇÅÂÒÁÍÉ ëÌÉÎÉ,
 668 (ÐÏÄËÌÁÓÓÙ $\kaMat(\ka K)$,
 669 × ÏÂÏÚÎÁÞÅÎÉÑÈ ÍÙ ÔÁËÉÅ ÁÌÇÅÂÒÙ ÍÁÔÒÉÃ ÉÄÅÎÔÉÆÉÃÉÒÕÅÍ Ó ÉÓÈÏÄÎÙÍÉ
 670 ÁÌÇÅÂÒÁÍÉ ëÌÉÎÉ)
 671 É Á×ÔÏÍÁÔÎÙÅ ×ÙÒÁÖÅÎÉÑ ($\AExp_\Sigma$).
 672 íÙ ÍÏÖÅÍ ÎÅ ÒÁÚÌÉÞÁÔØ,
 673 ÇÏ×ÏÒÉÍ ÍÙ ÏÂ ÁÌÇÅÂÒÅ ëÌÉÎÉ ÉÌÉ ÏÂ ÉÎÄÕÃÉÒÏ×ÁÎÎÏÊ ÁÌÇÅÂÒÅ ÍÁÔÒÉÃ É ÐÒÉ
 674 ÒÁÚÇÏ×ÏÒÅ Ï Ó×ÏÂÏÄÎÙÈ ÍÏÄÅÌÑÈ, ÐÏÔÏÍÕ ÞÔÏ Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ × ËÌÁÓÓÅ
 675 ÁÌÇÅÂÒ ëÌÉÎÉ ÉÎÄÕÃÉÒÕÅÔ Ó×ÏÂÏÄÎÕÀ ÍÏÄÅÌØ × ËÌÁÓÓÅ ÉÎÄÕÃÉÒÏ×ÁÎÎÙÈ ÉÍÉ
 676 ÁÌÇÅÂÒ ÍÁÔÒÉÃ:
 677 \begin{proposition}
 678   åÓÌÉ $\ka K_0, I_0$\T Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ, ÐÏÒÏÖÄ£ÎÎÁÑ $\Sigma$, ×
 679   $\class C \subseteq \KA$, ÔÏ
 680   $$
 681   \class C \models s = t
 682   \iff
 683   \ka K_0, I_0 \models s = t,
 684   $$
 685   ÇÄÅ $s, t \in \AExp_\Sigma$.
 686 \end{proposition}
 687 \begin{proof}
 688 ïÞÅ×ÉÄÎÏ, ÓÌÅÄÕÅÔ ÉÚ ÏÐÒÅÄÅÌÅÎÉÊ (ÉÌÉ ÞÅÒÅÚ ÔÅÏÒÅÍÕ ëÌÉÎÉ).
 689 \end{proof}
 690
 691 ÷ Ó×ÑÚÉ Ó ÔÅÍÉ ÚÁÄÁÞÁÍÉ, ËÏÔÏÒÙÅ ÍÙ ÒÅÛÁÅÍ × ÜÔÏÊ çÌÁ×Å, ÎÁÓ ÂÕÄÕÔ
 692 ÉÎÔÅÒÅÓÏ×ÁÔØ Ó×ÏÂÏÄÎÙÅ ÍÏÄÅÌÉ × ËÌÁÓÓÁÈ $\Gamma | E$, ÇÄÅ $E \in
 693 \Equa$: ÉÓÔÉÎÎÏÓÔØ Horn\dÆÏÒÍÕÌÙ $E \implic s = t$ × $\Gamma$
 694 ÍÏÖÅÔ ÒÅÛÁÔØÓÑ ÐÏ ÉÓÔÉÎÎÏÓÔÉ ÒÁ×ÅÎÓÔ×Á $s = t$ × Ó×ÏÂÏÄÎÏÊ ÍÏÄÅÌÉ ×
 695 $\Gamma | E$.
 696
 697 \begin{theorem}
 698   \label{th:Cons-free}
 699   \cite{KA-complexity}.
 700   ðÕÓÔØ $\Emonoid \in \MoEqua_\Sigma$, $\mo M_0 = \mo M_0(\Sigma,
 701   \Emonoid)$.
 702   ôÏÇÄÁ
 703   $(\REG \mo M_0, R_{\mo M_0})$\T Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ × $\KAc | \Emonoid$.
 704 \end{theorem}
 705 \begin{proof}
 706   \sm \cite{KA-complexity}, ÐÏ ÏÂÝÉÍ ÓÏÏÂÒÁÖÅÎÉÑÍ õÎÉ×ÅÒÓÁÌØÎÏÊ
 707   ÁÌÇÅÂÒÙ ÓÌÅÄÕÅÔ ÉÚ ÔÏÇÏ, ÞÔÏ $\Reg_\Sigma$\T Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ × $\KAc$.
 708 \end{proof}
 709
 710 \begin{corollary}
 711   ðÕÓÔØ $\Ecomm \in \Comm_\Sigma$, $\mo M_0 = \mo M_0(\Sigma,
 712   \Ecomm)$.
 713   ôÏÇÄÁ
 714   $(\REG \mo M_0, R_{\mo M_0})$\T Ó×ÏÂÏÄÎÁÑ ÍÏÄÅÌØ × $\RKA | \Ecomm$.
 715 \end{corollary}
 716 \begin{proof}
 717     óÌÅÄÓÔ×ÉÅ õÔ×.~\ref{prop:Cons-Rel-iso} É ôÅÏÒÅÍÙ~\ref{th:Cons-free}.
 718 \end{proof}
 719
 720 îÁ ÓÌÕÞÁÊ $\KA|\Emonoid$ ÒÅÚÕÌØÔÁÔÙ ÄÌÑ $Reg_\Sigma$ ÎÅ ÐÅÒÅÎÏÓÑÔÓÑ:
 721 $(\REG \mo M_0, R_{\mo M_0})$ ÎÅ ÍÏÖÅÔ ÂÙÔØ Ó×ÏÂÏÄÎÏÊ ÍÏÄÅÌØÀ ÄÌÑ
 722 $\KA|\Emonoid$ ÐÏÔÏÍÕ, ÞÔÏ $\HOf_\MoEqua \KA$ É $\HOf_\MoEqua \KAc$
 723 ÏÔÌÉÞÁÀÔÓÑ, ËÁË ÜÔÏ ×ÉÄÎÏ ÉÚ ÐÒÉ×ÅÄ£ÎÎÙÈ × \cite{KA-complexity}
 724 ÒÅÚÕÌØÔÁÔÏ× Ï ÓÌÏÖÎÏÓÔÉ ÉÈ ÒÁÚÒÅÛÅÎÉÑ. ôÁÍ ÖÅ ×ÉÄÎÏ, ÞÔÏ ÓÉÔÕÁÃÉÑ ÓÏ
 725 ÓÌÏÖÎÏÓÔØÀ $\HOf_\Comm \KA$ ÎÅÑÓÎÁÑ.
 726
 727
 728 \subsubsection{òÁÚÒÅÛÉÍÙÅ É ÎÅÒÁÚÒÅÛÉÍÙÅ ÐÒÏÂÌÅÍÙ.}
 729
 730 éÚ \cite[Section 5.2]{partial-commut} ÕÓÔÁÎÁ×ÌÉ×ÁÅÔÓÑ
 731 %% \cite[Thm. 8.4]{Berstel-transductions} ÐÒÅÄÌÁÇÁÅÔ ÓÌÅÄÕÀÝÉÊ ÎÁÂÏÒ
 732 %% ÐÒÏÂÌÅÍ ÄÌÑ $\REG \mo M_0(\Sigma, \Ecomm)$, ÇÄÅ $\Ecomm \in \Comm$:
 733 %% \begin{definition}
 734 %%   ðÕÓÔØ $\mo M_0 = \mo M_0(\Sigma, \Ecomm)$, $\Indep =
 735 %%   \IndepBy{\Ecomm}$. $s$, $t$ ÐÒÉÎÉÍÁÀÔ ÚÎÁÞÅÎÉÑ ÉÚ $\RExp_\Sigma$.
 736 %%   \begin{description}
 737 %%   \item[ÐÅÒÅÓÅÞÅÎÉÑ] $\prINT(\Sigma, \Indep)$:
 738 %%     $R_{\mo M_0}(s) \cap R_{\mo M_0}(t) = \emptyset$
 739 %%   \item[×ËÌÀÞÅÎÉÑ]
 740 %%   \item[ÒÁ×ÅÎÓÔ×Á]
 741 %%   \item[ÕÎÉ×ÅÒÓÁÌØÎÏÓÔÉ]
 742 %%   \item[ÄÏÐÏÌÎÅÎÉÑ]
 743 %%   \item[(ÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÏÊ) ÒÁÓÐÏÚÎÁ×ÁÅÍÏÓÔÉ]
 744 %%     ÓÍ.~ïÐÒ.~\ref{def:det-REC}.
 745 %%   \end{description}
 746 %% \end{definition}
 747 %%   \todo{[]}
 748
 749 %% \begin{theorem}[Ï ÎÅÏÂÈÏÄÉÍÙÈ É ÄÏÓÔÁÔÏÞÎÙÈ ÕÓÌÏ×ÉÑÈ ÒÁÚÒÅÛÉÍÏÓÔÉ
 750 %%   \prINT]
 751 %%   \cite[Thm.~5.3]{partial-commut}, \cite{??SEE}
 752 %%   \todo{[]}
 753 %% \end{theorem}
 754
 755 %% \begin{theorem}[Ï ÎÅÏÂÈÏÄÉÍÙÈ ÕÓÌÏ×ÉÑÈ ÒÁÚÒÅÛÉÍÏÓÔÉ 6 ÐÒÏÂÌÅÍ]
 756 %%   \cite[Thm.~5.4]{partial-commut}
 757 %%   \todo{[]}
 758 %% \end{theorem}
 759 %% \begin{proof}
 760 %%   \todo{[ÉÄÅÑ?]}
 761 %% \end{proof}
 762
 763 %% \begin{theorem}[Ï ÄÏÓÔÁÔÏÞÎÙÈ ÕÓÌÏ×ÉÑÈ ÒÁÚÒÅÛÉÍÏÓÔÉ 5 ÐÒÏÂÌÅÍ]
 764 %%   \cite[Thm.~5.5]{partial-commut}
 765 %%   \todo{[]}
 766 %% \end{theorem}
 767 %% \begin{proof}
 768 %%   ïÐÉÒÁÅÔÓÑ ÎÁ ÎÅÒÁÚÒÅÛÉÍÏÓÔØ ÐÒÏÂÌÅÍÙ ÓÏÏÔ×ÅÔÓÔ×ÉÊ ðÏÓÔÁ. óÈÅÍÁ
 769 %%   ÄÏËÁÚÁÔÅÌØÓÔ× ÂÙÌÁ ÐÒÉÄÕÍÁÎÁ \cite{Ibarra-decision}.
 770 %% \end{proof}
 771
 772 \begin{corollary}[Ï ÎÅÏÂÈÏÄÉÍÙÈ É ÄÏÓÔÁÔÏÞÎÙÈ ÕÓÌÏ×ÉÑÈ ÒÁÚÒÅÛÉÍÏÓÔÉ
 773   $\HOf_{\Ecomm} \KAc$]
 774   ðÕÓÔØ $\Ecomm \in \Commut_\Sigma$.
 775   $\HOf_{\Ecomm} \KAc$ ÒÁÚÒÅÛÉÍÁ \IFF
 776   $\IndepBy{\Ecomm}$ ÔÒÁÎÚÉÔÉ×ÎÏ.
 777 \end{corollary}
 778 \begin{remark}
 779   ðÒÏÓÔÅÊÛÅÅ ÎÅÔÒÁÎÚÉÔÉ×ÎÏÅ $\IndepBy{E}$ ÓÏÏÔ×ÅÔÓÔ×ÕÅÔ $E =
 780   E_{\mword{2ta}}$ <<ÍÏÄÅÌÉ>> Ä×ÕÈ ÌÅÎÔ, ÓÍ.\ ðÒÉÍÅÒ~\ref{ex:2ta}.
 781 \end{remark}
 782
 783 \begin{corollary}[Cohen, \cite{KAT-commutativity}]
 784   \label{th:Hcommut-undec}
 785   $\HOf_\Commut \KAc$ ÎÅÒÁÚÒÅÛÉÍÁ.
 786 \end{corollary}
 787 ïÔÌÉÞÉÅ ÜÔÏÊ ÆÏÒÍÕÌÉÒÏ×ËÉ ÏÔ ÐÒÅÄÙÄÕÝÅÊ: ÚÄÅÓØ ÎÅ
 788 ÆÉËÓÉÒÏ×ÁÎÏ $\Ecomm$, Á ÏÎÏ ÔÏÖÅ ÐÏÄÁ£ÔÓÑ ÎÁ ×ÈÏÄ ÁÌÇÏÒÉÔÍÁ.
 789
 790 ðÏ Ó×ÅÄÅÎÉÑÍ \cite{KA-complexity} ÎÅÉÚ×ÅÓÔÎÏ, ÒÁÚÒÅÛÉÍÁ ÌÉ
 791 $\HOf_\Commut \KA$. ôÁËÖÅ $\HOf_\MoEqua \KA$ ÎÅÒÁÚÒÅÛÉÍÁ.
 792
 793 %% \todo{[åÝ£ ÉÚ \cite{KAT-commutativity}.]}
 794
 795 %% \todo{[ÓÌÏÖÎÏÓÔØ]}
 796
 797 \subsection{üÌÉÍÉÎÁÃÉÑ ÐÏÓÙÌÏË (ÄÏÐÕÝÅÎÉÊ)}
 798 \label{sec:elimination}
 799
 800 ÷ ÐÒÏÓÔÅÊÛÅÍ ÓÌÕÞÁÅ ÏÐÉÓÁÎÎÙÅ ÚÄÅÓØ ×ÅÝÉ ÐÒÅÄÌÏÖÅÎÙ
 801 \cite{Cohen-annihilating-annih}, ÒÁÚÒÁÂÏÔÁÎÙ ÄÁÌØÛÅ
 802 \cite{??}.
 803
 804 \begin{definition}\label{def:eliminiation}
 805   ëÌÁÓÓ ÁÌÇÅÂÒ $\class C$ \tING{ÄÏÐÕÓËÁÅÔ ÜÌÉÍÉÎÁÃÉÀ ÐÏÓÙÌÏË
 806   ÏÐÒÅÄÅÌ£ÎÎÏÇÏ ×ÉÄÁ~$\thclass c$ × Horn\dÆÏÒÍÕÌÁÈ}, ÅÓÌÉ ÄÌÑ ÌÀÂÏÊ
 807   Horn\dÆÏÒÍÕÌÙ ×ÉÄÁ
 808   $$
 809   \psi \implic s = t,
 810   \text{ ÇÄÅ $\{ \psi \} \in \thclass c$,}
 811   $$
 812   ÎÁÊÄ£ÔÓÑ ÜË×É×ÁÌÅÎÔÎÁÑ (ÏÔÎÏÓÉÔÅÌØÎÏ $\class C$) ÆÏÒÍÕÌÁ ×ÉÄÁ
 813   $$
 814   s' = t',
 815   $$
 816   \te ÔÁËÁÑ, ÞÔÏ
 817   $$
 818   \class C
 819   \models
 820   (\psi \implic s = t)
 821   \equivc
 822   (s' = t').
 823   $$
 824
 825   ëÌÁÓÓ ÁÌÇÅÂÒ $\class C$ \tING{ÄÏÐÕÓËÁÅÔ ÜÌÉÍÉÎÁÃÉÀ ÍÎÏÖÅÓÔ×Á ÐÏÓÙÌÏË}
 826   ÏÐÒÅÄÅÌ£ÎÎÏÇÏ ×ÉÄÁ~$\thclass c$ × Horn\dÆÏÒÍÕÌÁÈ, ÅÓÌÉ ÄÌÑ ÌÀÂÏÊ
 827   Horn\dÆÏÒÍÕÌÙ ×ÉÄÁ
 828   $$
 829   E \implic s = t,
 830   \text{ ÇÄÅ $E \in \thclass c$,}
 831   $$
 832   ÎÁÊÄ£ÔÓÑ ÜË×É×ÁÌÅÎÔÎÁÑ ÆÏÒÍÕÌÁ ×ÉÄÁ
 833   $$
 834   s' = t'.
 835   $$
 836
 837   ëÌÁÓÓ ÁÌÇÅÂÒ $\class C$ \tING{ÄÏÐÕÓËÁÅÔ ÎÅÚÁ×ÉÓÉÍÕÀ
 838     ÜÌÉÍÉÎÁÃÉÀ ÍÎÏÖÅÓÔ×Á ÐÏÓÙÌÏË}
 839   ÏÐÒÅÄÅÌ£ÎÎÏÇÏ ×ÉÄÁ~$\thclass c$ × Horn\dÆÏÒÍÕÌÁÈ, ÅÓÌÉ ÄÌÑ ÌÀÂÏÊ
 840   Horn\dÆÏÒÍÕÌÙ ×ÉÄÁ
 841   $$
 842   E_1 \wedge E_2 \implic s = t,
 843   \text{ ÇÄÅ $E_1 \in \thclass c$,}
 844   $$
 845   ÎÁÊÄ£ÔÓÑ ÜË×É×ÁÌÅÎÔÎÁÑ ÆÏÒÍÕÌÁ ×ÉÄÁ
 846   $$
 847   E_2 \implic s' = t'.
 848   $$
 849
 850   åÝ£ ÏÄÉÎ (ÎÁÉÂÏÌÅÅ ÏÂÝÉÊ) ÓÌÕÞÁÊ, ÂÌÉÚËÉÊ Ë ÐÏÓÌÅÄÎÅÍÕ,\T
 851   ×ÏÚÍÏÖÎÏÓÔØ ÎÅÚÁ×ÉÓÉÍÏÊ ÜÌÉÍÉÎÁÃÉÉ ÐÏÓÙÌÏË Ó ÉÚÍÅÎÅÎÉÅÍ ÔÅÒÍÏ× ×
 852   $E_2$ ÔÏÖÅ, \te ÐÒÉ×ÏÄÑÝÅÊ Ë ÆÏÒÍÕÌÅ ×ÉÄÁ
 853   $$
 854   E_2' \implic s' = t'.
 855   $$
 856 \end{definition}
 857 \begin{remark}
 858   îÁÓ, ËÏÎÅÞÎÏ, ÂÕÄÕÔ ÉÎÔÅÒÅÓÏ×ÁÔØ ×ÙÞÉÓÌÉÍÙÅ ÓÐÏÓÏÂÙ ÜÌÉÍÉÎÁÃÉÉ
 859   ÐÏÓÙÌÏË.
 860
 861   åÓÌÉ ÒÁÚÒÅÛÉÍÁ $\EOf \class C$ É $\class C$ ÄÏÐÕÓËÁÅÔ (×ÙÞÉÓÌÉÍÕÀ)
 862   ÜÌÉÍÉÎÁÃÉÀ
 863   ÍÎÏÖÅÓÔ×Á ÐÏÓÙÌÏË ×ÉÄÁ~$\thclass c$, ÔÏ ÒÁÚÒÅÛÉÍÁ $\HOf_{\thclass c}\class C$.
 864
 865   åÓÌÉ ÒÁÚÒÅÛÉÍÁ $\HOf_{\thclass c_2} \class C$ É $\class C$ ÄÏÐÕÓËÁÅÔ
 866   ÎÅÚÁ×ÉÓÉÍÕÀ ÜÌÉÍÉÎÁÃÉÀ
 867   ÍÎÏÖÅÓÔ×Á ÐÏÓÙÌÏË ×ÉÄÁ~$\thclass c_1$,
 868   ÔÏ ÒÁÚÒÅÛÉÍÁ $\HOf_{\thclass c_1 \oplus \thclass c_2}\class C$.
 869
 870   ôÏ ÖÅ ÓÁÍÏÅ ×ÅÒÎÏ É ÄÌÑ <<ÎÅÚÁ×ÉÓÉÍÏÊ ÜÌÉÍÉÎÁÃÉÉ, ÍÅÎÑÀÝÅÊ ÔÅÒÍÙ ×
 871   $E_2$>>,
 872   ÅÓÌÉ ËÌÁÓÓ ÔÅÏÒÉÊ~$\thclass c_2$ ÚÁÍËÎÕÔ ÏÔÎÏÓÉÔÅÌØÎÏ ÜÔÉÈ ÉÚÍÅÎÅÎÉÊ
 873   ÔÅÒÍÏ×.
 874   (îÁÐÒÉÍÅÒ, $\Equa$ ÚÁÍËÎÕÔ ÏÔÎÏÓÉÔÅÌØÎÏ ÌÀÂÙÈ ÉÚÍÅÎÅÎÉÊ ÔÅÒÍÏ×.)
 875 \end{remark}
 876 \begin{question}
 877   ðÒÉÍÅÒ ÎÅ×ÙÞÉÓÌÉÍÏÊ ÜÌÉÍÉÎÁÃÉÉ ÐÏÓÙÌÏË × Horn\dÆÏÒÍÕÌÁÈ.
 878 \end{question}
 879
 880 \subsubsection{îÅÚÁ×ÉÓÉÍÁÑ ÜÌÉÍÉÎÁÃÉÑ ÄÏÐÕÝÅÎÉÊ ×ÉÄÁ $r = 0$.}
 881 éÚ \cite{KA-modular-elimination}.
 882
 883 \todo{[×ÁÖÎÁ ÌÉ ÒÁÂÏÔÁ ÓÏ Ó×ÏÂÏÄÎÙÍÉ ÍÏÄÅÌÑÍÉ ÄÌÑ ÜÔÏÊ ÔÅÏÒÅÍÙ?]}
 884
 885 \begin{definition}[\cite{KA-modular-elimination}]
 886   õÎÉ×ÅÒÓÁÌØÎÏÅ ÒÅÇÕÌÑÒÎÏÅ ×ÙÒÁÖÅÎÉÅ $u_\Sigma$ ÎÁÄ~$\Sigma = \{ a_1, \dotsc, a_n
 887   \}$\T ÜÔÏ:
 888   $$
 889   u_\Sigma \eqdef (a_1 + \dotsb + a_n)^*.
 890   $$
 891 \end{definition}
 892 \begin{proposition}[\cite{KA-modular-elimination}]
 893   $\KA \models s \leq u_\Sigma$ ÄÌÑ ÌÀÂÏÇÏ $s \in \RExp_\Sigma$.
 894 \end{proposition}
 895
 896 \begin{theorem}[\cite{KA-modular-elimination}]
 897   \label{th:elim-annih}
 898   ðÕÓÔØ $r, s, t \in \RExp_\Sigma$, $E$\T ËÏÎÅÞÎÏÅ ÍÎÏÖÅÓÔ×Ï ÄÏÐÕÝÅÎÉÊ
 899   Ó ÂÁÚÏ×ÙÍÉ ÓÉÍ×ÏÌÁÍÉ ÉÚ $\Sigma$. ôÏÇÄÁ, ÅÓÌÉ $u$\T ÕÎÉ×ÅÒÓÁÌØÎÏÅ
 900   ÒÅÇÕÌÑÒÎÏÅ ×ÙÒÁÖÅÎÉÅ ÎÁÄ~$\Sigma$, ÔÏ
 901   \begin{align}
 902     \label{eq:elim-annih-KA}
 903     \KA \models E \wedge r = 0 \implic s = t
 904     &\iff
 905     \KA \models E \implic s + uru = t + uru\\
 906     \label{eq:elim-annih-KAc}
 907     \KAc \models E \wedge r = 0 \implic s = t
 908     &\iff
 909     \KAc \models E \implic s + uru = t + uru\\
 910     \label{eq:elim-annih-RKA}
 911     \RKA \models E \wedge r = 0 \implic s = t
 912     &\iff
 913     \RKA \models E \implic s + uru = t + uru
 914   \end{align}
 915 \end{theorem}
 916 \begin{remark}
 917   ôÁË ÞÔÏ:
 918   \begin{align*}
 919     \HOf_{\thclass c} \KA \text{ ÒÁÚÒÅÛÉÍÁ}
 920     &\implies
 921     \HOf_{\thclass c \oplus \Annih} \KA \text{ ÒÁÚÒÅÛÉÍÁ}\\
 922     \HOf_{\thclass c} \KAc \text{ ÒÁÚÒÅÛÉÍÁ}
 923     &\implies
 924     \HOf_{\thclass c \oplus \Annih} \KAc \text{ ÒÁÚÒÅÛÉÍÁ}\\
 925     \HOf_{\thclass c} \RKA \text{ ÒÁÚÒÅÛÉÍÁ}
 926     &\implies
 927     \HOf_{\thclass c \oplus \Annih} \RKA \text{ ÒÁÚÒÅÛÉÍÁ}
 928   \end{align*}
 929 \end{remark}
 930 óÐÒÁ×ÅÄÌÉ×ÏÓÔØ ÓÌÅÄÓÔ×ÉÊ
 931 × ÕÔ×ÅÒÖÄÅÎÉÉ ôÅÏÒÅÍÙ~\ref{th:elim-annih}
 932 × ÎÁÐÒÁ×ÌÅÎÉÉ ÓÐÒÁ×Á ÎÁÌÅ×Ï ÐÏËÁÚÙ×ÁÅÔÓÑ ÏÞÅÎØ ÐÒÏÓÔÏ.
 933 ÷ ÄÒÕÇÕÀ ÓÔÏÒÏÎÕ ÓÌÏÖÎÅÅ.
 934 õÔ×ÅÒÖÄÅÎÉÅ ÔÅÏÒÅÍÙ ÄÏËÁÚÙ×ÁÅÔÓÑ
 935 ×~\cite{KA-modular-elimination} ÏÔÄÅÌØÎÏ ÄÌÑ \KA É \KAc, ÏÔÄÅÌØÎÏ ÄÌÑ
 936 \RKA (× ÐÏÓÌÅÄÎÅÍ ÓÌÕÞÁÅ ÉÓÐÏÌØÚÕÅÔÓÑ \tNDNo{ÓÉÓÔÅÍÁ ÄÏËÁÚÁÔÅÌØÓÔ×}
 937 Horn\dÆÏÒÍÕÌ ÄÌÑ ÒÅÌÑÃÉÏÎÎÙÈ ÍÏÄÅÌÅÊ, ÒÁÚ×ÉÔÁÑ
 938 ×~\cite{KA-proof-theory} ×ÍÅÓÔÅ Ó ÓÉÓÔÅÍÏÊ ÄÏËÁÚÁÔÅÌØÓÔ× ÄÌÑ \KAc).
 939 \begin{question}
 940   ôÅÏÒÅÍÁ ×ÅÒÎÁ ÔÏÌØËÏ ÄÌÑ $E \in \Equa$ ÉÌÉ ÄÌÑ ÆÏÒÍÕÌ ÄÒÕÇÏÇÏ ×ÉÄÁ
 941   ÔÏÖÅ? (á ÄÌÑ ÆÏÒÍÕÌ ÑÚÙËÁ ÐÅÒ×ÏÇÏ ÐÏÒÑÄËÁ?)
 942 \end{question}
 943 \begin{remark}[\cite{KA-modular-elimination}]
 944   óÌÕÞÁÊ, ËÏÇÄÁ $E = \emptyset$, ÏÓÏÂÙÊ. ÷×ÉÄÕ ÓÏ×ÐÁÄÅÎÉÑ $\EOf \KA$,
 945   $\EOf \KAc$, $\EOf \RKA$ (ôÅÏÒÅÍÁ~\ref{th:EKA-coincide}) ÕÔ×ÅÒÖÄÅÎÉÅ
 946   ôÅÏÒÅÍÙ ÐÒÉÏÂÒÅÔÁÅÔ ÐÒÏÓÔÏÊ ×ÉÄ:
 947
 948   óÌÅÄÕÀÝÉÅ ÞÅÔÙÒÅ ÕÔ×ÅÒÖÄÅÎÉÑ ÜË×É×ÁÌÅÎÔÎÙ:
 949   \begin{align*}
 950     \KA &\models r = 0 \implic s = t\\
 951     \KAc &\models r = 0 \implic s = t\\
 952     \RKA &\models r = 0 \implic s = t\\
 953     \KA &\models s + uru = t + uru.
 954   \end{align*}
 955
 956   äÏËÁÚÁÔÅÌØÓÔ×Ï ÔÁËÏÇÏ ÕÔ×ÅÒÖÄÅÎÉÑ ÐÒÏÝÅ:
 957   \cite{KAT-complete-decidable,Cohen-annihilating-annih}.
 958   ëÒÏÍÅ ÔÏÇÏ, ÚÁÍÅÔÉÍ, ÞÔÏ
 959   ÎÅÓËÏÌØËÏ ÐÏÓÙÌÏË ÔÁËÏÇÏ ×ÉÄÁ $r_1 = 0, \dotsc, r_k = 0$ ÍÏÖÎÏ
 960   ÚÁÍÅÎÉÔØ ÎÁ ÏÄÎÕ $r_1 + \dotsb + r_k = 0$. ðÏÜÔÏÍÕ × ÐÒÉ×ÅÄ£ÎÎÏÍ
 961   ÕÐÒÏÝ£ÎÎÏÍ ÕÔ×ÅÒÖÄÅÎÉÉ ÍÏÖÎÏ ÇÏ×ÏÒÉÔØ ÏÂ ÜÌÉÍÉÎÁÃÉÉ
 962   \emph{ÎÅÓËÏÌØËÉÈ} ÔÁËÏÇÏ ×ÉÄÁ.
 963
 964   ÷ ÉÔÏÇÅ ÐÒÉÈÏÄÉÍ Ë ×Ù×ÏÄÕ Ï ÔÏÍ, ÞÔÏ
 965   ÔÅÏÒÉÉ $\HOf_\Annih \KA$, $\HOf_\Annih \KAc$,
 966   $\HOf_\Annih \RKA$ ÓÏ×ÐÁÄÁÀÔ,
 967   ËÁË É ÜË×ÁÃÉÏÎÁÌØÎÙÅ ÔÅÏÒÉÉ ÜÔÉÈ ËÌÁÓÓÏ×, É ÏÎÉ ÒÁÚÒÅÛÉÍÙ (ôÅÏÒÅÍÁ~\ref{th:EKA-decidable}).
 968 \end{remark}
 969
 970
 971
 972 %% \subsection{éÔÏÇÏ×ÙÅ ÏÔ×ÅÔÙ}
 973 %% \label{sec:hypo-plain-all-answers}
 974
 975 %% ïÂÝÉÅ
 976
 977 %% commut.
 978
 979 %% \begin{table}[htbp]
 980 %%   \centering
 981 %%   \begin{tabular}{l|c|c|c|}
 982 %%     $\thclass c$ &
 983 %%     $\HOf_{\thclass c}\KA$ & $\HOf_{\thclass c}\KAc$ & $\HOf_{\thclass c}\RKA$ \\
 984 %%     \hline\hline
 985 %%     \Equa & \\
 986 %%     \MoEqua & \\
 987 %%     \ConsEqua & \\
 988 %%     \Commut &\\
 989 %%     $\thclass c' \oplus \Annih$ & \\
 990 %%     \Annih & \\
 991 %%     $\{ \emptyset \}$ &
 992 %%     \multicolumn{3}{|c|}\PSPACE\d{}complete
 993 %%   \end{tabular}
 994 %%   \caption{ïÔ×ÅÔÙ}
 995 %%   \label{tab:hypo-plain-answ}
 996 %% \end{table}
 997
 998 %% \begin{description}
 999 %% \item[$\emptyset$] $\EOf\KA = \EOf\KAc = \EOf\RKA$
1000 %%   (òÁÚÄÅÌ~\ref{sec:free-plain-ndet});
1001 %% \end{description}
1002
1003 \subsection{ðÒÏÞÅÅ}
1004 \label{sec:hypo-plain-misc}
1005
1006
1007 \paragraph{ðÒÅÄÓÔÁ×ÌÅÎÉÅ \KAT, ÐÅÒÅÈÏÄ ÏÔ \KAT Ë \KA.}
1008 \newcommand*{\BoolAx}{\metaconstSynt{BoolAx}}
1009 \KAT Ñ×ÌÑÅÔÓÑ \KA, ÐÒÉ ÜÔÏÍ
1010 ÐÏÄÓÔÒÕËÔÕÒÁ ÔÅÓÔÏ× ÄÏÌÖÎÁ ÕÄÏ×ÌÅÔ×ÏÒÑÔØ ÄÏÐÏÌÎÉÔÅÌØÎÙÍ ÕÓÌÏ×ÉÑÍ
1011 (ÁËÓÉÏÍÁÍ \tND{ÂÕÌÅ×ÏÊ ÁÌÇÅÂÒÙ}{def:boolean-algebra}) É × ÎÅÊ ÅÓÔØ
1012 ÄÏÐÏÌÎÉÔÅÌØÎÁÑ ÏÐÅÒÁÃÉÑ ($\nP$). íÙ ÍÏÖÅÍ <<ÐÒÏÍÏÄÅÌÉÒÏ×ÁÔØ>> ÜÔÏ
1013 ÐÏÓÙÌËÁÍÉ × ÆÏÒÍÕÌÁÈ, ÉÓÔÉÎÎÏÓÔØ ËÏÔÏÒÙÈ ÍÙ ÂÕÄÅÍ ÐÒÏ×ÅÒÑÔØ
1014 ÏÔÎÏÓÉÔÅÌØÎÏ \KA.
1015
1016 íÏÖÎÏ ÌÉ ÜÔÏ ÓÄÅÌÁÔØ? (äÌÑ ÆÉËÓÉÒÏ×ÁÎÎÏÇÏ ÁÌÆÁ×ÉÔÁ ÂÁÚÏ×ÙÈ ÔÅÓÔÏ×~$T$ ×
1017 Ó×ÏÂÏÄÎÏÊ ÂÕÌÅ×ÏÊ ÁÌÇÅÂÒÅ, ÐÏÒÏÖÄ£ÎÎÏÊ $T$, ËÏÎÅÞÎÏÅ ÞÉÓÌÏ ÜÌÅÍÅÎÔÏ×,
1018 ($3^T$).) åÓÔØ ÌÉ ËÏÎÅÞÎÁÑ ÐÏÌÎÁÑ ÓÉÓÔÅÍÁ ÜË×É×ÁÌÅÎÔÎÙÈ ÐÒÅÏÂÒÁÚÏ×ÁÎÉÊ
1019 ÔÅÒÍÏ× ÎÁÄ~$T$ (ÚÁÐÉÓÁÎÎÁÑ × ×ÉÄÅ ÒÁ×ÅÎÓÔ× ÔÅÒÍÏ× Ó ÂÁÚÏ×ÙÍÉ ÓÉÍ×ÏÌÁÍÉ
1020 ÉÚ $T$), ÒÁÂÏÔÁÀÝÁÑ × ÐÒÉÓÕÔÓÔ×ÉÉ ÁËÓÉÏÍ \KA. \todo{[×ÙÑÓÎÉÔØ. þÔÏ, ÎÁÐÒÉÍÅÒ,
1021   ÇÏ×ÏÒÉÔ \cite{OK}?]}
1022
1023 äÏÐÏÌÎÉÔÅÌØÎÙÅ ÕÓÌÏ×ÉÑ ÏÂÏÚÎÁÞÉÍ $\BoolAx(T)$ (ÐÏËÁ ÍÙ ÎÅ
1024 ×ÄÁ£ÍÓÑ × ÐÏÄÒÏÂÎÏÓÔÉ, ËÁË ÏÎÉ ×ÙÇÌÑÄÑÔ).
1025 ïÔÒÉÃÁÎÉÑ ÂÁÚÏ×ÙÈ ÔÅÓÔÏ× ÍÙ ÏÂÏÚÎÁÞÉÍ ÎÏ×ÙÍÉ ÓÉÍ×ÏÌÁÍÉ. ðÒÉ
1026 ÐÅÒÅ×ÏÄÅ × ÆÏÒÍÕÌÁÈ ÂÕÄÅÍ ÏÐÕÓËÁÔØ ÏÔÒÉÃÁÎÉÑ ÄÏ ÕÒÏ×ÎÑ ÂÁÚÏ×ÙÈ
1027 ÔÅÓÔÏ×. ôÁË ÞÔÏ ÂÕÄÅÔ ×ÅÒÎÏ:
1028 $$
1029 \KAT \models \phi
1030 \iff
1031 \KA \models \BoolAx(T) \implic \phi'
1032 $$
1033
1034 ôÁËÉÍ ÏÂÒÁÚÏÍ, ÎÁÐÒÉÍÅÒ, $\HOf_{\thclass c}(\KAT)$, ÏÇÒÁÎÉÞÅÎÎÁÑ
1035 ÆÏÒÍÕÌÁÍÉ Ó ÂÁÚÏ×ÙÍÉ ÓÉÍ×ÏÌÁÍÉ ÉÚ $\Sigma$, $T$, ÓÏÏÔ×ÅÔÓÔ×ÕÅÔ
1036 $\HOf_{\thclass c \oplus \{ \BoolAx(T) \} }(\KA)$. þÔÏ ÅÓÌÉ ÐÏÓÙÌËÉ
1037 ÔÏÇÏ ×ÉÄÁ, ËÏÔÏÒÏÇÏ ÕÓÌÏ×ÉÑ × $\BoolAx(T)$, ÍÙ ÓÍÏÖÅÍ ÜÌÉÍÉÎÉÒÏ×ÁÔØ?
1038
1039 ÷ÏÏÂÝÅ-ÔÏ, ÎÅÚÁ×ÉÓÉÍÏ ÏÔ ÜÔÏÇÏ, ÉÚ×ÅÓÔÎÏ~\cite{AGS} (ÓÍ.\
1040 õÔ×.~\ref{prop:G-to-R}), ÞÔÏ ÅÓÔØ ÔÁËÏÊ
1041 ÐÅÒÅ×ÏÄ $\Hat{\place}\colon \RExp_{\Sigma,T} \to \RExp_{\Sigma}$, ÞÔÏ
1042 $$
1043 \KAT \models s = t
1044 \iff
1045 \KA \models \Hat s = \Hat t.
1046 $$
1047 (\todo{<<ðÅÒÅ×ÏÄ ÓÈÅÍ ñÎÏ×Á × ËÏÎÅÞÎÙÅ Á×ÔÏÍÁÔÙ>>}.)
1048 üÔÏ
1049 ÓÏÏÔ×ÅÔÓÔ×ÉÅ ÍÅÖÄÕ $\EOf \KAT$ É $\EOf \KA$
1050 ÍÏÖÅÔ ÂÙÔØ Ó×ÉÄÅÔÅÌØÓÔ×ÏÍ ÔÏÇÏ, ÞÔÏ ÐÏÓÙÌËÉ ×ÉÄÁ~$\BoolAx(T)$ ÍÙ
1051 ÍÏÖÅÍ ÜÌÉÍÉÎÉÒÏ×ÁÔØ.
1052
1053 ôÁËÖÅ, ÁÎÁÌÏÇÉÞÎÏÅ ÓÏÏÔ×ÅÔÓÔ×ÉÅ ÅÓÔØ ÍÅÖÄÕ \KAT É \KA × ÏÄÎÏÍ ËÌÁÓÓÅ
1054 Horn\dÆÏÒÍÕÌ: ÍÙ ÍÏÖÅÍ ÍÏÄÅÌÉÒÏ×ÁÔØ ÜË×É×ÁÌÅÎÔÎÏÓÔØ
1055 \tD{ÎÅÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ ÍÎÏÇÏÌÅÎÔÏÞÎÙÈ Á×ÔÏÍÁÔÏ×}{def:nmta} (NMTA),
1056 Ó ÏÄÎÏÊ ÓÔÏÒÏÎÙ,
1057 Horn\dÆÏÒÍÕÌÁÍÉ ÏÄÎÏÇÏ ×ÉÄÁ × \KA,
1058 É, Ó ÄÒÕÇÏÊ ÓÔÏÒÏÎÙ, Horn\dÆÏÒÍÕÌÁÍÉ ÄÒÕÇÏÇÏ ×ÉÄÁ ×
1059 \KAT (ÓÍ.\ ðÒÉÍÅÒ~\ref{ex:nmta-KA-KAT}).
1060 üÔÏ
1061 ÓÏÏÔ×ÅÔÓÔ×ÉÅ ÍÅÖÄÕ $\HOf_{\thclass c_1}\KAT$ É $\HOf_{\thclass
1062   c_2}\KA$, ÇÄÅ ${\thclass c_1}$ É ${\thclass c_2}$ ÓÏÏÔ×ÅÔÓÔ×ÕÀÔ
1063 ÒÁÚÎÙÍ ÓÐÏÓÏÂÁÍ ÍÏÄÅÌÉÒÏ×ÁÔØ NMTA,
1064 ÍÏÖÅÔ ÂÙÔØ ËÏÓ×ÅÎÎÙÍ
1065 Ó×ÉÄÅÔÅÌØÓÔ×ÏÍ ×ÏÚÍÏÖÎÏÓÔÉ ÜÌÉÍÉÎÉÒÏ×ÁÔØ ÐÏÓÙÌËÉ ×ÉÄÁ~$\BoolAx(T)$ ×
1066 ÐÒÉÓÕÔÓÔ×ÉÉ ÄÒÕÇÉÈ ÐÏÓÙÌÏË, ÉÚÍÅÎÑÑ ÄÒÕÇÉÅ ÐÏÓÙÌËÉ (ÎÅËÏÔÏÒÙÍ ÎÅ ÏÞÅÎØ
1067 ÔÒÉ×ÉÁÌØÎÙÍ ÓÐÏÓÏÂÏÍ).
1068
1069 \begin{question}
1070   ëÁË Ó×ÑÚÁÎÙ ÏÐÉÓÁÎÎÙÅ ×ÏÚÍÏÖÎÏÓÔÉ ÐÅÒÅÈÏÄÁ ÏÔ ÔÅÏÒÉÊ $\KAT$ Ë
1071   ÔÅÏÒÉÑÍ $\KA$ Ó ×ÏÚÍÏÖÎÏÓÔØÀ ÜÌÉÍÉÎÉÒÏ×ÁÔØ × Horn\dÆÏÒÍÕÌÁÈ ÐÏÓÙÌËÉ
1072   ×ÉÄÁ~$\BoolAx(T)$? äÏÂÁ×ÌÑÅÔ ÌÉ ×ÏÚÍÏÖÎÏÓÔØ ÔÁËÏÊ ÜÌÉÍÉÎÁÃÉÉ ÞÔÏ-ÔÏ
1073   ÎÏ×ÏÅ Ë ÉÚ×ÅÓÔÎÙÍ ÓÌÕÞÁÑÍ, ËÏÇÄÁ ÜÌÉÍÉÎÁÃÉÑ ÄÏÐÕÓÔÉÍÁ \cite{?,?,?}?
1074 \end{question}
1075
1076 \subparagraph{ï ×ÉÄÅ $\BoolAx(T)$.}
1077 \begin{question}
1078   ëÁËÉÅ ×ÏÚÍÏÖÎÙ ×ÉÄÙ ÄÌÑ $\BoolAx(T)$?
1079   ëÁË ÏÎÉ Ó×ÑÚÁÎÙ Ó ÉÚ×ÅÓÔÎÙÍÉ ÓÌÕÞÁÑÍÉ ÄÏÐÕÓÔÉÍÏÊ ÜÌÉÍÉÎÁÃÉÉ ÐÏÓÙÌÏË
1080   × Horn\dÆÏÒÍÕÌÁÈ?
1081 \end{question}
1082 \begin{answer}
1083
1084 \cite[Section~2.5]{KA-modular-elimination} ÏÐÉÓÙ×ÁÅÔÓÑ ÓÏÏÔ×ÅÔÓÔ×ÉÅ
1085 ÍÅÖÄÕ $\HOf \RKA$ É $\HOf \RKAT$. ôÁÍ È×ÁÔÉÌÏ ÚÁÐÉÓÉ × ÐÏÓÙÌËÉ ÁËÓÉÏÍ
1086 ×ÉÄÁ
1087 \begin{align}
1088   \label{eq:boolax-compl}
1089   p + \n{p} &= 1
1090   &&\text{(ÄÏÐÏÌÎÉÔÅÌØÎÏÓÔØ)}
1091   \\
1092   \label{eq:boolax-annih}
1093   p \cdot \n{p} &= 0.
1094   &&\text{(ÁÎÎÉÇÉÌÑÃÉÑ)}
1095 \end{align}
1096 ðÒÏ ÐÏÓÙÌËÉ ÏÄÎÏÇÏ ÉÚ ÜÔÉÈ ×ÉÄÏ×\T ×ÉÄÁ~\eqref{eq:boolax-annih}\T
1097 ÉÚ×ÅÓÔÎÏ, ÞÔÏ ÉÈ  ÍÏÖÎÏ
1098 ÜÌÉÍÉÎÉÒÏ×ÁÔØ ÎÅÚÁ×ÉÓÉÍÏ (ÐÏËÁÚÁÎÏ ÔÁÍ ÖÅ
1099 \cite{KA-modular-elimination}).
1100 þÔÏ ÍÏÖÎÏ ÓËÁÚÁÔØ ×ÏÏÂÝÅ ÏÂ ÜÌÉÍÉÎÁÃÉÉ ÐÏÓÙÌÏË
1101 ×ÉÄÁ~\eqref{eq:boolax-compl}\T $a + b = 1$?
1102
1103 ÷ÏÚÍÏÖÎÏ ÌÉ ×ÚÑÔØ ÄÒÕÇÉÅ ÕÓÌÏ×ÉÑ × ËÁÞÅÓÔ×Å ÄÏÐÏÌÎÉÔÅÌØÎÏ ÔÒÅÂÕÀÝÉÈÓÑ
1104 ÁËÓÉÏÍ ÂÕÌÅ×ÏÊ ÁÌÇÅÂÒÙ × ÐÏÓÙÌËÁÈ? îÁÐÒÉÍÅÒ, ÚÁÍÅÎÉÔØ
1105 \eqref{eq:boolax-compl} ÎÁ
1106 \begin{align}
1107   \label{eq:boolax-idemp}
1108   pp &= p
1109   &&\text{(ÉÄÅÍÐÏÔÅÎÔÎÏÓÔØ)}
1110   \\
1111   \label{eq:boolax-commut}
1112   pq &= qp.
1113   &&\text{(ËÏÍÍÕÔÁÔÉ×ÎÏÓÔØ)}
1114 \end{align}
1115 ðÏÓÙÌËÉ ×ÉÄÁ \eqref{eq:boolax-commut} ×ÙÚÙ×ÁÀÔ ÎÅÒÁÚÒÅÛÉÍÏÓÔØ
1116 Horn\dÔÅÏÒÉÊ (ÓÍ.~ôÅÏÒÅÍÕ.~\ref{th:Hcommut-undec}, \ref{?}).
1117 ðÏÈÏÖÅ ÌÉ~\eqref{eq:boolax-idemp} ÎÁ ÓÌÕÞÁÊ ÐÏÓÙÌÏË ×ÉÄÁ $pa = p$,
1118 ËÏÔÏÒÙÅ ÍÏÖÎÏ ÜÌÉÍÉÎÉÒÏ×ÁÔØ <<ÐÏÞÔÉ>> ÎÅÚÁ×ÉÓÉÍÏ
1119 \cite{KA-modular-elimination}?
1120 \end{answer}
1121
1122 \begin{example}[2\dÈÌÅÎÔÏÞÎÙÅ Á×ÔÏÍÁÔÙ]
1123   \label{ex:nmta-KA-KAT}
1124   îÁ ÐÅÒ×ÏÊ ÌÅÎÔÅ Ä×ÕÈÂÕË×ÅÎÎÙÊ ÁÌÆÁ×ÉÔ, ÎÁ ×ÔÏÒÏÊ\T ÏÄÎÏÂÕË×ÅÎÎÙÊ.
1125
1126   \subparagraph{÷ $\HornOf\RKA$.} \todo{[REL, cont?]}
1127   $\Sigma = \{ a_1, b_1, a_2 \}$. íÎÏÖÅÓÔ×Ï ÐÏÓÙÌÏË $E$\T ÕÓÌÏ×ÉÑ ËÏÍÍÕÔÁÔÉ×ÎÏÓÔÉ:
1128   \begin{align*}
1129     a_1 a_2 &= a_2 a_1
1130     &
1131     b_1 a_2 &= a_2 b_1.
1132   \end{align*}
1133   ðÏ×ÅÒÑÅÍ
1134   $$
1135   \RKA \models E \implic s = t.
1136   $$
1137   \todo{[éÌÉ ÐÏÄËÌÁÓÓ?]}
1138   òÁÚÒÅÛÉÍÏÓÔØ ÐÒÏÂÌÅÍÙ ÜË×-ÔÉ ÎÅÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ 2\dÈÌÅÎÔÏÞÎÙÈ
1139   Á×ÔÏÍÁÔÏ×\T
1140   ÒÁÚÒÅÛÉÍÏÓÔØ $\HOf_{\{ E \}} \RKA$.
1141
1142   \subparagraph{÷ $\HornOf\RKAT$.} \todo{[REL, cont?]}
1143   $\Sigma = \{ c_1, c_2 \}, T = \{ p \}$.
1144   íÎÏÖÅÓÔ×Ï ÐÏÓÙÌÏË $E'$\T ÕÓÌÏ×ÉÑ ËÏÍÍÕÔÁÔÉ×ÎÏÓÔÉ É ÓÄ×ÉÇÏ×:
1145   \begin{align*}
1146     c_1 c_2 &= c_2 c_1
1147     &
1148     p c_2 \n{p} &= 0\\
1149     &&
1150     \n{p} c_2 p &= 0.
1151   \end{align*}
1152   ðÕÓÔØ $s' = \Expl(s), t' = \Expl(t)$.
1153   ðÏ×ÅÒÑÅÍ
1154   $$
1155   \RKAT \models E' \implic s' = t'.
1156   $$
1157 %  \todo{[éÌÉ ÄÒ. ÐÏÄËÌÁÓÓ?]}
1158   òÁÚÒÅÛÉÍÏÓÔØ ÐÒÏÂÌÅÍÙ ÜË×-ÔÉ ÎÅÄÅÔÅÒÍÉÎÉÒÏ×ÁÎÎÙÈ 2\dÈÌÅÎÔÏÞÎÙÈ
1159   Á×ÔÏÍÁÔÏ×\T
1160   ÒÁÚÒÅÛÉÍÏÓÔØ $\HOf_{\{ E' \}} \RKAT$.
1161
1162   äÌÑ Â\`ÏÌØÛÉÈ ÁÌÆÁ×ÉÔÏ× É Â\`ÏÌØÛÅÇÏ ËÏÌÉÞÅÓÔ×Á ÌÅÎÔ
1163   ÂÕÄÕÔ ÁÎÁÌÏÇÉÞÎÙÅ ÕÓÌÏ×ÉÑ.
1164 \end{example}
1165
1166 %%% Local Variables:
1167 %%% mode: latex
1168 %%% TeX-master: "main"
1169 %%% End: