Contents

{-# OPTIONS --guardedness --sized-types #-}

module General.index where

In this part we present our results on formal series that are valid for every product rule. The rest of the section is structured as follows.

In Series we define formal series and their vector space structure.

In Terms we define the notion of terms and develop their basic properties.

In ProductRules we define the notion of a product rule P, which is then used in Products to define the P-product operation on formal series.

In FinitelyGenerated we study the resulting notion of P-finite series and in Automata we study P-automata. This culminates with a proof of the coincidence of P-finite series and series recognized by P-automata.

Finally, in Reversal we study right derivatives and reversals of formal series, and in ReversalEnd we study what happens when reversal is an endomorphism.

import General.Series
import General.Terms
import General.ProductRules
import General.Products
import General.FinitelyGenerated
import General.Automata
import General.Reversal
import General.ReversalEnd

References