2.3.4

Доказательство коммутативности сложения с 1:
построение остаточной программы


 
 
  <P e1>  
e1 ® пусто    l m    e1 ® e2 I
 
  T  
e1 := e2
 
 

 
P     {    =   Т;
e2 I   =  <P e2>;
}
 

 
P     {    e1 =   Т;
}