Autowrite: A tool for checking properties of term rewriting systems Huet and Lévy have shown that for the class of orthogonal term rewriting systems (TRSs) every term not in normal form contains a needed redex (i.e., a redex contracted in every normalizing rewrite sequence) and that repeated contraction of needed redexes results in a normal form if it exists. However, neededness is in general undecidable. In order to obtain a decidable approximation to neededness Huet and Lévy introduced the subclass of strongly sequential TRSs and showed that strong sequentiality is a decidable property of orthogonal TRSs.