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 follows: (Formula Presented) Equation found Here μ and ν are the least and greatest fixed-point operators, respectively, and (Formula Presented) Equation found 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.@en

Moessner’s Theorem describes a construction of the sequence of powers (1n, 2n, 3n, . . .), by repeatedly dropping and summing elements from the sequence of positive natural numbers. The theorem was presented by Moessner in 1951 without a proof and later proved and generalized in several directions. More recently, a coinductive proof of the original theorem was given by Niqui and Rutten. We present a formalization of their proof in the Coq proof assistant. This formalization serves as a non-trivial illustration of the use of coinduction in Coq. During the formalization, we discovered that Long and Sali´e’s generalizations could also be proved using (almost) the same bisimulation.@en