\subsection{Soundness of Reduction}
\label{sec:soundness-of-reduction}

% This subsection gives the proof that each reduction step doesn't alter the semantic