Transformation of polynomial evaluation to a pipeline via Hornerʹs rule

We apply algebraic transformation techniques to synthesise Hornerʹs rule for polynomial evaluation. Hornerʹs rule is then transformed into a pipeline by the application of further axioms. The syntheses demonstrate the power of the algebraic style, in which inductive proof is replaced by constructive unfolding and folding of standard higher-order functions defined on lists.