Small step structural operational semantics sos

A style of semantics which defines evaluation via Evaluation statement/judgement of the form $t \to t'$, specifying how a term reduces by one atomic step at a time until reaching a Normal form.