  Proof terms in term rewriting are a representation means for reduction
sequences, and more in general for contraction activity, allowing to
distinguish e.g simultaneous from sequential reduction. Proof terms for
finitary, first-order, left-linear term rewriting are described in the Terese
book, chapter 8. In a previous work, we defined an extension of the finitary
proof-term formalism, that allows to describe contractions in infinitary
first-order term rewriting, and gave a characterisation of permutation
equivalence.
  In this work, we discuss how projections of possibly infinite rewrite
sequences can be modeled using proof terms. Again, the foundation is a
characterisation of projections for finitary rewriting described in Terese,
Section 8.7. We extend this characterisation to infinitary rewriting and also
refine it, by describing precisely the role that structural equivalence plays
in the development of the notion of projection. The characterisation we propose
yields a definite expression, i.e. a proof term, that describes the projection
of an infinitary reduction over another.
  To illustrate the working of projections, we show how a common reduct of a
(possibly infinite) reduction and a single step that makes part of it can be
obtained via their respective projections. We show, by means of several
examples, that the proposed definition yields the expected behavior also in
cases beyond those covered by this result. Finally, we discuss how the notion
of limit is used in our definition of projection for infinite reduction.
