2.2.3

Доказательство коммутативности сложения с 1:
суперкомпиляция предиката P


 
P     {   ex   =   <Eq (<Ad (ex) (I)>) (<Ad (I) (ex)>)>;
}
Ad   { (ex (ey) = ex ey;
}
Eq    {    () () T;
(ex I)  (ey I)   = <Eq (ex) (ey)>;
() (ey I) = F;
(ex I) () = F;
}

 
  <P e1>  
¯
  <Eq (<Ad (e1) (I)>) (<Ad (I) (e1)>)>  
¯
  <Eq (e1 I) (I e1)>   
e1 ® пусто    l m    e1 ® e2 I
  <Eq (I) (I)>  
  <Eq (e2 I I) (I e2 I)>  
¯ ¯
  <Eq () ())>  
  <Eq (e1 I) (I e1)>   
¯ ¯
  T  
e1 := e2