1: \begin{abstract}

2:   We present a coinductive framework for defining infinitary analogues of equational reasoning 

3:   and rewriting in a uniform way. We define the relation $\ieq$, a notion of 

4:   infinitary equational reasoning, and $\ired$, the standard notion of infinitary rewriting as follows:

5:   \begin{align*}

6:     {\ieq} &\;\;\defd\;\; \gfp{R}{(=_{\aes} \cup \mathrel{\down{R}})^*} \\ %

7:   %

8:   %

9:     {\ired} &\;\;\defd\;\; \lfp{R}{\gfp{S}{(\to_{\atrs} \cup \mathrel{\down{R}})^*\relcomp \down{S}}} %

10:   %

11:   %

12:   \end{align*}

13:   where $\slfp$ and $\sgfp$ are the least and greatest fixed-point operators, respectively,

14:   %

15:   and where 

16:   \begin{align*}

17:     \down{R} \;\defd\; \{\,\pair{f(s_1,\ldots,s_n)}{\,f(t_1,\ldots,t_n)} \mid f \in \Sigma,\, s_1 \mathrel{R} t_1,\ldots,s_n \mathrel{R} t_n\,\} \,\cup\, \id  \,.

18:   %

19:   \end{align*}

20:   

21:   The setup captures rewrite sequences of arbitrary ordinal length, 

22:   but it has neither the need for ordinals nor for metric convergence. 

23:   This makes the framework especially suitable for formalizations in theorem provers.

24: \end{abstract}

25: