2.2.4
Доказательство коммутативности сложения с 1:
построение остаточной программы
<P e
1
>
e
1
®
пусто
l
m
e
1
®
e
2
I
T
e
1
:= e
2
P
{
= Т;
e
2
I
= <P e
2
>;
}
P
{
e
1
= Т;
}