2.3.2

Доказательство коммутативности сложения с 1:
определение предиката P
 
P     {   ex   =   <Eq (<Ad (ex) (I)>) (<Ad (I) (ex)>)>;
}
Ad   { (ex)  () = ex;
(ex) (ey I) = <Ad (ex) (ey)> I;
}
Eq    {    () () =  T;
(ex I)  (ey I)   = <Eq (ex) (ey)>;
() (ey I) = F;
(ex I) () = F;
}
Пример выполнения программы (1+2 = 2+1):
 

<P I I>

<Eq (<Ad (I I) (I)>) (<Ad (I) (I I)>)>

<Eq (<Ad (I I) ()> I) (<Ad (I I) (I)>)>

<Eq (I I I) (<Ad (I) (I I)>)>

<Eq (I I I) (<Ad (I) (I)> I)>

<Eq (I I I) (<Ad (I) ()> I I)>

<Eq (I I I) (I I I)>

<Eq (I I) (I I)>

<Eq (I) (I)>

<Eq () ()>

T