Evaluation statement judgement

A formal assertion of the form $t \to t'$ or $t \Downarrow v$, stating that a term reduces to another term or evaluates to a value under specific Inference rules.