无穷重写的余归纳处理

我们引入了无穷项重写的余归纳定义。该设置出奇地简单，与通常的无穷重写定义不同，既不需要序数也不需要度量收敛。虽然余归纳处理无穷重写的想法并不新鲜，但所有先前的方法都局限于长度至多$\omega$的归约。本文提出的方法是第一个捕获具有任意序数长度的完全无穷项重写的方法。除了对已知概念的优雅重新表述外，我们的方法还非常自然地引出了无穷等式推理的新概念。