aboutsummaryrefslogtreecommitdiffhomepage
path: root/theories/Relations/intro.tex
blob: 5056f36f9762ba33e48d11404ee0ee84668cd5a8 (plain)
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
\section{Relations}\label{Relations}

This library develops closure properties of relations.

\begin{itemize}
\item {\tt Relation\_Definitions.v} deals with the general notions
  about binary relations (orders, equivalences, ...)

\item {\tt Relation\_Operators.v} and {\tt Rstar.v} define various
  closures of relations (by symmetry, by transitivity, ...) and
  lexicographic orderings.

\item {\tt Operators\_Properties.v} states and proves facts on the
  various closures of a relation.

\item {\tt Relations.v} puts {\tt Relation\_Definitions.v}, {\tt
    Relation\_Operators.v} and \\
    {\tt Operators\_Properties.v} together.

\item {\tt Newman.v} proves Newman's lemma on noetherian and locally
  confluent relations.

\end{itemize}