nLab termination

Let (X,)(X,\rightarrow) be an abstract rewriting system ie. a set equipped with a binary relation \rightarrow.

Then \rightarrow is terminating, strongly normalizing or noetherian iff there doesn’t exist any infinite reduction x 1x 2...x n...x_{1} \rightarrow x_{2} \rightarrow ... \rightarrow x_{n} \rightarrow ...

Last revised on August 6, 2022 at 13:12:25. See the history of this page for a list of all contributions to it.