Termination of string rewriting is known undecidable. Termination of string rewriting with only one rule is neither known decidable nor known undecidable. This paper presents a decision procedure for rules $u\rightarrow v$ such that some letter b from u occurs as often or less often in v. We call such rules "grid" rules. By far most rules are grid rules. Grid rules cover all rules which terminate by a total division order. Thus total division orders are shown to be irrelevant for the termination problem of one-rule string rewriting.

List homomorphisms are functions that are parallelizable using the divide-and-conquer paradigm. We study the problem of finding homomorphic representations of functions in the Bird–Meertens constructive theory of lists, by means of term rewriting and theorem proving techniques. A previous work proved that to each pair of leftward and rightward sequential representations of a function, based on cons - and snoc -lists, respectively, there is also a representation as a homomorphism. Our contribution is a mechanizable method to extract the homomorphism representation from a pair of sequential representations. The method is decomposed to a generalization problem and an inductive claim, both solvable by term rewriting techniques. To solve the former we present a sound generalization procedure which yields the required representation, and terminates under reasonable assumptions. The inductive claim is provable automatically. We illustrate the method and the procedure by the systematic parallelization of the scan -function (parallel prefix) and of the maximum segment sum problem.