The Algebra of Infinite Sequences: Notations and Formalization
Nachum Dershowitz, Jean-Pierre Jouannaud, Qian Wang · HAL (Le Centre pour la Communication Scientifique Directe) · 2014
Abstract. We propose some convenient notations for expressing complicated properties of finite and infinite, ordinal-indexed sequences. The algebra of ordinal-indexed sequences is being implemented in the proofassistant Coq, together with the algebra of ordinals represented in Cantor normal form. 1