NVNF-sequentiality of left-linear term rewriting systems

This paper introduces NVNF-sequentiality which is an extension of NV-sequentiality defined by Oyamaguchi. It is shown that the class of NVNF-sequential systems prop-erly includes the class of $\mathrm{N}\mathrm{V}$-sequential systems, and the indices with respect to NVNF-sequentiality are computed for a given term when a term rewriting system is NVNF-sequential. NVNF-sequentiality is decidable, and the index reduction is normalizing strat-egy for NVNF-sequential orthogonal term rewriting systems.