1: \begin{abstract}

2: \die{  We present a coinductive framework for developing the infinitary analogues of equational reasoning 

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

4:   infinitary equational reasoning with respect to an equality relation

5:   $=_{\aes}$, and $\ired$, the standard notion of infinitary rewriting

6:   with respect to a reduction relation $\to_{\atrs}$, as follows:}

7: We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic

8:   and term rewriting in a uniform way. We define $\ieq$, the

9:   infinitary extension of a given equational theory $=_{\aes}$,

10:   and $\ired$, the standard notion of infinitary rewriting

11:   associated to a reduction relation $\to_{\atrs}$, as follows:

12:   \begin{align*}

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

14:   %

15:   %

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

17:   %

18:   %

19:   \end{align*}

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

21:   %

22:   and 

23:   \begin{align*}

24:     \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  \,.

25:   %

26:   \end{align*}

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

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

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

30: \end{abstract}

31: