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

• Notations for equivalence relations and partial orders
• Decidable sets
• Binary relations
• Lists
  • Notations
  • Induction principles
  • General lemmas
  • Lists of pairs
    • Combine
    • Mix
    • Flip
  • Lists as finite sets
  • More general lemmas
  • Subsets of a list
  • Pairs
  • Enumerate lists of a certain length
  • Pad a list with an element
  • Lists over a decidable set
• Sum function
• Function predicates
• Enumerate permutations of a list

RIS.atoms: Nominal sets.

• Set of atoms
• Permutations
  • Definitions and elementary properties
  • Inverse of a permutation
  • Equivalence of permutations
  • Elements
  • Lifting an action on S to an action on list S
• Nominal sets
  • Definitions
  • Canonical nominal structures
    • Atoms
    • Lists
    • Pairs
    • Natural numbers
    • Option types
    • Sum types
  • Properties of group actions
• Minimality of support
• Useful remarks
• Equivariant functions

RIS.bijection: generate permutations.

• Permutation out of two lists
• Permutation out of a bijection
• Enumerate permutations

RIS.nominalsetoid: Nominal sets up-to equivalence.

• Definitions
• Lifting the structure to lists

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

• Preliminary definitions
  • Parameters
  • Letters
  • Binding monoid
  • Binding power
  • Balance properties
  • Decomposition properties
• Alpha-equivalence

RIS.stacks: an algebra of stacks.

• Definitions
• Simple properties
  • Accepting
  • absent
  • paired
• Converting a stack into a permutation

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

• Transducer
  • Definition
  • The function δt: computing a path in the transducer
  • Elementary properties
  • Binding power
  • Applying permutations on one component
• Main result
  • Completeness
  • Soundness

RIS.equiv_stacks: dynamic properties of the binding transducer.

• Static equivalence
• Definitions
• Lemmas
  • equiv_stacks
  • Characteristic words
  • Bissimilarity
  • Similarity
  • Semantics

RIS.alternate_eq: equivalent definitions of alpha-equivalence.

• Alternative definition of alpha-equivalence
  • Main results
  • Additional properties
• Alpha-equivalence from "Leaving the nest"

RIS.traces: extracting stacks directly from words.

• Simple trace
• Indexed traces
  • Technical definition
  • Main definitions
  • Properties of indexed traces
• Correspondence with stacks

RIS.representative: generic representation of nominal sets.

• Orbits
  • Definitions
  • Properties of orbits' relations
  • Nominal setoid structure.
• Lifting injections between sets of atoms as injective morphisms between sets of orbits.
• Representation of a nominal set
  • Hypothesis
  • Group-theoretic orbits
  • Representation
• Pointers
• The function η

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

• Adding natural numbers in the set of atoms
  • Lifting variables
  • Lifting letters
  • Lifting words
• Valid words and dynamic sequences
  • Validity
    • Definition
    • Boolean predicate
    • Remarks about validity
  • Defects
  • Dynamic sequences
• Normalisation
  • Rewrite steps
  • Normalisation procedure
• Concatenation of valid words and dynamic sequences
  • Addition as a permutation
  • Validity preserving concatenation
• 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.

• Definitions
  • Basic properties
  • Basic structures
  • Kleene algebra and Boolean algebra
• Facts about boolean algebra
  • Elementary properties
  • Boolean algebra as other structures
• Join semi-lattices
• Kleene algebras

RIS.language: Languages.

• Definitions
• Compatibily of the operations with the ordering
• Algebraic properties

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

• Definitions
• Basic properties
  • Properties of the language interpretation
  • Properties of the axiomatic equivalence
• The axiomatization KA.
• Equatity modulo associativity, commutativity, idempotence and units.
• Utilities
  • Variables
  • Empty word
  • Empty language
  • Unit language
  • Finite sums
  • Finite products
• 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

• Nominal structure
• Facts about the support
• Facts about the group action
• Splitting the size by name

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.

• Definitions
• Elementary facts
• Square expressions
• Homogeneous expressions
• Spines

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