2.2.5

Доказательство коммутативности сложения с 1:
выдача суперкомпилятора
Входной файл CommAdd1.ref:
  
*$MST_FROM_ENTRY;

$ENTRY 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;
}
Выходной файл r_CommAdd1.ref (руками удалены комментарии):
  
$ENTRY P {
 e.41  = T ;
}