Coinductive foundations of infinitary rewriting and infinitary equational logic

We present a coinductive framework for defining and reasoning about the infinitary analogues of equational logic and term rewriting in a uniform way. We define Equation found, the infinitary extension of a given equational theory =R, and →^∞, the standard notion of infinitary rewriting associated to a reduction relation →R, as...

Housing: Appendices