  The $Reflection$ $Calculus$ ($\mathcal{\mathbf{RC}}$) is the fragment of the
polymodal logic $\mathcal{\mathbf{GLP}}$ in the language $L^+$ whose formulas
are built up from $\top$ and propositional variables using conjunction and
diamond modalities. $\mathcal{\mathbf{RC}}$ is complete with respect to the
arithmetical interpretation that associates modalities with reflection
principles and has various applications in proof theory, specifically ordinal
analysis.
  We present ${\sf TRC}$, a tree rewriting system that is adequate and complete
with respect to $\mathcal{\mathbf{RC}}$, designed to simulate
$\mathcal{\mathbf{RC}}$ derivations. ${\sf TRC}$ is based on a given
correspondence between formulas of $L^{+}$ and modal trees ${\sf
Tree}^{\Diamond}$. Modal trees are presented as an inductive type allowing
precise positioning and transformations which give rise to the formal
definition of rewriting rules and facilitates formalization in proof
assistants. Furthermore, we provide a rewrite normalization theorem for
systematic rule application. The normalization of the rewriting process
enhances proof search efficiency and facilitates implementation.
  By providing ${\sf TRC}$ as an efficient provability tool for
$\mathcal{\mathbf{RC}}$, we aim to help on the study of various aspects of the
logic such as the subformula property and rule admissibility.
