# Coinductive Foundations of Infinitary Rewriting and Infinitary Equational Logic

## TL;DR

This paper introduces a coinductive framework for infinitary equational logic and rewriting that handles sequences of any ordinal length without relying on ordinals or metrics, facilitating formalization.

## Contribution

It provides a uniform, coinductive approach to infinitary rewriting and equational logic, avoiding the complexities of ordinal and metric-based methods.

## Key findings

- Framework captures rewrite sequences of arbitrary ordinal length
- No need for ordinals or metric convergence in the framework
- Suitable for formalizations in theorem provers

## Abstract

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform, coinductive way. The setup captures rewrite sequences of arbitrary ordinal length, but it has neither the need for ordinals nor for metric convergence. This makes the framework especially suitable for formalizations in theorem provers.

---
Source: https://tomesphere.com/paper/1706.00677