Mam problem dotyczący udowadniania poprawności semantycznej algorytmu ;/
nie wiem w jakiś sposób zapisać warunki alfa beta i gamma żeby dało się pokazać ze schemat Hornera poprawnie liczy wartość wielomianu, wie ktoś może gdzie mogę odnaleźć informacje na ten temat?

próbowałem tak,

alfa: a1,a2,..ak;
beta: w = a1x(k-1) +a2x</sup>(k-2) + ... +ak
gamma: ???