To explain how terms are computed to canonical form, we introduce the relation \(a \Rightarrow v\) between closed terms \(a\) and canonical forms (values) \(v\) given by the following computation rules: