## RIS.tools: Toolbox of simple definitions, lemmas and tactics.

- Notations for equivalence relations and partial orders
- Decidable sets
- Binary relations
- Lists
- Sum function
- Function predicates
- Enumerate permutations of a list

## RIS.atoms: Nominal sets.

## RIS.bijection: generate permutations.

## RIS.nominalsetoid: Nominal sets up-to equivalence.

## RIS.words: words, binding monoid and alpha-equivalence.

## RIS.stacks: an algebra of stacks.

## RIS.transducer: definition and properties of the binding transducer.

## RIS.equiv_stacks: dynamic properties of the binding transducer.

## RIS.alternate_eq: equivalent definitions of alpha-equivalence.

## RIS.traces: extracting stacks directly from words.

## RIS.representative: generic representation of nominal sets.

- Orbits
- Lifting injections between sets of atoms as injective morphisms between sets of orbits.
- Representation of a nominal set
- Pointers
- The function η

## RIS.normalise: normal form for words up-to alpha-equivalence.

- Adding natural numbers in the set of atoms
- Valid words and dynamic sequences
- Normalisation
- Concatenation of valid words and dynamic sequences
- Relational interpretation

## RIS.factors: square bindings and binding division.

- Enumerate bindings
- Factors
- Division when one projection is 0
- Square bindings
- Square factors of square bindings

## RIS.algebra: algebraic structures.

## RIS.language: Languages.

## RIS.regexp: regular expressions and the free Kleene algebra.

- Definitions
- Basic properties
- The axiomatization KA.
- Equatity modulo associativity, commutativity, idempotence and units.
- Utilities
- Derivatives
- Prefixes of a regular language
- Antimirov derivatives

## RIS.completenessKA: Link with relation-algebra to import the completeness proof of Kleene algebra.

## RIS.automata: finite state automata.

## RIS.systems: affine systems of equations

- Solving affine systems
- Automata as affine systems
- The Antimirov system
- Inclusion of two systems
- Intersection of two systems

## RIS.positive_regexp: regular expressions that do not contain the empty word.

## RIS.subword: the subword ordering on words.

## RIS.aeq_facts: lemmas about α-equivalence and the equivalence transducer.

## RIS.alpha_regexp

## RIS.alphaKA: axiomatisation of regular languages up-to α-equivalence.

## RIS.closed_languages: languages closed by α-equivalence.

## RIS.binding_finite: binding-finite and memory-finite expressions.

## RIS.closed_automaton: computing an automaton for the α-closure of an expression.

This page has been generated by coqdoc