2.3.5

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

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