\input style
\chapter{5 ��� �������}
� ���� ����� �� ������� ��� ������� �� ����������, ������� �������� 
�� ������� ���������� ������. ��� ������� �������� ����������� 
������ if-fi, � ������ --- ����������� ���������� do-od. � ���� ����� 
�� ����� ������������� �����������, ��������� �� ������ ���������� 
������
$$ 
B_1\to SL_1\wbox B_2\to SL_2  \wbox\ldots \wbox B_n\to 
SL_n 
$$

ᓄ�� ���������� ����� "IF" � "DO" ���������, ���������� 
����������� ����� ������ ���������� ������ � ���� ������ "if ... 
fi" � "do ... od" ��������������. � ����� ����� ������������ 
����������
$$ 
BB=(\exists j: 1\le j \le n: B_j) 
$$

򅎐���. (����� ������� ��� ����������� ������) 

葏������ ��������� ������ ��� �����������, �� ����� �������������� 
�������� ������� ��� ����������� ������: 

�� ����������� ������ IF � ���� ���������� $Q$ � $R$ ������, ��� 
$$ 
Q \Rightarrow BB  \eqno (1) 
$$ 
�
$$ (\forall j : 1\le j \le n : (Q \and B_j) \Rightarrow \wp (SL_j, R) )           
\eqno(2) 
$$ 
������������ ����������� ��� ���� ���������. 򎃄�
$$ 
Q \Rightarrow \wp(IF, R) \eqno (3) 
$$
����������� ����� ��� ���� ���������. ������, � ���� 
�����������,
$$ 
\wp(IF, R) = BB \and (\forall j: 1\le j \le n: 
B_j \Rightarrow \wp(SL_j,R)) 
$$
�, �������� (1), �� $Q$ ��������� ������� ������ ���� ������ �����, 
�� ��������� (3) ������������, ���� �� ��������� (2) �� ����� 
������� �����, ��� 
$$ 
Q \Rightarrow (\forall j: 1\le j \le n: B_j \Rightarrow \wp(SL_j,R)) \eqno(4)
$$
����������� ��� ���� ���������. 䋟 ������ ���������, ���
������� $Q$ �������� �����, ��������� (4) ������� � ���� 
����������� ����������� ����������. 䋟 ������ ���������, ��� 
������� $Q$ �������� �������, � ��� ������ �������� $j$ �� ����� 
��������� ��� ������: ���� $B_j$ �������� �����, �� ����� 
$B_j \Rightarrow \wp(SL_j, R)$ �������� ������� � ���� ����������� 
����������, ���� $B_j$ �������� �������, �� �����, �������� (2), 
$\wp(SL_j,R)$ �������� �������, � �������������, 
$B_j \Rightarrow \wp(SL_j,R)$ ���� �������� �������. � ���������� �� 
�������� ��������� (4), � �������������, � (3).

{\sl 瀌������.} � ������� ������ ��������� ������ ($n=2$) � ��� 
$B_2=\non B_1$ �� ����� $BB=T$, � ��������� ����������� 
������������� ���:
$$
\eqalign{ 
(B_1 \Rightarrow \wp(SL_1, R) ) \and (\non B_1 \Rightarrow \wp(SL_2, R)) &=\cr 
(\non B_1 \or \wp (SL_1, R) ) \and (B_1 \or \wp (SL_2, R) ) &=\cr 
(B_1 \and \wp (SL_1, R) ) \or (\non B_1 \and \wp (SL_2, R) )&\cr    
}
\eqno(5) 
$$
������ �������������� �������� ������, ��� �� ������� 
������������ ������������ ���� $B_1 \and \non B_1=F$ ����� ���� 
��������, � ���� $\wp(SL_1, R) \and \wp(SL_2, R)$ ���� ����� 
���� �������� �� ��������� �������: � ����� ���������, ��� �� 
�������, ����������� �������� ������� �����-�� ���� �� ���� ������ 
������� (5), � ������� ��� ������ ����� ��������� �� ����������. 
􎐌��� (5) ����� ������ ��������� � ������������� ������ ������� 
�������� ��������� ����������� \kwd{if}-\kwd{then}-\kwd{else} �� 
����� ����� 60. ������ ����� $BB=T$ ��������� ������� �� ���� 
������, �� ����� ������� (3) ��� ����� ������ �������������:
$$ 
((Q \and B_1) \Rightarrow \wp(SL_1,R)) \and ((Q \and \non 
B_1) \Rightarrow \wp(SL_2, R)) 
$$
{\sl (ꎍ�� ���������.)}

򅎐��a ��� ����������� ������ ������������ ������ �������� � 
������, ����� ���� ���������� $Q$ � $R$ ����� ���� �������� � ���� 
$$ 
\eqalign{
R&=P \cr 
Q&=P \and BB \cr 
}
$$
� ���� ������ ����������� (1) ����������� �������������, � 
��������� $(BB \and B_j) = B_j$, ����������� (2) �������� � 
����
$$ 
(\forall j: 1\le j\le n: (P \and B_j) \Rightarrow \wp(SL_j, P)) \eqno (6) 
$$
�� ���� �� ����� �������, �������� (3), 
$$ 
(P \and BB) \Rightarrow \wp(IF, P) \qquad\hbox{ ��� ���� ��������� } \eqno (7) 
$$

