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}
|