��� ��������� �������� ������������ ��� ����� ��������� �������.

{\bf 򅎐���.} (����� ������� ��� ����������� �������������.) 

�� ����� ���������� ������ � ����������� ��� ���� ������������ 
������ IF � �������� $P$  ������, ���
$$ 
(P \and BB) \Rightarrow \wp(IF, P) \eqno(7) 
$$
����������� ��� ���� ���������. 򎃄� ��� ��������������� 
����������� ���������� DO ����� �������, ���
$$ 
(P \and \wp (DO, �) ) \Rightarrow \wp (DO, P \and \non BB) \eqno(8) 
$$
��� ���� ���������.

��� �������, ������� �������� ����� ��� ��������� "��������  
������� �������������� ��� ������", �� ����������� ������ �� ������ 
������. �������� (7) ������� ���, ��� ���� �������� $P$ 
������������� ������� � ���� �� ���������� ������ ���������� ��� 
����������, �� ����� �� ���������� $P$ �������� ���� ����������. 
荀�� ������, �������������� �����������, ��� ���������� 
��������������� ������� ���������� �� ������� ���������� $P$, ���� 
��������� �������� $P$ ���� ��������. 񋅄���������, ��� 
����������� �� ����, ��� ����� ������������ ������� ���������� 
������� �� ���������� ������, �������� $P$ ����� ���������� ��� 
����� ����� �������� ���������������. �� ���������� ���� 
�����������  ����������, ����� �� ���� �� ��������������� �� 
��������  �������, �� ��� ����� �������� ������ � �������� 
���������, ��������������� $P \and \non BB$. ⎏��� � ���, 
���������� �� ������ ���������. �, ���� ������� $\wp(DO, T)$ 
����������� � �������; ��������� ����� ��������� ������������� $T$, 
�� $\wp(DO, T)$ �� ����������� �������� ��������� ������������ ��� 
���������� ���������, ������, ��� ������ ��������� DO �������� � 
��������� ����������� ������.

􎐌������ �������������� �������� ������� ��� ����������� 
���������� ������������ �� ���������� �������� ��������� ���� 
����������� (��. ���������� �����), �� �������� �� �������
$$ 
\eqalignno{
H_0(T)&=\non BB & (9) \cr 
\hbox{��� $k>0$}: H_k(T)&=\wp(IF,H_{k-1}(T)) \or \non BB & (10)\cr 
H_0(P \and \non BB)&=P \and \non BB &(11)\cr 
\hbox{��� $k>0$}: H_k(P \and \non BB)&=\wp(IF,H_{k-1} (P \and \non 
BB)) \or P \and \non BB &(12)\cr 
}
$$

퀗��� � ����, ��� ������� ����������� �������������� ��������, 
��� ����������� (7) ����������� ��������������
$$
 (P \and H_k(T)) \Rightarrow H_k(P \and \non BB) \eqno  (13) 
$$
��� ���� ���������.

� ���� ��������� (9) � (11) ��������� (13) ����������� ��� $k=0$. 
� �������, ��� ��������� (13) ����� ���� �������� ��� 
$k=K\;(K>0)$ �� ��������� �������������, ��� (13) ����������� ��� 
$k=K-1$.
$$ 
\eqalign{ 
P \and H_k(�)&=� \and \wp(IF, �_{K-1}�)) \or P \and \non 
BB\cr &=P \and BB \and \wp(IF, H_{K-1}(T)) \or P \and \non BB\cr 
& \Rightarrow \wp(IF, P) and wp(IF, H_{K-1}(T)) \or P \and \non BB\cr 
&=\wp(IF, P) and H_{K-1}(T)) or P and non BB\cr
& \Rightarrow wp(IF, H_{K-1} (P and non BB)) or P and non BB\cr 
&=H_K (P and non BB)\cr 
} 
$$
��������� � ������ ������ ������� �� (10), ��������� �� ������ 
������ ������� �� ����, ��� ������ $\wp(IF, R) \Rightarrow BB$, ���������� 
���������� � ������� ������ �������� �� (7), ��������� � 
��������� ������ ������������ �� �������� 3 ���������������� 
����������, ���������� � ����� ������ �������� �� �������� 2 
���������������� ���������� � �� ������������  ������������� (13) 
��� $k=K-1$, � ��������� ������ ������� �� (12). 蒀�, �� 
�������� (13) ��� $k=K$, � �������������, ��� ���� �������� $k 
\ge 0$. 

퀊����, ��� ����� ����� � ������������ ��������� �� �����, � 
���� (13),
$$ 
\eqalign{ 
P \and \wp(DO, T) &= (\exists k: k\ge 0: P and H_k(T))\cr 
& \Rightarrow (\exists k: k\ge 0 : H_k (P \and \non BB))\cr 
&=\wp(DO, P \and \non BB)\cr 
} 
$$
� ��� ����� �������� ��������  �������  (8) ��� ����������� 
����������. �������� �������� ������� ��� ����������� ���������� 
������������ �� ���, ��� �� � �����������, �� � �� ��������� �� 
����������� ����������� ����� ������� ���������� �������. ���� 
��� ��������� ���� � ��� �������, ����� ��� ����� �� ������������ 
��������� ����������.

\bye
