Diagonals and Block-Ordered Relations
Roland Backhouse[University of Nottingham, UK;
corresponding author]
and Ed Voermans[Independent Researcher, The Netherlands]

More than 70  years ago, Jaques Riguet suggested the existence of   an “analogie frappante”
(striking analogy) between so-called “relations de Ferrers” and a class of difunctional relations,
members of which we call “diagonals”.   Inspired by his suggestion, we formulate an  “analogie
frappante” linking  the notion of a block-ordered relation and the notion of the diagonal of a relation.
We formulate several novel properties of the core/index  of a diagonal, and use these properties to
rephrase our “analogie frappante”.  Loosely speaking, we show that a block-ordered relation  is a
provisional ordering   up to isomorphism and reduction to its  core.  (Our theorems make this informal
statement precise.) Unlike Riguet  (and others who follow his example),  we avoid almost entirely the
use of nested complements  to express  and reason about properties of these notions:   we  use factors (aka
residuals) instead.  The only (and inevitable) exception to this is to show that our definition of a  “staircase”
relation is equivalent to Riguet's definition of a “relation de Ferrers”.    Our “analogie frappante” also
makes it obvious that a  “staircase” relation is not necessarily block-ordered, in spite of the mental
picture of such a relation presented by Riguet.

§ INTRODUCTION

More than seventy years ago, in a series of publications [18, 19, 20],  Jacques Riguet introduced
the notions of a “relation difonctionelle” and  “relations de Ferrers”.   In
[20] he remarked on an “analogie frappante” between these two notions via what he referred to
as the “diff'erence”  of a given relation.   Riguet [20] states the following theorem:

Pour que $R$ soit une relation de Ferrers, il
faut et il suffit que $R$ soit r'eunion de rectangles dont les projections de même nom sont totalement
ordonn'ees par inclusion et tels que si la premi`ere projection de l'un des rectangles est contenue dans
la premi`ere projection d'un autre rectangle, la seconde projection du second est contenue dans
la seconde projection du premier.

For those unable to read French, the theorem states a necessary and sufficient condition for a relation to
be “de Ferrers” in terms of totally ordered rectangles  (“rectangles $\ldots$ totalement
ordonn'ees”).   The theorem clearly begs the question what is the definition of a “relation de Ferrers”.  We
postpone answering this question until section <ref>.  The reason for doing so is that Riguet gives both  a formal
definition and a mental picture —a picture like the one  in fig. <ref> of what we call a “staircase
relation”— but it is far from obvious how Riguet's definition and the mental picture are related.

Mental Picture of a  Staircase Relation

Riguet does not give a proof of the theorem and his  “analogie frappante” between  “relations de Ferrers” and
difunctional relations is unclear.  The proof of Riguet's theorem  is quite
straightforward: see [6].   However, clarifying the “analogie frappante” is  more difficult.

The work presented here initially began as an attempt to properly understand Riguet's work and to
rectify errors in extant literature.  We introduce, in section <ref>,  the “diagonal” of a
relation and, in section <ref>,  the notion  of a “block-ordered relation”.  The
“diagonal” of a relation is what Riguet referred to as the “diff'erence”; it is a difunctional relation.  We
formulate an “analogie frappante” (specifically, theorem <ref>) linking block-ordered relations
and diagonals.   We also formalise  the notion of a “staircase” relation:    as shown in [6],  our
definition  of a “staircase” relation and Riguet's  definition of a  “relation de Ferrers” are
equivalent[The name “staircase” is more informative than “relation de Ferrers” and our
definition uses factors rather than complementation  (from which Riguet's terminology “diff'erence” is
derived),   which is why we prefer to deviate from Riguet's presentation].    Ostensibly a “staircase”
relation is “block-ordered” where the “blocks” are totally ordered.  But, as we observed in our
initial investigations, this is not the case: as we show in section <ref>, the less-than
relation on real numbers is a “staircase” relation but is not “block-ordered”.

In addition to our  “analogie frappante”, a major contribution of our work is the application of the notions
of a core/index of a relation.  These notions and their properties are briefly summarised in section
<ref>.  Informally,  a core[We say “a” core because a relation typically has many
cores; all cores of a relation are, however, isomorphic.] of a relation captures its essential properties.  For example, a core
of a difunctional relation is an isomorphism.  An index of a relation is a core of the relation that has the
same type as the relation.
A fuller account of their properties is given in [10, 11].  In this paper, we
state and prove a number of properties of the core/index of the diagonal of a relation.  These properties
are relevant to our analogie frappante: theorem <ref> gives a method of testing whether or not a
relation is block-ordered in terms of the diagonal of the relation, and
theorem <ref> reformulates the test in terms of the core of the relation.

During the course of our investigation, we became aware of very similar work by Winter [23].
Winter's notion of “relations of order shape” is identical to our notion of “block-ordered relation”.
Winter also introduces the notion of the “diagonal” of a relation — but does not give the notion a name
and does not attribute the notion to Riguet [20].  (He does cite [20] and he denotes the
“diagonal” of a relation $R$ by $R^{d}$, his definition of which is identical to the definition of the  “diff'erence” of $R$
given by Riguet.)  Consequently, there is some overlap between our work and Winter's work.  We believe
the overlap is justified because we formulate the notion of a “diagonal” in terms of factors (“residuals” in
the terminology used by Winter) and we avoid the use of complements altogether — with the exception
of section <ref> where we observe the equivalence of the notion of a “staircase”
relation with Riguet's notion of a “relation de Ferrers”.  (Winter does express some properties in terms of
factors but, following in Riguet's footsteps,  his calculations invariably use complements, which he
denotes by an overbar.)  Winter also observes that not all “staircase” relations are “block-ordered” but
does not give any concrete example.  See the concluding section for further discussion of this aspect of
Winter's paper.

In order to make this paper relatively self-contained,  sections <ref> and  <ref>
summarise the axioms of (point-free) relation algebra and some basic concepts.  Typically, proofs of
properties stated in these sections  are omitted.  Exceptions to this rule concern properties that we deem
less familiar to many readers (for example, factorisation properties of functional relations   in section
<ref>).   Section <ref> introduces the notions of a core/index of a relation.   For proofs
of properties stated in this section see [10, 11].

§ AXIOMS OF POINT-FREE RELATION ALGEBRA

In this section, we give a brief summary of the axioms of point-free relation algebra.  For full details
of the axioms, see [8].

§.§ Summary

Point-free relation algebra comprises three layers with interfaces between the layers plus additional axioms
peculiar to relations.  The axiom system is typed.  For types $A$ and $B$,  0.15em$A{\sim}B$ denotes a set;  the elements of the set are called
(heterogeneous) relations of type  $A{\sim}B$.  Elements of type $A{\sim}A$, for some  type  $A$, are called homogeneous

The first layer axiomatises the properties of a partially ordered  set.  We postulate that, for each pair of
types $A$ and $B$,  $A{\sim}B$ forms  a complete, universally distributive lattice.     We use the symbol “${\subseteq}$” for the ordering relation, and  “${\cup}$”
and “${\cap}$” for the supremum and infimum operators.   We assume that this notation is familiar to the
reader, allowing us to skip a more detailed account of its  properties.   However, we use   ${\MPplatbottom}$
for the least element of the ordering  (rather than the conventional $\emptyset$)  and ${\MPplattop}$ for the greatest element.  In keeping with the
conventional practice of overloading the  symbol “$\emptyset$”, both these symbols are overloaded.

It is important to note that there is no axiom stating that a relation is a set, and there is no corresponding
notion of membership.   The lack of a notion of membership distinguishes point-free relation algebra from
pointwise algebra.

The second layer adds a composition operator.  If $R$ is a relation of type $A{\sim}B$ and $S$ is a relation of type
$B{\sim}C$, the composition of $R$ and $S$ is a relation of type $A{\sim}C$ which we denote by $R{\MPcomp}S$.     Composition is
associative and, for each type $A$, there is an identity relation which we denote by $I_{A}$.  We often overload
the notation for the identity relation, writing just $I$.  Occasionally, for greater clarity, we do supply the
type information.

The interface between the first and second layers defines a relation algebra to be an instance of a regular
algebra [5] (also  called a standard Kleene algebra, or S-algebra [12]).   For this paper,
the most important aspect of this interface is the existence and properties of the factor operators.  These
are introduced in section <ref>.  Also, ${\MPplatbottom}$ is a zero of composition: for all $R$,

The completeness axiom in the first layer  allows the reflexive-transitive closure $R^{*}$ of
each element  $R$  of type  $A{\sim}A$, for some type $A$,  to be defined.

The third layer is the introduction of a converse operator.   If $R$ is a relation of type $A{\sim}B$, the converse of
$R$, which we denote by $R^{\MPrev}$ (pronounced $R$ “wok”) is a relation of type $B{\sim}A$.
The interface with the first  layer is that converse is simultaneously  the lower and upper adjoint in a Galois
connection, and thus  a poset isomorphism (in particular,  ${\MPplatbottom}^{\MPrev}\ms{1}{=}\ms{1}{\MPplatbottom}$ and
${\MPplattop}^{\MPrev}\ms{1}{=}\ms{1}{\MPplattop}$);   the interface with the
second layer is formed by the two rules   $I^{\MPrev}\ms{1}{=}\ms{1}I$ and, for all relations $R$ and $S$ of appropriate type,

Additional axioms characterise properties peculiar to relations.
The modularity rule (aka Dedekind's rule [18]) is that, for all relations $R$, $S$ and $T$,
\begin{equation}\label{dedekind.rule}
\end{equation}
The dual property, obtained by exploiting properties of the converse operator, is, for all relations $R$, $S$ and $T$,
\begin{equation}\label{dedekind.rule.conv}
\end{equation}
The modularity rule is
necessary to the derivation of some of the properties we state without proof (for example, the
properties of the domain operators given in section <ref>).  Another rule is  the cone rule:
\begin{equation}\label{cone.rule}
\end{equation}
The cone rule limits consideration to “unary” relation algebras:  constructing the cartesian product of two
relation algebras to form a relation algebra (whereby the operators are defined pointwise) does not yield
an algebra satisfying the cone rule.

§.§ Factors

If $R$ is a relation of type $A{\sim}B$ and $S$ is a relation of type $A{\sim}C$, the relation $R{\setminus}S$ of type $B{\sim}C$ is defined by
the Galois connection, for all $T$ (of type $B{\sim}C$),
\begin{equation}\label{under}
\end{equation}
Similarly,  if $R$ is a relation of type $A{\sim}B$ and $S$ is a relation of type $C{\sim}B$, the relation $R{/}S$ of type $A{\sim}C$ is defined by
the Galois connection, for all $T$,
\begin{equation}\label{over}
\end{equation}
The existence of factors is a property of a regular algebra; in relation algebra, factors are also known as
“residuals”.    Factors enjoy a rich theory which underlies many of our calculations.

The relations $R{\setminus}R$ (of type $B{\sim}B$ if $R$ has type $A{\sim}B$) and $R{/}R$ (of type $A{\sim}A$ if $R$ has type $A{\sim}B$) play a
central rôle in section <ref>.  As is easily verified, both are preorders.  That is, both are transitive:R∖R11R∖R4⊆4R∖R9∧9R/R11R/R4⊆4R/Rand both are reflexive:I3⊆3R∖R8∧8I3⊆3R/R  .(The notation “$I$” is overloaded in the above equation.  In the left conjunct, it
denotes the identity relation of type $B{\sim}B$ and, in the right conjunct, it
denotes the identity relation of type $A{\sim}A$, assuming $R$ has type $A{\sim}B$.  We often overload constants in
this way. Note, however, that we do not attempt to combine the two inclusions into one.)
In addition, for all $R$,
\begin{equation}\label{factor.eq}
\end{equation}

\begin{equation}\label{preorder.1}
\end{equation}

\begin{equation}\label{preorder.2}
\end{equation}

\begin{equation}\label{preorder.3}
\end{equation}
In fact, we don't use (<ref>) directly; its relevance is as the initial step in proving the leftmost
equations of (<ref>) and (<ref>).  We choose not to exploit the associativity of the over and
under operators in (<ref>) and (<ref>) —by writing, for example, $(R{\setminus}R){/}(R{\setminus}R)$ as
$R{\setminus}R{/}(R{\setminus}R)$— in order to emphasise their rôle as properties of the
preorders  $R{\setminus}R$  and $R{/}R$.

In relation algebra (as opposed to regular algebra) it is possible to eliminate the factor operators
altogether because they can be expressed in terms of complements and converse.  The rules for doing so
are  as follows: for all $R$, $S$ and $T$,
\begin{equation}\label{underovernot}
\end{equation}

\begin{equation}\label{underover.to.not}
\end{equation}
Although the  elimination of factors  is highly
undesirable,  we are obliged to introduce complements in order to compare our work with that of Riguet
in section <ref> on staircase relations.

Property (<ref>) exemplifies how much easier calculations with factors can be compared to
calculations that combine complements with converses.  The property is very easy to spot and apply.
Expressed using  (<ref>), it is equivalent to R11(R^11R)6=6R6=6(R11R^)11R  .In this form, the property is difficult to spot and its correct application is difficult to check.

It is useful to record the distributivity properties of converse over the factor operators:
For all $R$ and $S$,
\begin{equation}\label{factor.props.under}
\end{equation}
\begin{equation}\label{factor.props.over}
\end{equation}
\begin{equation}\label{factor.props.both}
\end{equation}

In  (<ref>) and (<ref>), the inclusion of terms involving complements
is only  relevant in section <ref>.

§ SOME DEFINITIONS

This section introduces a number of concepts which have been studied in detail elsewhere.  For the most
part, their properties are stated without proof.  An exception to this is in section <ref> where we
combine the Galois connections defining factors with the Galois connection defining functionality.

§.§ Coreflexives

In point-free relation algebra, “coreflexives” of a given type   represent sets of elements of that type.  A
coreflexive of type $A$ is a relation $p$ such that $p\ms{1}{\subseteq}\ms{1}I_{A}$.  Frequently used properties are that, for all
coreflexives $p$,  p2=2p^2=2ppand, for all coreflexives $p$ and $q$, pq3=3p1∩1q3=3qp  .(The proof of these properties relies on the modularity rule.)  In the literature, coreflexives have several
different names, usually depending on the application area in question.  Examples are “monotype”,
“pid” (short for “partial identity”)  and “test”.

§.§ The Domain Operators

The “domain operators” (see eg. [9])  play a dominant and unavoidable role.  We
exploit their properties frequently in calculations, so much so that we assume great familiarity with
[Domain Operators]   Given  relation $R$ of type $A{\sim}B$,
the left domain $R{\MPldom{}}$  of   $R$ is a relation of type $A$ defined by the equation R6=6I_A3∩3R11R^and the right  domain $R{\MPrdom{}}$  of    $R$is a relation of type $B$  is defined by the equation R6=6I_B3∩3R^11R  .

The name “domain operator” is chosen because of the fundamental properties: for all $R$ and all
coreflexives $p$,
\begin{equation}\label{rdom.is.least}
\end{equation}
\begin{equation}\label{ldom.is.least}
\end{equation}
A simple, often-used consequence of (<ref>) and (<ref>) is the property:
\begin{equation}\label{ldom.and.rdom}
\end{equation}

As is the case for factors, the domain operators enjoy a rich theory which underlies many of our
calculations but we omit the details here.

§.§ Pers and Per Domains

Given relations $R$ of type $A{\sim}B$  and $S$ of type $A{\sim}C$,  the symmetric
right-division  is the  relation $R\rightsymdivision{}S$  of type $B{\sim}C$  defined in terms of right factors as
\begin{equation}\label{double.under.def}
\end{equation}
Dually, given relations $R$ of type $B{\sim}A$ and $S$ of type $C{\sim}A$,  the
symmetric left-division is the  relation $R\leftsymdivision{}S$  of type $B{\sim}C$ defined in terms of left factors as
\begin{equation}\label{double.over.def}
\end{equation}
The relation $R\rightsymdivision{}R$ is an equivalence relation.
Voermans [22] calls it the “greatest
right domain” of $R$. Riguet [18] calls $R\rightsymdivision{}R$ the “noyau”  of $R$ (but defines it using nested
complements).   Others  (see   [17] for references) call it the  “kernel” of $R$.

As remarked elsewhere [17],  the symmetric left-division inherits a number of (left) cancellation
properties from the properties of factorisation in terms of which it is defined.  In this section the focus is on
the left and right “per domains” introduced by Voermans [22].
[Right and Left Per Domains]   The right per domain of relation $R$, denoted
$R{\MPperrdom{}}$,   is defined by the equation
\begin{equation}\label{per.rightdomain}
\end{equation}
Dually, the left per domain of relation $R$, denoted $R{\MPperldom{}}$, is defined  by the equation
\begin{equation}\label{per.leftdomain}
\end{equation}

In order to prove additional
properties,   it is useful to record the left and right domains of  the   relation $R\rightsymdivision{}R\ms{1}{\MPcomp}\ms{1}R{\MPrdom{}}$.
For all $R$,(RR11R)4=4R4=4(R11RR)  ,(RR11R)4=4R4=4(R11RR)  ,RR11R3=3R11RR11R3=3R11RR  .

The left and right per domains are “pers” where “per” is an abbreviation of “partial equivalence
[Partial Equivalence Relation (per)]   A relation  is a partial equivalence
relation iff  it is symmetric and transitive. That is, $R$ is a partial equivalence relation iff R1=1R^5∧5RR1⊆1R  .Henceforth we abbreviate partial equivalence relation to per.

That $R{\MPperldom{}}$ and $R{\MPperrdom{}}$ are indeed pers is a direct consequence of the symmetry and transitivity of $R\rightsymdivision{}R$.

The left and right per domains are called “domains” because,  like the coreflexive domains, we have the
properties: for all relations $R$ and pers $P$,
\begin{equation}\label{per.rdom.is.least}
R\ms{1}{=}\ms{1}R{\MPcomp}P\ms{6}{\equiv}\ms{6}R{\MPperrdom{}}\ms{2}{=}\ms{2}R{\MPperrdom{}}\ms{1}{\MPcomp}\ms{1}P\mbox{~~, and}
\end{equation}

\begin{equation}\label{per.ldom.is.least}
\end{equation}
The right per domain  $R{\MPperrdom{}}$ can be defined equivalently by the equation
\begin{equation}\label{per.rightdomain.equiv}
\end{equation}
\begin{equation}\label{per.rightdomain.doms}
\end{equation}
(See [6] for the proofs of these properties.)  Symmetrical properties hold of $R{\MPperldom{}}$.

For further properties of pers and per domains, see [22].

§.§ Functionality

In this section, we present  a number of lesser-known properties of “functional” relations.   A relation $R$ of type $A{\sim}B$
is said to be  left-functional iff $R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}\ms{2}{=}\ms{2}R{\MPldom{}}$.    Equivalently,   $R$ is left-functional  iff $R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}\ms{2}{\subseteq}\ms{2}I_{A}$.
It is said to be  right-functional  iff  $R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R\ms{2}{=}\ms{2}R{\MPrdom{}}$ (equivalently,  $R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R\ms{2}{\subseteq}\ms{2}I_{B}$).   A relation $R$
is said to be a bijection iff it is both left- and right-functional.

Rather than left-  and right-functional, the more common terminology is “functional” and “injective”
but publications differ on which of left- or right-functional is “functional” or “injective”.  We choose to
abbreviate “left-functional” to functional and to use the term injective instead of right-functional.
Typically, we use  $f$ and $g$ to denote functional relations, and Greek letters to denote bijections (although
the latter is not always the case).  Other authors make the opposite choice.

The properties we present here stem from
the observation that functionality can be defined via a Galois connection.
Specifically, the relation   $f$ is (left-)functional iff, for all relations $R$ and $S$ (of appropriate type),
\begin{equation}\label{functional.GC}
\end{equation}
It is a simple exercise to show that (<ref>) is equivalent to the property $f\ms{1}{\MPcomp}\ms{1}f^{\MPrev}\ms{2}{\subseteq}\ms{2}I$.  (Although
(<ref>) doesn't immediately fit the standard definition of a Galois connection, it can be turned
into standard form by restricting the range of the dummy $R$ to relations that satisfy $f{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}R\ms{2}{=}\ms{2}R$, i.e.
relations $R$ such that $R{\MPldom{}}\ms{1}{\subseteq}\ms{1}f{\MPrdom{}}$.)

The converse-dual of (<ref>) is also used frequently:  $g$ is functional iff, for all $R$ and $S$,
\begin{equation}\label{functional.GC.conv}
\end{equation}

Comparing the Galois connections defining the over and under operators

with the Galois connection defining functionality (see  (<ref>)) suggests a formal relationship
between “division” by a functional relation and composition with the relation's converse.  The precise
form of this relationship is given by the following lemma.

For all $R$ and all functional relations $f$,f11f∖R5=5f^11R  .

Proof   We use the anti-symmetry of the subset relation.  First,

$=$		$\{$	domains$~~~ \}$

$\Leftarrow$		$\{$	monotonicity$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$\Leftarrow$		$\{$	definition and monotonicity$~~~ \}$

$f$ is functional   .

$\Leftarrow$		$\{$	$f{\MPrdom{}}\ms{2}{\subseteq}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}f$; monotonicity and transitivity$~~~ \}$

$\Leftarrow$		$\{$	monotonicity$~~~ \}$

$=$		$\{$	cancellation$~~~ \}$

Two  lemmas  that will be needed later now follow.   Lemma <ref>
allows the converse of a functional relation (i.e. an injective relation) to be cancelled, whilst lemma
<ref> expresses a distributivity property.

For all $R$ and all functional relations $f$,f22f^1∖1(f^11R)6=6f11R  .

$=$		$\{$	assumption:  $f$ is functional$~~~ \}$

$\subseteq$		$\{$	cancellation$~~~ \}$

$=$		$\{$	assumption:  $f$ is functional$~~~ \}$

$\Leftarrow$		$\{$	monotonicity$~~~ \}$

$=$		$\{$	factors$~~~ \}$

The lemma follows by anti-symmetry of the subset relation.

For all $R$ and $S$ and all functional relations $f$ ,R∖(Sf)11f5=5R∖S11f  .

$\Leftarrow$		$\{$	$f{\MPrdom{}}\ms{2}{\subseteq}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}f$,  monotonicity$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$\Leftarrow$		$\{$	cancellation$~~~ \}$

$=$		$\{$	assumption:  $f$ is functional$~~~ \}$

$\Leftarrow$		$\{$	monotonicity,  $f\ms{2}{=}\ms{2}f\ms{1}{\MPcomp}\ms{1}f{\MPrdom{}}$$~~~ \}$

$=$		$\{$	factors and cancellation$~~~ \}$

The lemma follows by anti-symmetry of the subset relation.

The following lemma is crucial to fully understanding Riguet's “analogie frappante”.

(The lemma is complicated by the fact that it
has five free variables.  Simpler, possibly better known, instances can be obtained by instantiating one or
more  of $f$, $g$, $U$ and $W$ to the identity relation.)
Suppose $f$ and $g$ are functional.  Then, for all $U$, $V$ and $W$,

$=$	$f{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}(g^{\MPrev}\ms{1}{\MPcomp}\ms{1}U\ms{1}{\MPcomp}\ms{1}f){\setminus}(g^{\MPrev}\ms{1}{\MPcomp}\ms{1}V\ms{1}{\MPcomp}\ms{1}f){/}(g^{\MPrev}\ms{1}{\MPcomp}\ms{1}W\ms{1}{\MPcomp}\ms{1}f)\ms{1}{\MPcomp}\ms{1}g{\MPrdom{}}~~.$

Proof   Guided by the assumed functionality of $f$ and $g$, we use the rule of indirect equality.  Specifically,
we  have, for all $R$, $U$, $V$ and $W$,

$=$		$\{$	assumption:    $f$ and $g$ are functional,   (<ref>) and (<ref>)$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	assumption:    $f$ and $g$ are functional

i.e.    $f\ms{1}{\MPcomp}\ms{1}f^{\MPrev}\ms{2}{=}\ms{2}f{\MPldom{}}\ms{3}{\wedge}\ms{3}g\ms{1}{\MPcomp}\ms{1}g^{\MPrev}\ms{2}{=}\ms{2}g{\MPldom{}}$$~~~ \}$

$=$		$\{$	assumption:    $f$ and $g$ are functional, (<ref>) and (<ref>)$~~~ \}$

$=$		$\{$	domains (four times)$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	$f{\MPrdom{}}$ and $g{\MPrdom{}}$ are coreflexives$~~~ \}$

The lemma follows by instantiating $R$ to the left and right sides of the claimed equation, simplifying using
domain calculus,  and then applying  the
reflexivity and anti-symmetry of the subset relation.

The final lemma in this section anticipates the discussion of per domains in section <ref>.
Suppose relations  $R$,     $f$    and $g$  are such that   f11f^3=3f3=3R6∧6g3=3g11g^  .Then, for all $S$,
\begin{equation}\label{fwok.elim.gen1}
\end{equation}
It follows that
\begin{equation}\label{fwok.elim.gen2}
\end{equation}

Proof   The proof of (<ref>) is as follows.

$=$		$\{$	factors:$~~~ \}$

$=$		$\{$	lemma <ref> with $f{,}R\ms{2}{:=}\ms{2}g\ms{1}{,}\ms{1}(f^{\MPrev}\ms{1}{\MPcomp}\ms{1}R){\setminus}(f^{\MPrev}\ms{1}{\MPcomp}\ms{1}S)$$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	$\left[\ms{2}R{\setminus}S\ms{1}{=}\ms{1}R{\setminus}(R{\MPldom{}}\ms{1}{\MPcomp}\ms{1}S)\ms{2}\right]$ with $R{,}S\ms{3}{:=}\ms{3}R\ms{2}{,}\ms{2}f^{\MPrev}\ms{1}{\setminus}\ms{1}(f^{\MPrev}\ms{1}{\MPcomp}\ms{1}S)$

assumption:  $f{\MPldom{}}\ms{1}{=}\ms{1}R{\MPldom{}}$$~~~ \}$

$=$		$\{$	lemma <ref> with $f{,}R\ms{1}{:=}\ms{1}f{,}S$$~~~ \}$

$=$		$\{$	assumption:  $f{\MPldom{}}\ms{1}{=}\ms{1}R{\MPldom{}}$,  $\left[\ms{2}R{\setminus}S\ms{1}{=}\ms{1}R{\setminus}(R{\MPldom{}}\ms{1}{\MPcomp}\ms{1}S)\ms{2}\right]$$~~~ \}$

Now we prove (<ref>).

$=$		$\{$	(<ref>) with $S\ms{1}{:=}\ms{1}R{\MPcomp}g$$~~~ \}$

$=$		$\{$	lemma <ref>$~~~ \}$

§.§ Difunctions

Formally,  relation $R$ is difunctional iff
\begin{equation}\label{difunctional.def}
\end{equation}
As for pers,  there are several equivalent definitions of “difunctional”, as formulated below.

For all $R$, the following statements are all equivalent.

(i)  $R$ is difunctional (i.e.  $R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R\ms{3}{\subseteq}\ms{3}R$)  ,

(ii) $R\ms{3}{=}\ms{3}R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R$  ,

(iii)$R{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}R{\setminus}R\ms{3}{=}\ms{3}R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R$  ,

(iv) $R{\MPperrdom{}}\ms{3}{=}\ms{3}R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R$  ,

(v)  $R{/}R\ms{1}{\MPcomp}\ms{1}R{\MPldom{}}\ms{3}{=}\ms{3}R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}$  ,

(vi) $R{\MPperldom{}}\ms{3}{=}\ms{3}R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}$  ,

(vii)$R\ms{3}{=}\ms{3}R\ms{1}{\cap}\ms{1}(R{\setminus}R{/}R)^{\MPrev}$  .

§.§ Provisional Orderings

There are various well-known  notions of ordering: preorder, partial and linear (aka total) ordering.  For
our purposes all of these are too strict — the fact  is that, in practice,   relations are rarely  “total” (for example, not
everyone has a sibling).  So, in this section, we introduce the notion of a “provisional
ordering”.  The adjective “provisional” has been chosen because the notion “provides” just what we need.
For later use, we state a number of properties but without proof.  All proofs can be found in the
companion working document [10].

The standard definition of an ordering is an anti-symmetric  preorder whereby a preorder is required to
be reflexive and transitive.  It is the reflexivity requirement that is too strict for our purposes.
So, with the intention of weakening  the standard definition of a preorder to requiring reflexivity of a
relation  over  some superset of its left and right domains, we propose the following definition.
Suppose  $T$ is a  homogeneous relation.     Then $T$  is said to be a
provisional  preorder   if T2⊆2T6∧6T2⊆2T6∧6TT1⊆1T  .

Fig. <ref>  depicts a provisional preorder on a set of eight elements as a directed graph.
The blue squares should be ignored for the moment.  (See the discussion following lemma
<ref>.)  Note that the relation depicted is not a preorder
because it is not reflexive:  the top-right node depicts an element that is not in the left or right domain of
the relation.

A Provisional Preorder

An immediate consequence of the definition is:
If $T$ is a provisional  preorder then $T{\MPldom{}}\ms{2}{=}\ms{2}T{\MPrdom{}}$.

A trivial property that is nevertheless used frequently:
$T$  is  a provisional  preorder equivales $T^{\MPrev}$
is  a provisional  preorder.

A preorder is a provisional preorder with left (equally right) domain equal to the identity relation.  In
other words, a preorder is a total provisional preorder.  It is easy to show that, for any relation $R$, the
relations $R{\setminus}R$ and $R{/}R$ are preorders.  It is also easy to show that $R$ is a preorder if and only if $R\ms{1}{=}\ms{1}R{\setminus}R$
(or equivalently if and only if $R\ms{1}{=}\ms{1}R{/}R$).  These properties generalise to provisional preorders.

For all relations $R$, the relations $R{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}R{\setminus}R$ and $R{/}R\ms{1}{\MPcomp}\ms{1}R{\MPldom{}}$ are provisional

$T$ is a provisional  preorder equivalesT6=6T11T∖T6=6T/T11T6=6T11T∖T/T11T  .

Lemma <ref> is sometimes used in a form where the domains are replaced by per
Suppose $T$ is a provisional  preorder.  ThenT6=6T11T∖T6=6T/T11T6=6T11T∖T/T11T  .

Suppose $T$ is a provisional  preorder.  ThenT6=6T1∩1T^6=6T  .Hence $T\ms{1}{\cap}\ms{1}T^{\MPrev}$ is a per.

Referring back to fig. <ref>, the blue squares depict the equivalence classes of the
symmetric closure of a  provisional preorder.  As remarked earlier, the depicted relation is not a
preorder; correspondingly, the blue squares depict a truly partial equivalence relation.

We assume the reader is familiar with the notions of  an ordering and a linear (or total)
ordering.   We now extend these notions to provisional orderings.   (The at-most relation on the
integers is both anti-symmetric and linear.  The at-most relation restricted to some arbitrary
subset of the  integers is an  example of a linear provisional ordering according to the definition below.)
Suppose $T$  is a homogeneous relation  of type
$A{\sim}A$, for some $A$.     Then $T$ is said to be provisionally anti-symmetric if  T1∩1T^3⊆3I_A  .Also,  $T$  is said to be a  provisional  ordering   if  $T$ is provisionally anti-symmetric and
$T$ is a provisional preorder.  Finally, $T$  is said to be a  linear provisional  ordering   if $T$ is a
provisional ordering and T1∪1T^4=4(T1∩1T^)(T1∩1T^)  .

Definition <ref> weakens the equality in the standard notion of anti-symmetry to an inclusion.  The
standard definition of  a partial ordering —an anti-symmetric preorder— is weakened accordingly (as
mentioned earlier, in order to “provide” for our needs).

The following lemma anticipates the use of provisional preorders/orderings in examples presented later.
Suppose $T$ is a provisional ordering.  ThenT5=5T1∩1T^5=5T  .

§.§ Squares and  Rectangles

We now introduce the notions  of a “rectangle” and a “square”; rectangles  are typically heterogeneous
whilst squares are, by definition, homogeneous relations.  Squares are rectangles;  properties of squares
are typically  obtained by specialising properties of rectangles.
[Rectangle and Square]   A relation $R$ is a rectangle iff  $R\ms{1}{=}\ms{1}R{\MPcomp}{\MPplattop}{\MPcomp}R$.  A relation $R$
is a square iff $R$ is a symmetric rectangle.

It is easily shown that a rectangle is a difunction and a square is a per.

§.§ Isomorphic Relations

The (yet-to-be-defined) cores and indexes of a given relation are not unique; in common mathematical
jargon, they are unique “up to isomorphism”.  In order to make this precise, we need to define the
notion of isomorphic relation and establish a number of properties.
Suppose $R$ and $S$ are two relations (not necessarily of the same type).  Then we say
that $R$ and $S$ are isomorphic and write $R\ms{1}{\cong}\ms{1}S$ iff

$:$	$\phi\ms{1}{\MPcomp}\ms{1}\phi^{\MPrev}\ms{2}{=}\ms{2}R{\MPldom{}}\ms{5}{\wedge}\ms{5}\phi^{\MPrev}\ms{1}{\MPcomp}\ms{1}\phi\ms{2}{=}\ms{2}S{\MPldom{}}\ms{5}{\wedge}\ms{5}\psi\ms{1}{\MPcomp}\ms{1}\psi^{\MPrev}\ms{2}{=}\ms{2}R{\MPrdom{}}\ms{5}{\wedge}\ms{5}\psi^{\MPrev}\ms{1}{\MPcomp}\ms{1}\psi\ms{2}{=}\ms{2}S{\MPrdom{}}$

$:$	$R\ms{2}{=}\ms{2}\phi\ms{1}{\MPcomp}\ms{1}S\ms{1}{\MPcomp}\ms{1}\psi^{\MPrev}$

§ INDEXES AND CORE RELATIONS

This section introduces the notions of “index” and “core” of a relation and records some of their
properties. An “index” is a special case of a “core” of a relation but, in general, it is more useful.  For a
detailed account of their properties (including proofs)  see [10, 11].

§.§ Definitions

The definition of an “index” of a relation is as follows.
[Index]   An index of a relation $R$ is a relation $J$ that  has the following properties:

Indexes are a special case of what we call “core” relations.
[Core]   Suppose $R$ is an arbitrary relation and suppose $C$ is a relation
such that C4=4λ11R11ρ^for some relations $\lambda$ and $\rho$ satisfying  R3=3λ^11λ7∧7λ2=2λ11λ^7∧7R3=3ρ^11ρ7∧7ρ2=2ρ11ρ^  .Then $C$ is said to be a core of  $R$ as witnessed by $\lambda$ and $\rho$.

Note particularly requirement <ref>(a).  A consequence of this requirement is that an index of a
relation has the same type as the relation, which is not necessarily the case for cores.

An index $J$ of a  relation $R$  is a core of the relation as witnessed by $J{\MPldom{}}\ms{1}{\MPcomp}\ms{1}R{\MPperldom{}}$ and $J{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}R{\MPperrdom{}}$.

The property that is common to cores and indexes  is captured by the following definition.
[Core Relation]   A relation $R$ is a core relation  iff $R{\MPldom{}}\ms{1}{=}\ms{1}R{\MPperldom{}}$ and $R{\MPrdom{}}\ms{1}{=}\ms{1}R{\MPperrdom{}}$.

We exploit the fact that both indexes and cores satisfy definition <ref> later.  (The proof of this fact in
[10] assumes that $R$ has an index.  The —much less straightforward— proof without this
assumption is given in [6].)

A number of properties of cores and indexes are needed below.  Suppose $C$ is a core of $R$ as witnessed by
$\lambda$ and $\rho$.   Then

\begin{equation}\label{core.equn}
\end{equation}

\begin{equation}\label{core.domains}
\end{equation}
Suppose $J$ is an index of $R$.  Then

\begin{equation}\label{R-perleft}
\end{equation}

§.§ Indexes of Pers

A relation $R$ is a per iff $R\ms{1}{=}\ms{1}R{\MPperldom{}}\ms{1}{=}\ms{1}R{\MPperrdom{}}$.  Using this property, the definition of index can be simplified for pers.

[Index of a Per]   Suppose $P$ is a per.  Then a (coreflexive)
index of $P$ is a relation $J$ such  that

To our axiom system we add the  postulate that every per has a coreflexive index.
We call this the axiom of choice.
[Axiom of Choice]   Every per has a coreflexive  index.

Assuming our axiom of choice, it follows that every relation has an index.  Specficially, we have:
Suppose  $J$ and $K$ are (coreflexive)  indices of $R{\MPperldom{}}$ and
$R{\MPperrdom{}}$, respectively.  Then $J{\MPcomp}R{\MPcomp}K$ is an index of $R$.

It is also the case that Freyd and Ščedrov's  [13] so-called “splittings” of pers always exist.
If per $P$  has a coreflexive index $J$ , thenP4=4(JP)^11(JP)8∧8J4=4(JP)11(JP)^  .Thus, assuming the  axiom of choice,   for all relations $R$,𝗉𝖾𝗋.R5≡5⟨∃f3:3f11f^3=3f3:3R2=2f^11f⟩  .

The property that $R$ is a difunction is equivalent to  $R{\MPperldom{}}\ms{2}{=}\ms{2}R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}$  (and symmetrically to  $R{\MPperrdom{}}\ms{2}{=}\ms{2}R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R$).
Also, since $R\ms{2}{=}\ms{2}R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R$,  the
definition of an index of a difunction can be restated as follows.
[Difunction Index]   An index  of a difunction $R$ is a relation $J$ that  has the following properties:

In the same way that pers are characterised by a single function $f$ —see theorem <ref>—
difunctions are characterised by a pair of functions $f$ and $g$:
Assuming the axiom of choice (axiom <ref>),  for all relations $R$,𝖽𝗂𝖿𝗎𝗇𝖼𝗍𝗂𝗈𝗇.R5≡5⟨∃1f,g3:3f11f^3=3f3=3g11g^3=3g3:3R2=2f^11g⟩  .

§ THE DIAGONAL

This section  anticipates the study of block-ordered relations

introduce the notion of  the “diagonal” of a relation in section  <ref> and formulate
some basic properties in section <ref>.

§.§ Definition and Examples

Straightforwardly from the definition of factors, properties of converse  and set intersection,
\begin{equation}\label{difun.delta}
R\mbox{ is difunctional\ms{8}}{\equiv}\ms{8}R\ms{3}{=}\ms{3}R\ms{1}{\cap}\ms{1}(R{\setminus}R{/}R)^{\MPrev}~~.
\end{equation}
More generally, we have:
For all $R$,   $R\ms{1}{\cap}\ms{1}(R{\setminus}R{/}R)^{\MPrev}$ is difunctional.

Proof   Let $S$ denote $R\ms{1}{\cap}\ms{1}(R{\setminus}R{/}R)^{\MPrev}$.  We have to prove that $S$ is difunctional.  That is, by definition,S11S^11S3⊆3S  .Since the right side is an intersection, this is equivalent to S11S^11S3⊆3R6∧6S11S^11S3⊆3(R∖R/R)^  .The first is (almost) trivial:

$\subseteq$		$\{$	$S\ms{1}{\subseteq}\ms{1}R$, $S\ms{1}{\subseteq}\ms{1}(R{\setminus}R{/}R)^{\MPrev}$,

converse,  monotonicity$~~~ \}$

$\subseteq$		$\{$	cancellation$~~~ \}$

In the above calculation, the trick was to replace the outer occurrences of $S$ on the left side by $R$ and the
middle occurrence by $(R{\setminus}R{/}R)^{\MPrev}$.  The replacement is done the opposite way around in the second

$\Leftarrow$		$\{$	$S\ms{1}{\subseteq}\ms{1}(R{\setminus}R{/}R)^{\MPrev}$, $S\ms{1}{\subseteq}\ms{1}R$,  monotonicity and transitivity$~~~ \}$

$=$		$\{$	converse$~~~ \}$

$=$		$\{$	Galois connection$~~~ \}$

$=$		$\{$	cancellation,  monotonicity and transitivity$~~~ \}$

We call the relation $R\ms{1}{\cap}\ms{1}(R{\setminus}R{/}R)^{\MPrev}$ the
diagonal of $R$;  Riguet [20] calls it the “différence”.  (Riguet's definition does
not use factors but  is equivalent.; indeed, rewriting the definition using
(<ref>) the diagonal of $R$ is the “différence” of $R$ and $R^{\MPrev}\ms{1}{\MPcomp}\ms{1}{\neg}R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}$.)
[Diagonal]   The diagonal of relation $R$ is the relation $R\ms{1}{\cap}\ms{1}(R{\setminus}R{/}R)^{\MPrev}$.
For brevity,  $R\ms{1}{\cap}\ms{1}(R{\setminus}R{/}R)^{\MPrev}$ will  be denoted by $\Delta{}R$.

Many readers will be familiar with the decomposition of a preorder into a partial ordering on a set of
equivalence classes.  The diagonal of a preorder $T$  is the  equivalence relation $T\ms{1}{\cap}\ms{1}T^{\MPrev}$.  More

The diagonal of a provisional preorder $T$ is $T\ms{1}{\cap}\ms{1}T^{\MPrev}$.  This is because,
for an arbitrary relation $T$,  T1∩1(T∖T/T)^7=7T3∩3T11(T∖T/T)^11T  .But,  if $T$ is a provisional preorder,  T11(T∖T/T)^11T5=5T^  .(See lemmas <ref> and  <ref>.)

A particular instance of example <ref> is if   $G$ is the edge
relation of a finite  graph.  Then $\Delta(G^{*})$ is $G^{*}\ms{1}{\cap}\ms{1}(G^{\MPrev})^{*}$, the relation that holds between nodes $a$ and $b$ if there
is a path from $a$ to $b$ and a path from $b$ to $a$ in the graph.     Thus $\Delta(G^{*})$  is the equivalence relation that
holds between nodes that are in the same strongly  connected  component of $G.$

In this example, we consider three versions of the less-than relation: the
homogeneous less-than relation on integers, which we denote by ${<}_{\MPInt}$,  the homogeneous less-than
relation  on real numbers, which we denote by ${<}_{\MPReal}$, and the heterogeneous less-than relation on integers
and real numbers, which we denote by ${}_{\MPInt}{<}_{\MPReal}$.    Specifically, the relation ${}_{\MPInt}{<}_{\MPReal}$ relates integer $m$ to real
number $x$ when  $m\ms{1}{<}\ms{1}x$  (using the conventional over-loaded notation).  We also subscript the at-most
symbol ${\leq}$ in the same way in order to indicate the type of the relation in question.

The diagonal of the less-than relation on integers is the predecessor
relation (i.e. it relates integer $m$ to integer $n$ exactly when $n\ms{1}{=}\ms{1}m{+}1$).
This is because ${<}_{\MPInt}{\setminus}{<}_{\MPInt}\ms{2}{=}\ms{2}{\leq}_{\MPInt}$,   and ${\leq}_{\MPInt}{/}{<}_{\MPInt}$ relates integer $m$ to integer $n$ exactly when $m\ms{1}{\leq}_{\MPInt}\ms{1}n{+}1$ (where
the subscript $\MPInt$ indicates the type of the ordering).  The diagonal is thus functional and injective.

The diagonal of the less-than  relation on real numbers is the empty relation.  This is because
${<}_{\MPReal}{\setminus}{<}_{\MPReal}\ms{2}{=}\ms{2}{\leq}_{\MPReal}$,   ${\leq}_{\MPReal}{/}{<}_{\MPReal}\ms{2}{=}\ms{2}{\leq}_{\MPReal}$  and ${<}_{\MPReal}\ms{1}{\cap}\ms{1}{\geq}_{\MPReal}\ms{1}{=}\ms{1}{\MPplatbottom}_{\MPReal}$.  (Again, the subscript indicates the type of the ordering.)

The diagonal of the heterogeneous less-than relation ${}_{\MPInt}{<}_{\MPReal}$ relates integer $m$ to real number $x$ when
$m\ms{1}{<}\ms{1}x\ms{1}{\leq}\ms{1}m{+}1$.  This is equivalent to $\lceil{}x\rceil\ms{1}{=}\ms{1}m{+}1$.   The diagonal  is thus a difunctional relation characterised
by   —in the sense of theorem <ref>— the  ceiling function ${\left\langle{}x\ms{1}{:}{:}\ms{1}\lceil{}x\rceil\right\rangle}$  and the successor function

The following example introduces a general mechanism for constructing illustrative examples of the
concepts introduced later.  The example exploits the observation that $\Delta{}R$ is injective if the preorder $R{\setminus}R$
is anti-symmetric; that is, $\Delta{}R$ is injective if $R{\setminus}R$ is a partial ordering.  (Equivalently, $\Delta{}R$ is functional if
$R{/}R$ is a partial ordering.)  We leave the straightforward proof to the reader.
Suppose $\mathcal{X}$ is a finite type.  We use dummy $x$ to range over
elements of type $\mathcal{X}$.   Let $\mathcal{S}$ denote a subset of $2^{\mathcal{X}}$.
Let $\mathsf{in}$ denote the membership relation of type $\mathcal{X}{\sim}\mathcal{S}$.  That is, if   $S$ is a subset of  $\mathcal{S}$,  $x{\MPcomp}{\MPplattop}{\MPcomp}S\ms{1}{\subseteq}\ms{1}\mathsf{in}$ exactly
when $x$ is an element of the set $S$.   The relation $\mathsf{in}{\setminus}\mathsf{in}$ is the subset relation of type $\mathcal{S}{\sim}\mathcal{S}$.

(Conventionally,  $\mathsf{in}$ is denoted by the
symbol “${\in}$” and one writes $x{\in}S$ instead of $x{\MPcomp}{\MPplattop}{\MPcomp}S\ms{1}{\subseteq}\ms{1}\mathsf{in}$.  Also, the relation $\mathsf{in}{\setminus}\mathsf{in}$ is conventionally denoted by
the symbol “${\subseteq}$”.  That is,  if $S$ and $S'$ are both elements of $\mathcal{S}$,   $S{\MPcomp}{\MPplattop}{\MPcomp}S'\ms{1}{\subseteq}\ms{1}\mathsf{in}{\setminus}\mathsf{in}$  exactly when $S\ms{1}{\subseteq}\ms{1}S'$.
Were we to adopt conventional practice, the
overloading  of the notation that occurs is  likely to cause confusion, so we choose to avoid it.)

The relation $\mathsf{in}{\setminus}\mathsf{in}$ is anti-symmetric.  As a consequence, $\Delta\mathsf{in}$ is injective.  (Equivalently,  $(\Delta\mathsf{in})^{\MPrev}$ is
functional.)  Specifically, for all $x$ of type $\mathcal{X}$ and $S$ of type $\mathcal{S}$, xS2⊆2Δ𝗂𝗇6≡6xS1⊆1𝗂𝗇3∧3⟨∀S'2:2xS'1⊆1𝗂𝗇2:2SS'1⊆1𝗂𝗇∖𝗂𝗇⟩  ,where dummy $S'$ ranges over elements of $\mathcal{S}$.   Using conventional notation, the right side of this equation is
recognised as the definition of a minimum, and  one might writex2Δ𝗂𝗇2S7≡7S22⟨𝖬𝖨𝖭1S'1:1x∈S'1:1S'⟩where  the venturi tube “$\tuberight$” indicates an equality assuming the well-definedness of the expression on its
right side.

Diagonal of an Instance of the Membership Relation

Fig. <ref> shows a particular instance.  The set $\mathcal{X}$ is the set of numbers from $0$ to $3$.  The
set $\mathcal{S}$ is a subset of $2^{\{0{,}1{,}2{,}3\}}$; the chosen subset and the  relation $\mathsf{in}{\setminus}\mathsf{in}$ for this choice are depicted by  the
directed graph  forming the central portion of fig. <ref>.  The relation $\Delta\mathsf{in}$ of type $\mathcal{X}\ms{1}{\sim}\ms{1}\mathcal{S}$ is
depicted by the undirected graph whereby  the atoms of the relation are depicted as rectangles.  Note
that the numbers  $0$ and $3$  are  not related by $\Delta\mathsf{in}$ to any of the elements of $\mathcal{S}$.

§.§ Basic Properties

Primarily for notational convenience, we note a simple property of the diagonal:
(ΔR)^4=4Δ(R^)  .

$=$		$\{$	definition and distributivity$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	definition$~~~ \}$

A consequence of lemma <ref> is that we can write $\Delta{}R^{\MPrev}$ without ambiguity.  This we do from now

Very straightforwardly,  the relation  $R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}$ is a per if $R$ is difunctional.  For a difunctional relation $R$,
the relation $R\ms{1}{\MPcomp}\ms{1}R^{\MPrev}$ is the left per domain of $R$.  (Symmetrically, $R^{\MPrev}\ms{1}{\MPcomp}\ms{1}R$ is the right per
domain of $R$.  See theorem <ref>, parts (iv) and (vi).)
Thus $\Delta{}R\ms{1}{\MPcomp}\ms{1}(\Delta{}R)^{\MPrev}$ is the left per domain of  the diagonal of $R$.
The following lemma is the basis of the construction,  in certain cases,  of an economic representation
of the diagonal of $R$ and, hence,  of $R$ itself.

For all relations $R$, (ΔR)5=5(ΔR)11R5=5R11(ΔR)  .Dually,(ΔR)5=5R11(ΔR)5=5(ΔR)11R  .

Proof   We prove the first equation by mutual inclusion.  First,

$=$		$\{$	$\Delta{}R$ is difunctional, theorem <ref>;  definition:  (<ref>)$~~~ \}$

$\Leftarrow$		$\{$	domains and monotonicity$~~~ \}$

$=$		$\{$	definition of $R\leftsymdivision{}R$,  converse and factors$~~~ \}$

$=$		$\{$	$\Delta{}R\ms{1}{\subseteq}\ms{1}R$;  $\Delta{}R^{\MPrev}\ms{1}{\subseteq}\ms{1}R{\setminus}R{/}R$ and cancellation$~~~ \}$

$=$		$\{$	$\Delta{}R$ is difunctional,  theorem <ref>$~~~ \}$

$\Leftarrow$		$\{$	domains and definition:  (<ref>)$~~~ \}$

$\Leftarrow$		$\{$	monotonicity and converse$~~~ \}$

$=$		$\{$	definition of diagonal$~~~ \}$

$\Leftarrow$		$\{$	$\Delta{}R\ms{1}{\subseteq}\ms{1}R$ ;  converse $~~~ \}$

$=$		$\{$	cancellation; factors$~~~ \}$

$\Leftarrow$		$\{$	cancellation  and  $\Delta{}R^{\MPrev}\ms{1}{\subseteq}\ms{1}R{\setminus}R{/}R$$~~~ \}$

$=$		$\{$	cancellation$~~~ \}$

The remaining three  equalities are  simple consequences of the properties of converse, pers and

The following  corollary  of lemma <ref> proves to be crucial later:

For all relations $R$,   (ΔR)3=3R6≡6(ΔR)2=2R  .Dually,(ΔR)3=3R6≡6(ΔR)2=2R  .

Proof   The proof is by mutual implication:

$\Rightarrow$		$\{$	lemma <ref> and Leibniz$~~~ \}$

$=$		$\{$	dual of (<ref>)$~~~ \}$

$\Rightarrow$		$\{$	Leibniz$~~~ \}$

$=$		$\{$	dual of (<ref>) with $R\ms{1}{:=}\ms{1}\Delta{}R$ and $R\ms{1}{:=}\ms{1}R$$~~~ \}$

§.§ Reduction to the Core

In this section our goal is to prove that if $J$ is an index of relation $R$ then $\Delta{}J$ is an index of $\Delta{}R$.
Instantiating definition <ref> with $J{,}R\ms{1}{:=}\ms{1}\Delta{}J{,}\Delta{}R$the properties we have to prove are as follows.

Of these, the hardest to prove is (b).  For properties (a), (c) and (d), all we need is that $J$ is an arbitrary
index of $R$.  For property (b), we use the fact that
an index of an arbitrary relation $R$ is defined to be $J{\MPcomp}R{\MPcomp}K$ where $J$ is an index of $R{\MPperldom{}}$ and $K$ is an index of

We begin with the easier properties.
Suppose $J$ is an index of $R$. Then ΔJ1⊆1ΔR  .

$=$		$\{$	definition <ref>$~~~ \}$

$=$		$\{$	domains$~~~ \}$

$\Leftarrow$		$\{$	$J$ is an index of $R$, so $J\ms{1}{\subseteq}\ms{1}R$; monotonicity$~~~ \}$

$=$		$\{$	converse$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	$J$ is an index of $R$, definition <ref>(b); per domains$~~~ \}$

$\Leftarrow$		$\{$	monotonicity$~~~ \}$

Continuing with the left side of the inclusion:

$=$		$\{$	domains$~~~ \}$

$=$		$\{$	$J$ is an index of $R$; definition <ref>(c) and (d)$~~~ \}$

$\subseteq$		$\{$	domains and cancellation$~~~ \}$

$\subseteq$		$\{$	$J$ is an index of $R$; definition <ref>(a)$~~~ \}$

Suppose $J$ is an index of $R$.   Then (ΔJ)22ΔR22ΔR^22(ΔJ)6=6(ΔJ)  .Dually, (ΔJ)22ΔR^22ΔR22(ΔJ)6=6(ΔJ)  .

$=$		$\{$	$\Delta{}R$ is a difunction, theorem <ref>$~~~ \}$

$=$		$\{$	lemma <ref> (and symmetry)$~~~ \}$

$=$		$\{$	by lemma <ref> and monotonicity,  $(\Delta{}J){\MPldom{}}\ms{1}{\subseteq}\ms{1}(\Delta{}R){\MPldom{}}$$~~~ \}$

$=$		$\{$	$(\Delta{}J){\MPldom{}}\ms{1}{\subseteq}\ms{1}J{\MPldom{}}$ (since $\Delta{}J\ms{1}{\subseteq}\ms{1}J$)$~~~ \}$

$=$		$\{$	$J$ is an index of $R$,  definition <ref>(c)$~~~ \}$

$=$		$\{$	$(\Delta{}J){\MPldom{}}\ms{1}{\subseteq}\ms{1}J{\MPldom{}}$ (since $\Delta{}J\ms{1}{\subseteq}\ms{1}J$)$~~~ \}$

In order to prove (b), we prove a more general theorem on cores.  First, a lemma:
Suppose $R$,  $C$,   $\lambda$ and $\rho$ are as in definition  <ref>.  Then  R11R∖R/R11R5=5ρ^11C∖C/C11λ  .

$=$		$\{$	(<ref>)$~~~ \}$

$=$		$\{$	$R{\MPperldom{}}\ms{3}{=}\ms{3}\lambda^{\MPrev}\ms{1}{\MPcomp}\ms{1}\lambda$,   $R{\MPperrdom{}}\ms{3}{=}\ms{3}\rho^{\MPrev}\ms{1}{\MPcomp}\ms{1}\rho$, and domains$~~~ \}$

$=$		$\{$	(<ref>)$~~~ \}$

$=$		$\{$	lemma <ref> with $f{,}g{,}U{,}V{,}W\ms{1}{:=}\ms{1}\rho{,}\lambda{,}C{,}C{,}C$$~~~ \}$

$=$		$\{$	$C\ms{2}{=}\ms{2}\lambda\ms{1}{\MPcomp}\ms{1}R\ms{1}{\MPcomp}\ms{1}\rho^{\MPrev}$; so $\lambda{\MPldom{}}\ms{1}{\MPcomp}\ms{1}C\ms{2}{=}\ms{2}C\ms{2}{=}\ms{2}C\ms{1}{\MPcomp}\ms{1}\rho{\MPldom{}}$$~~~ \}$

Suppose $R$, $C$,   $\lambda$ and $\rho$ are as in definition <ref>.  Then ΔR4=4λ^11ΔC11ρ8∧8ΔC4=4λ11ΔR11ρ^  .In  words, if $\lambda$ and $\rho$ witness that $C$ is a core of $R$, then $\lambda$ and $\rho$ witness that $\Delta{}C$ is a core of $\Delta{}R$.

$=$		$\{$	definition $~~~ \}$

$=$		$\{$	domains and converse$~~~ \}$

$=$		$\{$	lemma <ref>$~~~ \}$

$=$		$\{$	straightforwardly)  $R\ms{4}{=}\ms{4}\lambda^{\MPrev}\ms{1}{\MPcomp}\ms{1}C\ms{1}{\MPcomp}\ms{1}\rho$$~~~ \}$

$=$		$\{$	distributivity of converse and  functional relations$~~~ \}$

$=$		$\{$	definition <ref>$~~~ \}$

$=$		$\{$	above$~~~ \}$

$=$		$\{$	$\lambda$ and $\rho$ are functional$~~~ \}$

$=$		$\{$	$\Delta{}C\ms{1}{\subseteq}\ms{1}C$;  so  $(\Delta{}C){\MPldom{}}\ms{2}{\subseteq}\ms{2}C{\MPldom{}}$ and $(\Delta{}C){\MPrdom{}}\ms{2}{\subseteq}\ms{2}C{\MPrdom{}}$

(<ref>) and domains$~~~ \}$

We are now in a position to prove the final property (b) above.
Suppose $J$ is an index of $R$.   Then ΔR11ΔJ^11ΔR3=3ΔR  .

Proof   We begin by noting that theorem  <ref> applies with $C$ instantiated to $J$ and
$\lambda$ and $\rho$ defined by $\lambda\ms{2}{=}\ms{2}J{\MPldom{}}\ms{1}{\MPcomp}\ms{1}R{\MPperldom{}}$ and $\rho\ms{2}{=}\ms{2}J{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}R{\MPperrdom{}}$.  This is because $J$ is a core of $R$.  So

$=$		$\{$	theorem  <ref> with $C{,}\lambda{,}\rho\ms{3}{:=}\ms{3}J\ms{2}{,}\ms{2}J{\MPldom{}}\ms{1}{\MPcomp}\ms{1}R{\MPperldom{}}\ms{2}{,}\ms{2}J{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}R{\MPperrdom{}}$$~~~ \}$

$=$		$\{$	converse$~~~ \}$

$=$		$\{$	definition of $\rho$ and $\lambda$,  $(J{\MPldom{}}\ms{1}{\MPcomp}\ms{1}R{\MPperldom{}})^{\MPrev}\ms{2}{=}\ms{2}R{\MPperldom{}}\ms{1}{\MPcomp}\ms{1}J{\MPldom{}}$$~~~ \}$

$=$		$\{$	per domains$~~~ \}$

$=$		$\{$	 lemma <ref>$~~~ \}$

$=$		$\{$	lemma <ref>$~~~ \}$

$=$		$\{$	lemma <ref>$~~~ \}$

$=$		$\{$	per domains$~~~ \}$

$=$		$\{$	$\Delta{}R$ is difunctional, theorem <ref>$~~~ \}$

Putting all the lemmas together, we have:
Suppose $J$ is an index of $R$.   Then
$\Delta{}J$ is an index of $\Delta{}R$.

Proof   Lemmas <ref>,  <ref> and
<ref>  combined with definition <ref> (instantiated with $J{,}R\ms{1}{:=}\ms{1}\Delta{}J{,}\Delta{}R$).

We conclude with a beautiful theorem.

Suppose $J$ is an index of $R$.   ThenΔJ3=3J11ΔR11J9∧9ΔR3=3R11ΔJ11R  .

Proof   We first prove, by mutual implication, that the two equations are equivalent.  Assume thatΔR4=4R11ΔJ11R  .Then,

$=$		$\{$	assumption$~~~ \}$

$=$		$\{$	$\Delta{}J\ms{1}{\subseteq}\ms{1}J$, so $(\Delta{}J){\MPldom{}}\ms{1}{\subseteq}\ms{1}J{\MPldom{}}$ and $(\Delta{}J){\MPrdom{}}\ms{1}{\subseteq}\ms{1}J{\MPrdom{}}$; domains$~~~ \}$

$=$		$\{$	$J$ is an index of $R$,  definition <ref>(c) and (d)$~~~ \}$

$=$		$\{$	reverse of middle step$~~~ \}$

Conversely, assumeΔJ2=2J11ΔR11J  .Then,

$=$		$\{$	assumption$~~~ \}$

$=$		$\{$	lemma <ref>$~~~ \}$

$=$		$\{$	lemma <ref> and domains$~~~ \}$

$=$		$\{$	definition <ref>(c) and <ref>(d)$~~~ \}$

$=$		$\{$	lemma <ref>  and domains$~~~ \}$

Combining the two calculations,  the two equations are equivalent
and, therefore, it  suffices to prove just one of them[It is not necessary to prove the
equivalence of the two statements in order to prove the theorem; we could have omitted the second
calculation.   But some redundancy in proofs
enhances their reliability.].  We prove the second by mutual inclusion:

$=$		$\{$	$\Delta{}R$ is difunctional$~~~ \}$

$=$		$\{$	lemma <ref>, converse$~~~ \}$

$=$		$\{$	$\Delta{}R$ is difunctional, theorem <ref>(iv) and (vi)$~~~ \}$

$=$		$\{$	lemma <ref>$~~~ \}$

$\subseteq$		$\{$	domains are coreflexive$~~~ \}$

$\subseteq$		$\{$	lemma <ref> and monotonicity$~~~ \}$

$=$		$\{$	lemma <ref>, domains$~~~ \}$

§ BLOCK-ORDERED RELATIONS

In general, dividing a subset of a set $A$ into blocks
is formulated by specifying a functional relation  $f$, say, with source[In
the terminology we use, a
relation  of type $A{\sim}B$  has target $A$ and source $B$.] the set $A$;
elements $a0$ and $a1$ are in the same block equivales  $f{.}a0$ and $f{.}a1$ are both defined and  $f{.}a0\ms{1}{=}\ms{1}f{.}a1$.
In mathematical terminology, a functional relation $f$ defines the  partial equivalence relation $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}f$ and
the  “blocks” are the equivalence classes of $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}f$.  (Partiality means that some elements may not be in an
equivalence class.)

Given functional relations  $f$ and $g$ with sources $A$ and $B$, respectively, and equal  left  domains,   relation
$R$ of type $A{\sim}B$ is said to be block-structured by $f$ and $g$ if there is a relation $S$  such that $R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}S\ms{1}{\MPcomp}\ms{1}g$.
Informally, whether or not $a$ and $b$ are related by $R$ depends entirely on the “block” $(f{.}a\ms{1},\ms{1}g{.}b)$ to which
they belong.  Note that it is not required that $f$ and $g$ be total functions: it suffices that $f{\MPrdom{}}\ms{1}{=}\ms{1}R{\MPldom{}}$ and $g{\MPrdom{}}\ms{1}{=}\ms{1}R{\MPrdom{}}$.
The type of $S$ is  $C{\sim}C$ where $C$ includes   $\{a{:}\ms{3}a\ms{1}{\MPcomp}\ms{1}f{\MPrdom{}}\ms{2}{=}\ms{2}a{:}\ms{3}f{.}a\}$ (equally $\{b{:}\ms{3}b\ms{1}{\MPcomp}\ms{1}f{\MPrdom{}}\ms{2}{=}\ms{2}b{:}\ms{3}g{.}b\}$).
[Block-Ordered Relation]
Suppose $T$ is  a relation of type $C{\sim}C$,   $f$ is a   relation of  type $C{\sim}A$   and $g$ is a   relation
of type   $C{\sim}B$.   Suppose further that  $T$ is  a provisional ordering and
that $f$ and $g$ are functional and onto the domain of $T$.  That is, suppose
\begin{equation}\label{def:Block-Ordered Relationfg}
\end{equation}
Then we say that the relation   $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$ is a block-ordered relation.   A relation $R$ of
type $A{\sim}B$ is said to be block-ordered by $f$, $g$ and $T$ if $R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$  and
$f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$ is a block-ordered relation.

The archetypical   example of a block-ordered relation is
a   preorder.   Informally, if  $R$ is a preorder,  its  symmetric closure     $R\ms{1}{\cap}\ms{1}R^{\MPrev}$   is an equivalence relation,
and the relation $R$ defines a partial  ordering on the equivalence classes.   Equivalently,  if a representative element
is chosen for each equivalence class, the relation $R$ is a partial ordering on the representatives.
Theorem <ref>  makes this precise.

Suppose $T$ is a provisional preorder  and suppose $J$ is a (coreflexive) index of
$T{\MPperldom{}}$.  Then $J{\MPcomp}T{\MPcomp}J$ is an index of $T$ and is a provisional ordering.  Hence,  $T$ is a
block-ordered relation.

Proof   That $J{\MPcomp}T{\MPcomp}J$ is an index of $T$ is the combination of lemma <ref> and
theorem <ref>.  It is a provisional preorder because $T$ is a preorder and $J$ is coreflexive.
So, it remains to show that $J{\MPcomp}T{\MPcomp}J$ is provisionally anti-symmetric.  That is, we must show that

$=$		$\{$	$J$ is coreflexive, distributivity$~~~ \}$

$\subseteq$		$\{$	<ref>$~~~ \}$

$=$		$\{$	$J$ is an index of $T{\MPperldom{}}$, definition  <ref>(b) with $P\ms{1}{:=}\ms{1}T{\MPperldom{}}$$~~~ \}$

$\subseteq$		$\{$	$J$ is coreflexive$~~~ \}$

Identifying a block-ordering  of a  relation —if it exists— is important for efficiency.    Although a
relation is defined to be a set of pairs, relations —even relations on finite sets— are rarely stored as such;
instead some base set of pairs is stored and an algorithm used to generate, on demand, additional
information about the relation.  This is particularly so of ordering relations.  For example, a test $m\ms{1}{<}\ms{1}n$ on
integers $m$ and $n$ in a computer program is never implemented as a table lookup; instead an algorithm is
used to infer from the basic relations  $0\ms{1}{<}\ms{1}1$ together with the internal  representation of $m$ and $n$ what the
value of the test is.  In the case of block-structured relations,  functional relations  $f$ and $g$  define partial
equivalence relations $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}f$ and $g^{\MPrev}\ms{1}{\MPcomp}\ms{1}g$ on their respective sources.  (The relations $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}f$ and  $g^{\MPrev}\ms{1}{\MPcomp}\ms{1}g$ are
partial because $f$ and $g$ are not required to be total.)  Combining the functional relations  with an
ordering relation on their  (common) target is an effective way of implementing a  relation
(assuming the ordering relation is also implemented effectively).

Suppose $G$ is the edge relation of a finite graph.   The
relation $G^{*}$ is, of course, a preorder and so is block-ordered.  The block-ordering of $G^{*}$  given by theorem
<ref>  is, however, not very useful.  For practical
purposes a block-ordering constructed from  $G$ (rather than $G^{*}$) is preferable.   Here we outline how this is

Recall from example <ref>, that the diagonal $\Delta(G^{*})$ is the relation $G^{*}\ms{1}{\cap}\ms{1}(G^{\MPrev})^{*}$
and that this  is an equivalence relation on the nodes of $G$, whereby the equivalence classes are
the strongly connected components of $G$.  Let $N$ denote the nodes of $G$ and $C$ denote the set of strongly
connected components  of $G.$  By theorem <ref>,  there is a function $\mathsf{sc}$ of  type $C{\leftarrow}N$ such that
\begin{equation}\label{bd:sc.partition}
\end{equation}
The relation $\mathcal{A}$ defined by 𝗌𝖼11G11𝗌𝖼^4∩4I_Cis a homogeneous relation on the strongly connected components of $G$, i.e. a relation of type $C{\sim}C$.
Informally, it is a graph obtained from the graph $G$ by coalescing the nodes in a strongly connected
component of $G$ into a single node whilst retaining the edges of $G$ that connect nodes in distinct strongly
connected components.   A fundamental  theorem is  that
\begin{equation}\label{bd:SCgraph1}
\end{equation}
Moreover,  $\mathcal{A}$ is acyclic.   That is,
\begin{equation}\label{bd:SCgraph2}
\end{equation}
(See [8, 7] for the  details of the proof of (<ref>) and (<ref>). In fact
the theorem is valid for all relations $G$; finiteness is not required.)

The relation $\mathcal{A}^{*}$ is, of course,  transitive.  It is also reflexive;  combined with its acyclicity, it follows that
\begin{equation}\label{bd:acyclic.equiv.defs}
\mathcal{A}^{*}\ms{1}{\cap}\ms{1}(\mathcal{A}^{*})^{\MPrev}\ms{4}{=}\ms{4}I_{C}~~.
\end{equation}
That is, $\mathcal{A}^{*}$ is a (total) provisional ordering on $C.$    The conclusion is that $G^{*}$ is
block-ordered by $\mathsf{sc}$, $\mathsf{sc}$ and $\mathcal{A}^{*}$.

Informally, a finite graph can always be decomposed into its strongly connected components together
with an acyclic graph connecting the components.

Although the informal interpretation of this theorem is well-known,  the  formal proof is non-trivial.
Although not formulated in the same way, it is essentially the “transitive reduction” of an arbitrary (not
necessarily acyclic) graph formulated by Aho, Garey and Ullman  <cit.>.

The  decomposition (<ref>)  is (implicitly)  exploited when computing
the inverse $\mathbf{A}^{{-}1}$ of a real matrix $\mathbf{A}$ in order to minimise storage requirements: using an elimination
technique, a so-called “product form” is computed for each strongly connected component, whilst the
process of “forward substitution” is applied to the acyclic-graph structure.

Theorem <ref> makes precise the statement that block orderings —where they exist—
are unique “up to isomorphism”.
Suppose $T$ is  a provisional ordering.
Suppose also that $f$ and $g$ are functional and onto the domain of $T$.  That is, suppose f11f^4=4f4=4T1∩1T^4=4g4=4g11g^  .Suppose further[The types of $T$ and $S$ may be different.  The types of $f$ and $h$, and of $g$ and $k$ will then also be
different.  As in lemma <ref>, the
requirement is that the types are compatible with the type restrictions on the
operators in all assumed properties.
The symbol “$I$” in (<ref>) is overloaded: if the type of $T$ is $A{\sim}A$ and the type of $S$ is
$B{\sim}B$,  $\phi\ms{1}{\MPcomp}\ms{1}\phi^{\MPrev}$ has type $A{\sim}A$ and $\phi^{\MPrev}\ms{1}{\MPcomp}\ms{1}\phi$ has type $B{\sim}B$.]
that $S$,  $h$  and $k$  satisfy the same properties as  $T$, $f$ and $g$ (respectively) and that
\begin{equation}\label{BD.fRSg}
\end{equation}
\begin{equation}\label{BD.provorder.dom.theo}
\end{equation}

\begin{equation}\label{BD.provorder.fghk}
\end{equation}

\begin{equation}\label{BD.provorder.fgRShk}
f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T^{\MPrev}\ms{1}{\MPcomp}\ms{1}g\ms{4}{=}\ms{4}h^{\MPrev}\ms{1}{\MPcomp}\ms{1}S^{\MPrev}\ms{1}{\MPcomp}\ms{1}k\mbox{~~, and}
\end{equation}

\begin{equation}\label{BD.provorder.fhgk}
\end{equation}
Also,  letting $\phi$ denote $f\ms{1}{\MPcomp}\ms{1}h^{\MPrev}$ (equally, by  (<ref>),  $g\ms{1}{\MPcomp}\ms{1}k^{\MPrev}$),
\begin{equation}\label{BD.provorder.iso}
\phi\ms{1}{\MPcomp}\ms{1}\phi^{\MPrev}\ms{2}{=}\ms{2}T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{5}{\wedge}\ms{5}\phi^{\MPrev}\ms{1}{\MPcomp}\ms{1}\phi\ms{2}{=}\ms{2}S\ms{1}{\cap}\ms{1}S^{\MPrev}\ms{5}{\wedge}\ms{5}\phi{\MPcomp}T\ms{1}{=}\ms{1}S{\MPcomp}\phi~~.
\end{equation}
In words, $\phi$ is an order isomorphism of the domains of $T$ and $S$.

Proof   In combination with the assumption (<ref>), properties (<ref>),
(<ref>) and (<ref>) are immediate from
(<ref>), (<ref>) and (<ref>), respectively.

Proof of (<ref>) is a step on the way to proving (<ref>). From
symmetry considerations, it is an obvious first step.

$=$		$\{$	assumption:  $k\ms{1}{\MPcomp}\ms{1}k^{\MPrev}\ms{2}{=}\ms{2}h{\MPldom{}}$$~~~ \}$

$=$		$\{$	(<ref>)$~~~ \}$

$=$		$\{$	assumption:  $f\ms{1}{\MPcomp}\ms{1}f^{\MPrev}\ms{2}{=}\ms{2}g{\MPldom{}}$$~~~ \}$

$=$		$\{$	definition of $\phi$, converse$~~~ \}$

$=$		$\{$	(<ref>)$~~~ \}$

$=$		$\{$	 (<ref>) and converse$~~~ \}$

$=$		$\{$	assumption:  $f\ms{1}{\MPcomp}\ms{1}f^{\MPrev}\ms{2}{=}\ms{2}T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{2}{=}\ms{2}g\ms{1}{\MPcomp}\ms{1}g^{\MPrev}$$~~~ \}$

Symmetrically,  $\phi^{\MPrev}\ms{1}{\MPcomp}\ms{1}\phi\ms{2}{=}\ms{2}T\ms{1}{\cap}\ms{1}T^{\MPrev}$.  Finally,

$=$		$\{$	definition of $\phi$$~~~ \}$

$=$		$\{$	assumptions:  $f\ms{1}{\MPcomp}\ms{1}f^{\MPrev}\ms{2}{=}\ms{2}T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{2}{=}\ms{2}g\ms{1}{\MPcomp}\ms{1}g^{\MPrev}$

$T\ms{3}{=}\ms{3}(T\ms{1}{\cap}\ms{1}T^{\MPrev})\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}(T\ms{1}{\cap}\ms{1}T^{\MPrev})$$~~~ \}$

$=$		$\{$	assumption:  $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g\ms{4}{=}\ms{4}h^{\MPrev}\ms{1}{\MPcomp}\ms{1}S\ms{1}{\MPcomp}\ms{1}k$  , (<ref>) and converse$~~~ \}$

$=$		$\{$	assumption:  $h\ms{1}{\MPcomp}\ms{1}h^{\MPrev}\ms{2}{=}\ms{2}S\ms{1}{\cap}\ms{1}S^{\MPrev}\ms{2}{=}\ms{2}k\ms{1}{\MPcomp}\ms{1}k^{\MPrev}$$~~~ \}$

$=$		$\{$	definition of $\phi$$~~~ \}$

§.§ Pair Algebras and Galois Connections

In order to find lots of examples of block-ordered relations one need look no further than the theory of
Galois connections (which are, of course, ubiquitous).   In this section, we briefly review the notion of a
“pair algebra” —due to Hartmanis and Stearns [15, 16]— and its relation to Galois

Hartmanis and Stearns limited their analysis to finite, complete posets, and  their
analysis was less general than is  possible.  This work was extended in [2] to non-finite posets and
the current section is a short extract.

A Galois connection involves two posets  $(\mathcal{A},\sqsubseteq)$ and ($\mathcal{B}\ms{1}{,}\ms{1}{\preceq}$) and
two functions, $F\ms{1}{\in}\ms{1}\mathcal{A}{\leftarrow}\mathcal{B}$ and $G\ms{1}{\in}\ms{1}\mathcal{B}{\leftarrow}\mathcal{A}$.  These four components together form a
Galois connection iff for all $b{\in}\mathcal{B}$ and $a{\in}\mathcal{A}$
\begin{equation}\label{galois}
\end{equation}
We  refer to $F$ as the lower adjoint and to $G$ as the upper adjoint.

A Galois connection is thus a connection between two functions between posets.
Typical accounts of the properties of Galois connections (e.g.  [14]) focus
on the properties of these functions. For example, given a function $F$, one may ask
whether  $F$ is a lower adjoint in a Galois connection.  The question posed
by Hartmanis and Stearns was, however, rather different.

To motivate their  question, note that the statement $F{.}b\ms{1}{\sqsubseteq}\ms{1}a$ defines a
relation between $\mathcal{B}$  and $\mathcal{A}$.    So too does  $b\ms{1}{\preceq}\ms{1}G{.}a$.  The existence of a Galois
connection states that these two relations are equal.  A natural question is therefore:
under which conditions does an arbitrary (binary) relation between  two posets
define a Galois connection between the sets?

Exploring the question in more detail leads to two separate questions.
The first is:  suppose $R$ is a relation between posets
$(\mathcal{A},\sqsubseteq)$ and  ($\mathcal{B}\ms{1}{,}\ms{1}{\preceq}$).  What is a necessary and sufficient condition that there exist
a function  $F$ such that (a,b)1∈1R4≡4F.b1⊑1aThe second is the dual of the first: given relation $R$,
what is a necessary and sufficient condition that there exist a function $G$ such
that (a,b)1∈1R4≡4b1≼1G.aThe conjunction of these two conditions is a necessary and  sufficient condition for a
relation $R$ to define a Galois connection.  Such a relation is called  a pair algebrapair algebra.

It is easy to demonstrate that the two questions are separate.  To this end,
fig. <ref> depicts two posets and a relation between them.  The posets are $\{\alpha{,}\beta\}$ and $\{\mathsf{A}{,}\mathsf{B}\}$; both are
ordered lexicographically: the reflexive-transitive reduction of the lexicographic ordering is depicted by
the directed  edges.  The relation of type $\{\alpha{,}\beta\}{\sim}\{\mathsf{A}{,}\mathsf{B}\}$ is depicted by the undirected edges.

A Relation on Two Posets

Let the relation be denoted by $R$.  Define the function $F$ of type $\{\alpha{,}\beta\}\ms{1}{\leftarrow}\ms{1}\{\mathsf{A}{,}\mathsf{B}\}$ by $F{.}\mathsf{B}\ms{1}{=}\ms{1}\alpha$ and $F{.}\mathsf{A}\ms{1}{=}\ms{1}\beta$.  Then it
is easy to check that. for $a{\in}\{\alpha{,}\beta\}$ and $b{\in}\{\mathsf{A}{,}\mathsf{B}\}$,(a,b)1∈1R4≡4F.b1⊑1a  .(There are just four cases to be considered.)  On the other hand,  there is no function $G$  of type
$\{\mathsf{A}{,}\mathsf{B}\}\ms{1}{\leftarrow}\ms{1}\{\alpha{,}\beta\}$  such that (a,b)1∈1R4≡4b1≼1G.a  .To check that this is indeed the case, it suffices to check that the assignment $G{.}\mathsf{A}\ms{1}{=}\ms{1}\alpha$ is invalid (because $\alpha\ms{1}{\sqsubseteq}\ms{1}\alpha$ but $(\alpha,\mathsf{A})\ms{1}{\not\in}\ms{1}R$)  and
the assignment $G{.}\mathsf{A}\ms{1}{=}\ms{1}\beta$ is also invalid (because $\alpha\ms{1}{\sqsubseteq}\ms{1}\beta$  but $(\alpha,\mathsf{A})\ms{1}{\not\in}\ms{1}R$).

A less artificial, general way to demonstrate that the two questions are
separate is to consider the membership relation.  Specifically, suppose $\mathcal{S}$ is a set.  Then the membership
relation, denoted as usual by the —overloaded—  symbol  “${\in}$”, is a heterogeneous relation of type $\mathcal{S}\ms{1}{\sim}\ms{1}2^{\mathcal{S}}$
(where $2^{\mathcal{S}}$  denotes the type of subsets of $\mathcal{S}$).   Now,  for all  $x$  of type $\mathcal{S}$ and $X$ of type $2^{\mathcal{S}}$,  x1∈1X3≡3{x}1⊆1X  .The right side of this equation has the form $F{.}b\ms{1}{\sqsubseteq}\ms{1}a$ where $F$ is the function that maps an element into a
singleton set and the ordering is the subset ordering.  Also, its  left side has the form $(a,b)\ms{1}{\in}\ms{1}R$, where the
relation $R$ is the membership relation and $a$ and $b$ are $x$ and $X$, respectively.  (This is where the
overloading of notation can become confusing, for which our apologies!)  It is, however, not possible to
express $x\ms{1}{\in}\ms{1}X$  in the form $x\ms{1}{\preceq}\ms{1}G{.}X$ (except in the trivial cases where $\mathcal{S}$ has cardinality at most one).   We
leave the proof to the reader.

An example of a Galois connection is the definition
of the ceiling function on real numbers:  for all real numbers $x$,  $\lceil{}x\rceil$ is an integer such that, for all
integers $m$, x1≤1m4≡4⌈x⌉1≤1m  .To properly fit the definition of a Galois connection, it is necessary to make explicit the implicit coercion
from  integers to real numbers in the left side of this equation.  Specifically,  we have, for all real numbers $x$
and integers $m$,  x ≤_ 𝗋𝖾𝖺𝗅.m8≡8⌈x⌉ ≤_ mwhere $\mathsf{real}$ denotes the function that “coerces” an integer to a real, and $\leq_{\MPReal}$ and $\leq_{\MPInt}$ denote
the (homogeneous) at-most relations on, respectively,  real numbers and integers.  If, however, we
consider the symbol “${\leq}$” on the left side of the equation to denote the heterogeneous  at-most
relation of type $\MPReal\ms{1}{\sim}\ms{1}\MPInt$,  the fact that  x1≤1m7≡7⌈x⌉ ≤_ mgives a  representation of the (heterogeneous) “${\leq}$” relation of type $\MPReal\ms{1}{\sim}\ms{1}\MPInt$ as a block-ordered
relation:  referring to definition <ref>,  the provisional
ordering is ${\leq}_{\MPInt}$,  $f$ is the ceiling function and $g$ is the identity function.

More interesting is if we take the contrapositive.  We have, for all real numbers $x$ and integers $m$,  m1<1x5≡5m1≤1⌈x⌉-1  .On the right of this equation is the (homogeneous) at-most relation on integers.  On the left is the
(heterogeneous) less-than relation of type $\MPInt\ms{1}{\sim}\ms{1}\MPReal$.  The equation demonstrates that this relation is
block-ordered; the “blocks” of real numbers being all the numbers that have the same ceiling.  (The
functional  $f$ is the identity function, the functional $g$ maps real number $x$ to $\lceil{}x\rceil{-}1$ and the provisional
ordering is the ordering $\leq_{\MPInt}$.)   The example is interesting because the (homogeneous) less-than relation
on real numbers is not block-ordered.  This is because  its diagonal is empty.  See examples
<ref>  and <ref>.

Returning to the discussion immediately preceding example <ref>,  the two separate questions are each of interest in their own right: a
positive answer to either question may predict that  a given relation has a block-ordering of a specific
form: in the case of the first question, where the functional $g$ in definition <ref> is
the identity function, and, in the case of the second question,   where the functional $f$ in definition
<ref>  is the identity function.  In both cases, a further step is to check the
requirement on $f$ and $g$: in the first case, one has to check that the function $F$ is surjective and in the
second case that the function $G$ is surjective.  (A Galois connection is said to be “perfect” if both $F$ and $G$ are
surjective.) For example,  the fact that x1≤1m8≡8x ≤_ 𝗋𝖾𝖺𝗅.mdoes  not define a block-ordering because the function $\mathsf{real}$ is not surjective.

The relevant theory predicting exactly when the first of the two questions has
a positive answer is as follows.  Suppose  $(\mathcal{B},\sqsubseteq)$ is a complete poset.
Let ${\bigsqcap}$ denote the infimum operator for $\mathcal{B}$ and suppose $p$ is a predicate on $\mathcal{B}$.  Then we
define inf-preserving   by
\begin{equation}\label{p.inf-preserving}
p\mbox{ is  inf-preserving\ms{6}}{\equiv}\ms{6}{\left\langle\forall{}g\ms{3}{:}{:}\ms{3}p{.}({\sqcap}g)\ms{2}{\equiv}\ms{2}{\left\langle\forall{}x\ms{2}{:}{:}\ms{2}p{.}(g{.}x)\right\rangle}\right\rangle}~~.
\end{equation}
So, for a given $a$, the predicate  $\langle{}b{:}{:}\ms{2}(a,b)\ms{1}{\in}\ms{1}R\rangle$ is  inf-preserving equivales⟨∀g5::5(a1,1⊓g)1∈1R4≡4⟨∀x2::2(a1,1g.x)1∈1R⟩⟩  .Then we have:
Suppose $\mathcal{A}$ is a  set  and $(\mathcal{B},\sqsubseteq)$ is a complete poset.
Suppose  $R\ms{1}{\subseteq}\ms{1}\mathcal{A}{\MPtimes}\mathcal{B}$ is a relation between the two sets.
Define $F$  by
\begin{equation}\label{defF}
\end{equation}
Then the following two statements are equivalent.

* ${\left\langle\forall\ms{1}{}a{,}b\ms{4}{:}\ms{4}a{\in}\mathcal{A}\ms{1}{\wedge}\ms{1}b{\in}\mathcal{B}\ms{4}{:}\ms{4}(a,b)\ms{1}{\in}\ms{1}R\ms{4}{\equiv}\ms{4}F{.}a\ms{1}{\sqsubseteq}\ms{1}b\right\rangle}$.

* For all $a$, the predicate $\langle{}b{:}{:}\ms{2}(a,b)\ms{1}{\in}\ms{1}R\rangle$ is  inf-preserving.

The answer to the second question is, of course, obtained by formulating the dual of theorem <ref>.

In general, for most relations occurring in practical information systems the answer to the pair-algebra
questions will be negative: the required inf- and sup-preserving properties just do not hold.
However, a  common way to define a pair algebra is to extend a given
relation  to a relation between sets in such a way that the infimum and supremum preserving
properties are automatically satisfied.  Hartmanis and Stearns'  [15, 16] solution to the state
assignment problem was to consider the lattice of partitions of a given set; in so-called “concept analysis”,
the technique is to extend a given relation to a relation between rectangles.

An important property of Galois connections is the  theorem we call the  “unity of opposites”:
if $F$ and $G$ are  the adjoint functions in a Galois connection of the posets $(\mathcal{A},\sqsubseteq)$ and  ($\mathcal{B}{,}{\preceq}$),
then there is an isomorphism between the posets $(F{.}\mathcal{B}\ms{1},\ms{1}\sqsubseteq)$ and  ($G{.}\mathcal{A}\ms{1}{,}\ms{1}{\preceq}$).  ($F{.}\mathcal{B}$ denotes the “image”  of the
function $F$, and similarly for $G{.}\mathcal{A}$.)  Knowledge of the unity-of-opposites theorem suggests theorem
<ref>, which expresses an isomorphism between different  representations of
block-ordered relations.

§.§ Analogie Frappante

In this section, we relate block-orderings to diagonals.     The main result is  theorem  <ref>; we
call theorem  <ref> the “analogie frappante” because it generalises Riguet's  “analogie
frappante” connecting “relation de Ferrers” to diagonals.

Some elements of the following lemma have been recorded earlier by Winter [23].   We think
the overlap is justified because Winter's calculations make very heavy use of complementation whereas our
calculations avoid its use altogether.
Suppose $T$ is  a provisional   ordering of type $C{\sim}C$.
Suppose also that $f$ and $g$ are functional and onto the domain of $T$.
That is,  suppose[The ordering  $T$ must be homogeneous
but $f$ and $g$ may be heterogeneous and of different type, so long as both have target $C$.]  that f11f^4=4f4=4T1∩1T^4=4g4=4g11g^  .Let $R$ denote $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$.  Then
\begin{equation}\label{BD.provorder.dom}
\end{equation}

\begin{equation}\label{BD.provorder.Rwok}
f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T^{\MPrev}\ms{1}{\MPcomp}\ms{1}g\ms{4}{=}\ms{4}R{\MPldom{}}\ms{1}{\MPcomp}\ms{1}(R{\setminus}R{/}R)^{\MPrev}\ms{1}{\MPcomp}\ms{1}R{\MPrdom{}}\mbox{~, and}
\end{equation}

\begin{equation}\label{BD.provorder.fwokg}
\end{equation}

\begin{equation}\label{BD.provorder.domdelta}
\end{equation}

\begin{equation}\label{BD.provorder.perdom}
\end{equation}

Proof   Property (<ref>) is a straightforward application of domain calculus:

$=$		$\{$	definition:   $R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$$~~~ \}$

$=$		$\{$	domains (specifically,  $\left[\ms{2}(U{\MPcomp}V){\MPrdom{}}\ms{1}{=}\ms{1}(U{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}V){\MPrdom{}}\ms{2}\right]$  and $\left[\ms{2}(U^{\MPrev}){\MPrdom{}}\ms{1}{=}\ms{1}U{\MPldom{}}\ms{2}\right]$)$~~~ \}$

$=$		$\{$	 assumption:   $T\ms{2}{=}\ms{2}f{\MPldom{}}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g{\MPldom{}}$  (so $T\ms{2}{=}\ms{2}f{\MPldom{}}\ms{1}{\MPcomp}\ms{1}T$)$~~~ \}$

$=$		$\{$	domains (specifically,  $\left[\ms{2}(U{\MPcomp}V){\MPrdom{}}\ms{1}{=}\ms{1}(U{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}V){\MPrdom{}}\ms{2}\right]$)$~~~ \}$

$=$		$\{$	lemma <ref> and assumption: $T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{2}{=}\ms{2}g{\MPldom{}}$  $~~~ \}$

By a symmetric argument, $(f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g){\MPldom{}}\ms{2}{=}\ms{2}f{\MPrdom{}}$.

Now we consider (<ref>).  The raison d'être of (<ref>) is that it expresses the
left side as a function of $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$.   In a pointwise
calculation a natural step is to use indirect ordering.  In a point-free calculation, this corresponds to using
factors.  That is, we exploit  lemma <ref>:

$=$		$\{$	assumption: $T$ is a provisional ordering

lemmas <ref>, <ref> and  <ref>$~~~ \}$

$=$		$\{$	assumption:   $f{\MPldom{}}\ms{2}{=}\ms{2}T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{2}{=}\ms{2}g{\MPldom{}}$ $~~~ \}$

$=$		$\{$	lemma <ref> and assumption:   $T\ms{2}{=}\ms{2}f{\MPldom{}}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g{\MPldom{}}$$~~~ \}$

$=$		$\{$	(<ref>) and definition of $R$$~~~ \}$

$=$		$\{$	factors$~~~ \}$

Note the use of lemma <ref>.   The discovery of this lemma is driven by the goal of the calculation.

The pointwise interpretation of $f^{\MPrev}\ms{1}{\MPcomp}\ms{1}g$ is a relation expressing  equality between values of $f$ and $g$.  This
suggests that, in order to prove (<ref>),  we begin by exploiting the anti-symmetry of $T$:

$=$		$\{$	$f{\MPldom{}}\ms{3}{=}\ms{3}T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{3}{=}\ms{3}g{\MPldom{}}$ and domains$~~~ \}$

$=$		$\{$	distributivity (valid because $f$ and $g$ are functional)$~~~ \}$

$=$		$\{$	definition of $R$ and (<ref>)$~~~ \}$

$=$		$\{$	(<ref>)  (see below)$~~~ \}$

$=$		$\{$	domains  (specifically,  $f{\MPrdom{}}\ms{1}{\MPcomp}\ms{1}f^{\MPrev}\ms{2}{=}\ms{2}f^{\MPrev}$ and $g\ms{1}{\MPcomp}\ms{1}g{\MPrdom{}}\ms{2}{=}\ms{2}g$)$~~~ \}$

$=$		$\{$	definition of $R$ and $\Delta{}R$$~~~ \}$

A crucial step in the above calculation is the use of the property
\begin{equation}\label{ARSB}
\end{equation}
for all relations $U$ and $V$ and coreflexive relations $p$ and $q$.   This is a frequently used property of domain

The remaining equations (<ref>) and (<ref>) are straightforward.

$=$		$\{$	(<ref>)$~~~ \}$

$=$		$\{$	domains and assumption:  $f{\MPldom{}}\ms{2}{=}\ms{2}g{\MPldom{}}$$~~~ \}$

$=$		$\{$	assumption:  $f{\MPldom{}}\ms{3}{=}\ms{3}T\ms{1}{\cap}\ms{1}T^{\MPrev}$$~~~ \}$

$=$		$\{$	domains and converse$~~~ \}$

$=$		$\{$	lemma <ref> and domains$~~~ \}$

$=$		$\{$	domains and assumption:  $g{\MPldom{}}\ms{2}{=}\ms{2}T\ms{1}{\cap}\ms{1}T^{\MPrev}$

and lemma <ref>$~~~ \}$

That is  $(\Delta{}R){\MPldom{}}\ms{3}{=}\ms{3}R{\MPldom{}}$.    The dual equation  $(\Delta{}R){\MPrdom{}}\ms{3}{=}\ms{3}R{\MPrdom{}}$ is immediate from the fact that $(\Delta{}R)^{\MPrev}\ms{1}{=}\ms{1}\Delta(R^{\MPrev})$ and
properties of the domain operators.     For the per  domains, we have:

$=$		$\{$	$R{\MPldom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPldom{}}$ and $R{\MPrdom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPrdom{}}$ (above);  lemma <ref> $~~~ \}$

$=$		$\{$	$\Delta{}R$ is difunctional,  theorem <ref> (with $R\ms{1}{:=}\ms{1}\Delta{}R$)$~~~ \}$

$=$		$\{$	lemma <ref> and definition of $\Delta{}R$ $~~~ \}$

$=$		$\{$	converse and $f{\MPldom{}}\ms{4}{=}\ms{4}g{\MPldom{}}\ms{4}{=}\ms{4}g\ms{1}{\MPcomp}\ms{1}g^{\MPrev}$$~~~ \}$

Again, the dual equation is immediate.

We now prove the converse of lemma  <ref>.
A relation $R$ is block-ordered if $R{\MPldom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPldom{}}$ and $R{\MPrdom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPrdom{}}$.

Proof   Suppose $R{\MPldom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPldom{}}$ and $R{\MPrdom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPrdom{}}$.  Our task is to construct relations  $f$,  $g$ and  $T$ such thatR2=2f^11T11g  ,T1∩1T^3⊆3I7∧7T3=3(T1∩1T^)11T11(T1∩1T^)7∧7TT1⊆1T f11f^4=4f4=4T1∩1T^4=4g4=4g11g^  .Since $\Delta{}R$ is difunctional,  theorem <ref> is the obvious place to start.  Applying the theorem,
we can  construct $f$ and $g$ such that  ΔR2=2f^11g5∧5f11f^3=3f3=3g11g^3=3g  .Using standard properties of the domain operators together with the assumption that
$R{\MPldom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPldom{}}$ and $R{\MPrdom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPrdom{}}$, it follows that R2=2f5∧5R2=2g  .It remains to construct the provisional ordering $T$.  The appropriate construction is suggested  by lemma
<ref>, in particular (<ref>).  Specifically, we define $T$ by the equation
\begin{equation}\label{def.prov.order}
\end{equation}
The proof that $R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$ is by mutual inclusion.  First note that
\begin{equation}\label{prov.order.delta}
\end{equation}

$=$		$\{$	(<ref>)$~~~ \}$

$=$		$\{$	$\Delta{}R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}g$$~~~ \}$

$\subseteq$		$\{$	(<ref>) and $\Delta{}R\ms{1}{\subseteq}\ms{1}R$$~~~ \}$

$\subseteq$		$\{$	cancellation$~~~ \}$

$=$		$\{$	(<ref>)$~~~ \}$

$=$		$\{$	per domains$~~~ \}$

$=$		$\{$	assumption:  $R{\MPldom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPldom{}}$ and $R{\MPrdom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPrdom{}}$,    lemma <ref>$~~~ \}$

$=$		$\{$	 $\Delta{}R$ is difunctional,  theorem <ref> (with $R\ms{1}{:=}\ms{1}\Delta{}R$)$~~~ \}$

$\Leftarrow$		$\{$	monotonicity$~~~ \}$

$\Leftarrow$		$\{$	$\Delta{}R^{\MPrev}\ms{1}{\subseteq}\ms{1}R{\setminus}R{/}R$, monotonicity$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	cancellation$~~~ \}$

Combining the two inclusions we conclude that indeed $R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$.

We now establish the requirements on $T$.  First,

$=$		$\{$	definition and converse$~~~ \}$

$\subseteq$		$\{$	modular law$~~~ \}$

$=$		$\{$	$\Delta{}R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}g$$~~~ \}$

$\subseteq$		$\{$	$\Delta{}R\ms{1}{\subseteq}\ms{1}R$, monotonicity and cancellation$~~~ \}$

$=$		$\{$	$\Delta{}R\ms{2}{=}\ms{2}R\ms{3}{\cap}\ms{3}(R{\setminus}R{/}R)^{\MPrev}$$~~~ \}$

$=$		$\{$	$\Delta{}R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}g$$~~~ \}$

$=$		$\{$	$f\ms{1}{\MPcomp}\ms{1}f^{\MPrev}\ms{3}{=}\ms{3}f{\MPldom{}}\ms{3}{=}\ms{3}g\ms{1}{\MPcomp}\ms{1}g^{\MPrev}\ms{3}{=}\ms{3}g{\MPldom{}}$$~~~ \}$

Thus $T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{2}{\subseteq}\ms{2}f{\MPldom{}}$.   So $T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{2}{\subseteq}\ms{2}I$.   Now

$=$		$\{$	infima and $f{\MPldom{}}$ is coreflexive$~~~ \}$

$\Leftarrow$		$\{$	domains$~~~ \}$

$\Leftarrow$		$\{$	definition of $T$ and monotonicity$~~~ \}$

$\Leftarrow$		$\{$	$f{\MPldom{}}\ms{3}{=}\ms{3}g\ms{1}{\MPcomp}\ms{1}g^{\MPrev}$, domains and monotonicity$~~~ \}$

$=$		$\{$	$f^{\MPrev}\ms{1}{\MPcomp}\ms{1}g\ms{2}{=}\ms{2}\Delta{}R$$~~~ \}$

$=$		$\{$	$\Delta{}R\ms{3}{=}\ms{3}R\ms{2}{\cap}\ms{2}(R{\setminus}R{/}R)^{\MPrev}$, converse$~~~ \}$

So, by anti-symmetry we have established that $T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{2}{=}\ms{2}f{\MPldom{}}$.    Since also $f{\MPldom{}}\ms{1}{=}\ms{1}g{\MPldom{}}$, we conclude from the
definition of $T$ and properties of domains that T3=3(T1∩1T^)11T11(T1∩1T^)  .The final task is to show that $T$ is transitive:

$=$		$\{$	definition$~~~ \}$

$=$		$\{$	$\Delta{}R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}g$$~~~ \}$

$\subseteq$		$\{$	$\Delta{}R\ms{1}{\subseteq}\ms{1}R$$~~~ \}$

$\subseteq$		$\{$	factors$~~~ \}$

$=$		$\{$	definition$~~~ \}$

It is interesting to reflect on the proof of lemma <ref>.    The hardest part is to find appropriate
definitions of $f$, $g$ and $T$ such that $R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$.  The key to constructing $f$ and $g$ is Riguet's “analogie
frappante” [20] whereby he introduced the  “diff'erence” —the diagonal $\Delta{}R$—  of the relation $R$.
Expressing the diagonal in terms of factors as we have done makes many parts of the calculations very
straightforward.  One much less straightforward step is the use of lemma <ref> in the proof that
$R\ms{2}{\subseteq}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$.  Note how calculational needs drive the search for the lemma:  in order to simplify the
inclusion it is necessary to expose the term $R{\setminus}R{/}R$ on the right side, and that is precisely what the lemma

We conclude with the theorem that we call the “analogie frappante”.  It is not the theorem that Riguet
suggested  but we have chosen to give it this name in order to recognise Riguet's contribution.
[Analogie Frappante]   A relation $R$ is block-ordered if and only
if  $R{\MPldom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPldom{}}$ and $R{\MPrdom{}}\ms{2}{=}\ms{2}(\Delta{}R){\MPrdom{}}$.

Proof    Lemma <ref> establishes “only-if” and lemma <ref> establishes “if”.

A generic way to construct examples of relations that are not
block-ordered is to exploit example  <ref>.  In order to avoid unnecessary repetition, we
refer the reader to that example for the definition of the relation $\mathsf{in}$ given a finite set  $\mathcal{X}$ and a set $\mathcal{S}$ of
subsets of $\mathcal{X}$.

Recall  that the diagonal  $\Delta\mathsf{in}$ of type $\mathcal{X}{\sim}\mathcal{S}$ is injective.  It follows that the
size of  $(\Delta\mathsf{in}){\MPldom{}}$  is at most  the size of  $\mathcal{S}$.    If, however, the set $\mathcal{S}$ has $\mathcal{X}$ as one of its elements, the size of $\mathsf{in}{\MPldom{}}$
equals the size of $\mathcal{X}$.   Theorem  <ref> thus predicts that,  if $\mathcal{X}$ is an element of $\mathcal{S}$,   a necessary
condition for $\mathsf{in}$ to be block-ordered is  that the sizes of  $\mathcal{X}$ and $\mathcal{S}$ must be equal;  conversely,  if $\mathcal{X}$ is an
element of $\mathcal{S}$,  $\mathsf{in}$ is not block-ordered if  the sizes of  $\mathcal{X}$ and $\mathcal{S}$ are  different.

Fig. <ref> (example <ref>)  shows that, even if the sizes of $\mathcal{X}$ and $\mathcal{S}$ are
equal, the relation $\mathsf{in}$ may not be block-ordered: as remarked then,  for the choice of $\mathcal{S}$ shown in fig.
<ref>,  $\mathsf{in}{\MPldom{}}$ and $(\Delta\mathsf{in}){\MPldom{}}$  are different since $0$ and $3$  are  elements  of  the former but not the

It is straightforward to construct instances of $\mathcal{X}$ and $\mathcal{S}$ such that the relation $\mathsf{in}$ is block-ordered.  It
suffices to ensure that three conditions are satisfied:   $\mathcal{X}$ is an element of $\mathcal{S}$,  the sizes of $\mathcal{X}$ and $\mathcal{S}$ are equal,
and, for each $x$ in $\mathcal{X}$,  the set of sets represented by $(x{\MPcomp}\mathsf{in}){\MPrdom{}}$ is totally ordered.   Fig. <ref> is
one such.  Referring to definition  <ref>,  the functional $f$ is $\Delta\mathsf{in}^{\MPrev}$
(depicted by rectangles)  and the functional $g$ is $I_{\mathcal{S}}$;  the ordering relation is
the subset relation $\mathsf{in}{\setminus}\mathsf{in}$ (depicted by the directed graph).

A Block-Ordered Membership Relation

The following theorem is a corollary of theorem <ref>.   In combination with theorem
<ref> it states that a relation is block-ordered iff its core is block-ordered.  Testing whether or
not  a given relation is block-ordered can thus be decomposed into computing a core of the relation
and then testing whether or not that is block-ordered.   (For practical purposes computing an index of the
relation is to be preferred.)
Suppose $R$ is an arbitrary relation and suppose $C$ is a core of $R$ as
witnessed by $\lambda$ and $\rho$.  Then R3=3(ΔR)7≡7C3=3(ΔC)  .Dually,  R3=3(ΔR)7≡7C3=3(ΔC)  .

Proof   Suppose $R$, $C$,   $\lambda$ and $\rho$ are as in definition <ref>.  Then

$=$		$\{$	definition <ref> and theorem  <ref> $~~~ \}$

$\Rightarrow$		$\{$	Leibniz$~~~ \}$

$=$		$\{$	domains$~~~ \}$

$=$		$\{$	 $\lambda^{\MPrev}\ms{1}{\MPcomp}\ms{1}\lambda\ms{1}{\MPcomp}\ms{1}R\ms{4}{=}\ms{4}R{\MPperldom{}}\ms{1}{\MPcomp}\ms{1}R\ms{4}{=}\ms{4}R$,

$(\rho^{\MPrev}){\MPldom{}}\ms{3}{=}\ms{3}(\rho^{\MPrev}\ms{1}{\MPcomp}\ms{1}\rho){\MPldom{}}\ms{3}{=}\ms{3}(R{\MPperrdom{}}){\MPldom{}}\ms{3}{=}\ms{3}R{\MPrdom{}}$,  and domains $~~~ \}$

$=$		$\{$	$(\rho^{\MPrev}){\MPldom{}}\ms{3}{=}\ms{3}(\rho^{\MPrev}\ms{1}{\MPcomp}\ms{1}\rho){\MPldom{}}$  and   domains$~~~ \}$

$=$		$\{$	theorem <ref>$~~~ \}$

$=$		$\{$	theorem <ref>$~~~ \}$

$=$		$\{$	definition <ref>, theorem  <ref> and Leibniz$~~~ \}$

$\Rightarrow$		$\{$	Leibniz and domains$~~~ \}$

$=$		$\{$	$\rho{\MPldom{}}\ms{3}{=}\ms{3}(\rho\ms{1}{\MPcomp}\ms{1}\rho^{\MPrev}){\MPldom{}}$  and   domains$~~~ \}$

$=$		$\{$	theorem <ref> (applied twice)$~~~ \}$

The property R3=3(ΔR)7≡7C3=3(ΔC)follows by mutual implication.  The dual follows by instantiating  $R$ to  $R^{\MPrev}$ and applying the properties of

By combining the definition of block-ordering with theorem <ref>, it is immediately clear that
$R$ is block-ordered if  its core $C$ is a provisional ordering.  In general, a core of a block-ordered relation will not
be a provisional ordering.  This is  because the types of the targets of the  components $\lambda$ and $\rho$ in the
definition of a core are  not required to be the same; on the other hand, orderings are  required to be
homogeneous relations.    However by carefully restricting the choice of core,  it is possible to construct a
core that is indeed a provisional ordering.
Suppose $R$ is an arbitrary relation.  Then  if  $R$ is block-ordered it
has a core  that is a provisional ordering.

Proof   Suppose $R$ is block-ordered. That is, suppose that $f$, $g$ and $T$ are relations such that  $T$ is a
provisional ordering, R2=2f^11T11gand f11f^4=4f4=4T1∩1T^4=4g4=4g11g^  .Then,  by lemma <ref>,    $R{\MPperldom{}}\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}f$ and ,  $R{\MPperrdom{}}\ms{2}{=}\ms{2}g^{\MPrev}\ms{1}{\MPcomp}\ms{1}g$.   Thus $f$ and $g$ satisfy the conditions
for witnessing  a core  $C$ of $R$.  (Cf. definition <ref> with $\lambda{,}\rho\ms{1}{:=}\ms{1}f{,}g$.)  Consequently,

$=$		$\{$	definition <ref>$~~~ \}$

$=$		$\{$	$R\ms{2}{=}\ms{2}f^{\MPrev}\ms{1}{\MPcomp}\ms{1}T\ms{1}{\MPcomp}\ms{1}g$$~~~ \}$

$=$		$\{$	$f\ms{1}{\MPcomp}\ms{1}f^{\MPrev}\ms{4}{=}\ms{4}f{\MPldom{}}\ms{4}{=}\ms{4}T\ms{1}{\cap}\ms{1}T^{\MPrev}\ms{4}{=}\ms{4}g{\MPldom{}}\ms{4}{=}\ms{4}g\ms{1}{\MPcomp}\ms{1}g^{\MPrev}$$~~~ \}$

$=$		$\{$	$T$ is a provisional ordering, lemma <ref> and domains$~~~ \}$

We conclude that $C$ is the  provisional ordering $T$.

Combining theorem <ref> with the theorem that all cores of a given relation are
isomorphic, we conclude that any core of a
block-ordered relation is isomorphic to a provisional ordering.  Loosely speaking, block-ordered
relations are   provisional orderings  up to isomorphism and reduction to the core.
From the Galois connection, for all reals $x$ and integers  $m$,  ⌈x⌉1≤1m4≡4x1≤1mdefining the ceiling function, we deduce  that the heterogeneous relation  ${}_{\MPReal}{\leq}_{\MPInt}$  has core the provisional
ordering ${\leq}_{\MPInt}$.  This is because  the ceiling function is surjective.   Its core in not the ordering ${\leq}_{\MPReal}$ because
the  coercion $\mathsf{real}$  from integers to reals is  not surjective.  (See also  example  <ref>.)

On the other hand, if a  Galois connection  F.b1⊑1a2≡2b1≼1G.aof posets  $(\mathcal{A},\sqsubseteq)$ and ($\mathcal{B}\ms{1}{,}\ms{1}{\preceq}$)  is “perfect” (i.e. both $F$ and $G$ are surjective),  both the orderings ${\sqsubseteq}$ and ${\preceq}$ are
cores of the defined heterogeneous relation.  That the orderings are isomorphic is an instance of  the
unity-of-opposites theorem [4].

§ STAIRCASE RELATIONS

For any binary  relation $R$, the relations $R{\setminus}R$ and $R{/}R$ are preorders.  That is, both are transitive and
reflexive.   (If $R$ has type $A{\sim}B$ then $R{\setminus}R$ has type $B{\sim}B$ and $R{/}R$ has type $A{\sim}A$.)
That  relation $R$ is a “staircase” relation  means formally
that the preorder $R{\setminus}R$ is linear[An
ordering  $S$ —of any sort— is said to be linear  if $S\ms{1}{\cup}\ms{1}S^{\MPrev}\ms{3}{=}\ms{3}{\MPplattop}$.  Sometimes the word “total” is
used instead of linear.  For example,  Riguet [20] uses the term “totalement
ordonn'ees”.].  For brevity, we denote the property of being a staircase relation by $\mathsf{SC}$.  That is:
The predicate $\mathsf{SC}$ on (binary) relations is defined by, for all $R$,𝖲𝖢.R9≡9R∖R1∪1(R∖R)^3=3  .A relation that satisfies the predicate $\mathsf{SC}$ is called a staircase relation.

The pointwise formulation of the relation $R{\setminus}R$ is b0R∖Rb17≡7⟨∀a2:2aRb02:2aRb1⟩  .In terms of the mental picture shown in fig. <ref>,  a vertical line through a
point $b$  depicts the set of points $a$ such that $a\MPdopen{}R\MPdclose{}b$;  a staircase relation is one such that the points of type $B$
can be ordered in such a way that the preorder $R{\setminus}R$ is depicted by the left-to-right ordering of points on
the  $B$-axis,   and the length of the  vertical lines increases monotonically (although not always
strictly) as one proceeds from left to right in the diagram.

Various equivalent definitions of the predicate $\mathsf{SC}$ are given below.  Riguet [20] defined a “relation
de Ferrers” to be a relation satisfying (<ref>).    The equivalence of (<ref>) and (<ref>)
corresponds in the mental picture of a staircase relation to the property that the
vertical lines being increasing in length is equivalent to the horizontal lines being decreasing  in length.
(Cf.  the statement of Riguet's theorem quoted in the introduction.)
The following are all equivalent formulations of $\mathsf{SC}{.}R$:
\begin{equation}\label{BDunder}
\end{equation}

\begin{equation}\label{BDover}
\end{equation}

\begin{equation}\label{BDboth}
\end{equation}

\begin{equation}\label{BDneg}
\end{equation}

Proof   We prove first that (<ref>) and (<ref>) are equivalent:

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	complements$~~~ \}$

$=$		$\{$	 (<ref>) with $R{,}S\ms{2}{:=}\ms{2}R^{\MPrev}\ms{1}{,}\ms{1}R^{\MPrev}$ (and $R\ms{1}{=}\ms{1}(R^{\MPrev})^{\MPrev}$)$~~~ \}$

$=$		$\{$	(<ref>) with $R{,}S\ms{1}{:=}\ms{1}R{,}R$$~~~ \}$

$=$		$\{$	$\left[\ms{1}S\ms{1}{\subseteq}\ms{1}{\MPplattop}\ms{1}\right]$ with $S\ms{2}{:=}\ms{2}R{/}R\ms{2}{\cup}\ms{2}(R{/}R)^{\MPrev}$ and anti-symmetry$~~~ \}$

A symmetric argument establishes the equivalence of (<ref>) and (<ref>):

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	complements$~~~ \}$

$=$		$\{$	 (<ref>) with $S{,}T\ms{2}{:=}\ms{2}R^{\MPrev}\ms{1}{,}\ms{1}R^{\MPrev}$ $~~~ \}$

$=$		$\{$	(<ref>) with $R{,}S\ms{1}{:=}\ms{1}R{,}R$ (and $R\ms{1}{=}\ms{1}(R^{\MPrev})^{\MPrev}$)$~~~ \}$

$=$		$\{$	$\left[\ms{1}S\ms{1}{\subseteq}\ms{1}{\MPplattop}\ms{1}\right]$ with $S\ms{2}{:=}\ms{2}R{\setminus}R\ms{2}{\cup}\ms{2}(R{\setminus}R)^{\MPrev}$ and anti-symmetry$~~~ \}$

$=$		$\{$	factors$~~~ \}$

$=$		$\{$	converse and complements $~~~ \}$

$=$		$\{$	$\left[\ms{1}S\ms{1}{\subseteq}\ms{1}{\MPplattop}\ms{1}\right]$ with $S\ms{2}{:=}\ms{2}R\ms{2}{\cup}\ms{2}(R{\setminus}R{/}R)^{\MPrev}$ and anti-symmetry$~~~ \}$

An example of a staircase relation predicted by lemma <ref> is the at-most relation — on
natural numbers, integers, rational numbers or reals.

Two general methods for identifying examples of staircase relations are given in lemmas
<ref> and <ref>.
A linear preorder  is a staircase relation.  That is,  for all (homogeneous)  $R$,𝖲𝖢.R7⇐7RR1⊆1R4∧4I1⊆1R4∧4R1∪1R^2=2  .

Proof   We haveR1=1R∖R/R6⇐6RR1⊆1R3∧3I1⊆1Rsince

$=$		$\{$	factors$~~~ \}$

$\Leftarrow$		$\{$	monontonicity and transitivity$~~~ \}$

$=$		$\{$	$\left[\ms{2}R\ms{1}{=}\ms{1}I{\setminus}R{/}I\ms{2}\right]$$~~~ \}$

$\Leftarrow$		$\{$	(anti)monotonicity$~~~ \}$

Also,R^11R^2⊆2R^4∧4I1⊆1R^7≡7RR1⊆1R3∧3I1⊆1R  .(The converse of a preorder is a preorder.) So

$=$		$\{$	lemma <ref>, in particular (<ref>)$~~~ \}$

$=$		$\{$	assumption:  $R$ is a preorder

(hence,  $R^{\MPrev}$ is a preorder and $R^{\MPrev}\ms{2}{=}\ms{2}R^{\MPrev}\ms{1}{\setminus}\ms{1}R^{\MPrev}\ms{1}{/}\ms{1}R^{\MPrev}$)

lemma <ref>, in particular  (<ref>)$~~~ \}$

$=$		$\{$	assumption:  $R$ is linear (i.e.  $R\ms{1}{\cup}\ms{1}R^{\MPrev}\ms{2}{=}\ms{2}{\MPplattop}$)$~~~ \}$

The second way of constructing a staircase relation is to reduce a linear preorder by eliminating its
reflexive part (making it so-called “strict”).  For example, the less-than relation (on
natural numbers, integers, rational numbers or reals) is a staircase relation.
Formally, we have:
For all (homogeneous)  $R$,𝖲𝖢.R7⇐7RR1⊆1R4∧4R1∪1I1∪1R^2=2  .

$=$		$\{$	 (<ref>)$~~~ \}$

$=$		$\{$	$\left[\ms{1}X\ms{1}{\subseteq}\ms{1}{\MPplattop}\ms{1}\right]$ and antisymmetry$~~~ \}$

$\Leftarrow$		$\{$	assumption:  $R\ms{1}{\cup}\ms{1}I\ms{1}{\cup}\ms{1}R^{\MPrev}\ms{2}{=}\ms{2}{\MPplattop}$, so ${\MPplattop}\ms{2}{\subseteq}\ms{2}R\ms{1}{\cup}\ms{1}I\ms{1}{\cup}\ms{1}R^{\MPrev}$

monotonicity and transitivity$~~~ \}$

$=$		$\{$	converse, factors and distributivity$~~~ \}$

$=$		$\{$	supremum and monotonicity$~~~ \}$

$=$		$\{$	assumption$~~~ \}$

The less-than relations on the integers, ${<}_{\MPInt}$, on the rationals,  ${<}_{\MPRational}$,
and on the reals, ${<}_{\MPReal}$,
are all staircase relations since in each case $<{\setminus}<$  is the at-most relation, $\leq$.
See example <ref> for details of the preorder  in each case.
The less-than relation on the integers is a (linearly) block-ordered relation but the
less-than relation on the rationals and the less-than relation on the reals are not block-ordered.  This is
because, as shown in example <ref>,  the less-than relations on the rationals and on the
reals both have empty diagonals.

That the less-than relation on the real
numbers is not block-ordered is a consequence of the fact that if $x\ms{1}{<}\ms{1}y$ the interval between $x$ and $y$ can
always be subdivided at will.  (That is, it is always possible to find a real number $z$ such that $x\ms{1}{<}\ms{1}z$ and
$z\ms{1}{<}\ms{1}y$.)  The same is also true of the rationals.   Abstracting from the details of the less-than
relation, we get the following theorem.  (Winter [23] proves a similar theorem. See section
<ref> for further discussion.)
Suppose $R$ is a homogeneous relation such that R1≠16∧6I∩R1=16∧6R1=1RR6∧6R1∪1I1∪1R^2=2  .Then $R$ is a staircase relation and $\Delta{}R\ms{1}{=}\ms{1}{\MPplatbottom}$.

It follows that any such relation is not block-ordered.

Proof   Lemma <ref> proves that $R$ is a staircase relation.

Comparing the above conditions on $R$ with those in  lemma <ref>, the additions are the
non-emptiness property $R\ms{1}{\neq}\ms{1}{\MPplatbottom}$,   the “strictness”  property   $I{\cap}R\ms{1}{=}\ms{1}{\MPplatbottom}$  and the  “subdivision” property
$R\ms{2}{\subseteq}\ms{2}R{\MPcomp}R$.    (The less-than relation on real numbers has the subdivision  property whereas the less-than
relation on the integers does not.) Applying lemma <ref> (below), the subdivision and strictness
properties imply that  $\Delta{}R\ms{1}{=}\ms{1}{\MPplatbottom}$. That $R$ is not block-ordered follows from theorem <ref> and the
assumption that $R\ms{1}{\neq}\ms{1}{\MPplatbottom}$.

The lemma used to prove theorem <ref> is the following:
R1⊆1RR2⇒2(ΔR1=12≡2I∩R1⊆1)  .

$\Rightarrow$		$\{$	monotonicity$~~~ \}$

$\Rightarrow$		$\{$	modular law$~~~ \}$

$=$		$\{$	assumption:  $R\ms{1}{\subseteq}\ms{1}R{\MPcomp}R$$~~~ \}$

$=$		$\{$	complements$~~~ \}$

$=$		$\{$	$I\ms{1}{=}\ms{1}I^{\MPrev}$,  converse and shunting$~~~ \}$

$\Rightarrow$		$\{$	monotonicity$~~~ \}$

$\Rightarrow$		$\{$	assumption:  $R\ms{1}{\subseteq}\ms{1}R{\MPcomp}R$ and transitivity$~~~ \}$

That is,
\begin{equation}\label{dense.IandR}
\end{equation}

$=$		$\{$	$\left[\ms{1}{\MPplatbottom}\ms{1}{\subseteq}\ms{1}X\ms{1}\right]$ and antisymmetry, definition of $\Delta{}R$$~~~ \}$

$=$		$\{$	shunting $~~~ \}$

$=$		$\{$	(<ref>)$~~~ \}$

$=$		$\{$	assumption:  $R\ms{1}{\subseteq}\ms{1}R{\MPcomp}R$,  (<ref>) $~~~ \}$

§ CONCLUSION

The primary novel contribution of this paper is the combination of theorems <ref>  and
<ref>: essentially, a block-ordered relation is a relation whose core is a provisional
ordering.   The discovery of these theorems was inspired by Riguet's suggestion of an
“analogie frappante” linking the notion of a “relation de Ferrers” and the (difunctional)  “diff'erence”
of a relation.  Theorem <ref> is a precise statement of an “analogie” linking the notions of a
block-ordered relation and  the diagonal of a relation.

A secondary, but nevertheless important,  contribution of this paper is  our (almost) exclusive use of the
properties of factors of a relation, particularly with respect to formulating and reasoning about the
notion of the diagonal of a relation (Riguet's “diff'erence”), as opposed to Riguet's use of nested
complements.    Indeed, our only use of complements is in section <ref> where we
formulated the notion of a staircase relation —in terms of factors— and showed its equivalence to
Riguet's notion of a “relation de Ferrers” —which he formulated in terms of nested complements— .

Our motivation for including section <ref> is partly to give proper credit to Riguet's
contribution but also to rectify misleading/incorrect statements
in the extant literature[See  [6], in
particular the concluding section,  for references to the relevant literature.].  Specifically, the claim that
a “relation de Ferrers … can be rewritten in staircase block form”  <cit.>
is, at best, confused: as shown in example <ref>,  the less-than relation on real numbers is a
staircase relation but not block-ordered.  The lesson to be learnt is, in our view, that mental pictures, such
as the one of a staircase relation shown in fig.  <ref> and informal natural-language statements,
can never be relied on.  Ultimately,  it is vital that
informal notions are  formalised and the properties of the formal notions are explored in detail in order
to confirm that they do indeed conform to their intended meaning.

Many thanks to Jules Desharnais for helping to locate Riguet's publications.

[1]
A.V. Aho, M.R. Garey, and J.D. Ullman.
The transitive reduction of a directed graph.
SIAM J. of Computing, 1(2):131–137, 1972.

[2]
Roland Backhouse.
Pair algebras and Galois connections.
Information Processing Letters, 67(4):169–176, 31 August 1998.

[3]
Roland Backhouse.
Fixed point calculus.
Summer School and Workshop on Algebraic and Coalgebraic Methods in
the Mathematics of Program Construction, available at
, April 2000.

[4]
Roland Backhouse.
Galois connections and fixed point calculus.
In Roland Backhouse, Roy Crole, and Jeremy Gibbons, editors, Algebraic and Coalgebraic Methods in the Mathematics of Program
Construction, volume 2297 of LNCS Tutorial, chapter 4, pages 89–148.
Springer, 2002.
International Summer School and Workshop, Oxford, UK, April 2000,
Revised Lectures (Abridged version of [3]).

[5]
Roland Backhouse.
Regular algebra applied to language problems.
Journal of Logic and Algebraic Programming, 66:71–111, 2006.

[6]
Roland Backhouse.
Difunctions and block-ordered relations.
Working document. Available at ResearchGate and
, 2021.

[7]
Roland Backhouse.
Elements of algorithmic graph theory. An exercise in combining
precision with concision.
Working Document. Extended version of [8]. Also
available from ResearchGate, 2022.

[8]
Roland Backhouse, Henk Doornbos, Roland Glück, and Jaap van der Woude.
Components and acyclicity of graphs. An exercise in combining
precision with concision.
Journal of Logical and Algebraic Methods in Programming,
124:100730, 2022.

[9]
R.C. Backhouse and P. Hoogendijk.
Elements of a relational theory of datatypes.
In B. Möller, H.A. Partsch, and S.A. Schuman, editors, Formal Program Development. Proc. IFIP TC2/WG 2.1 State of the Art Seminar,
Rio de Janeiro, Jan. 1992, volume 755 of LNCS, pages 7–42.
Springer-Verlag, 1993.

[10]
Roland Backhouse and Ed Voermans.
The index and core of a relation. With application to the
axiomatics of relation algebra and block-ordered relations.
Available at ResearchGate, April 2022.

[11]
Roland Backhouse and Ed Voermans.
The index and core of a relation. With application to the
axiomatics of relation algebra.
Submitted for publication., September 2023.

[12]
J.H. Conway.
Regular Algebra and Finite Machines.
Chapman and Hall, London, 1971.

[13]
P.J. Freyd and A. Ščedrov.
Categories, Allegories.
North-Holland, 1990.

[14]
G. Gierz, K. H. Hofmann, K. Keimel, J.D. Lawson, M. Mislove, and D. S. Scott.
A Compendium of Continuous Lattices.
Springer-Verlag, 1980.

[15]
J. Hartmanis and R.E. Stearns.
Pair algebras and their application to automata theory.
Information and Control, 7(4):485–507, 1964.

[16]
J. Hartmanis and R.E. Stearns.
Algebraic Structure Theory of Sequential Machines.
Prentice-Hall, 1966.

[17]
José N. Oliveira.
Programming from metaphorisms.
JLAMP, 94:15–44, January 2018.

[18]
J. Riguet.
Relations binaire, fermetures, correspondances de Galois.
Bulletin de la Société Mathématiques de France,
76:114–155, 1948.

[19]
J. Riguet.
Quelques propriétés des relations difonctionelles.
C.R.Acad.Sci. Paris, 230:1999–2000, 1950.

[20]
J. Riguet.
Les relations de Ferrers.
Compte Rendus des Séances hebdomadaires de l'Acadamie
des Sciences (Paris), 232:1729–1730, 1951.

[21]
Gunther Schmidt and Thomas Ströhlein.
Relations and Graphs.
EATCS Monographs on Theoretical Computer Science. Springer-Verlag
Berlin Heidelberg, 1993.

[22]
Ed (Theodorus Sebastiaan) Voermans.
Inductive Datatypes with Laws and Subtyping. A Relational
Technische Universiteit Eindhoven, Department of Mathematics and
Computer Science, 1999.
Ph.D. thesis. DOI:10.6100/IR51.

[23]
Michael Winter.
Decomposing relations into orderings.
In B. Möller R. Berghammer and G. Struth, editors, Proc. of
the Internat. Workshop RelMiCS '7 and 2nd Internat. Workshop on Applications
of Kleene Algebra, in combination with a workshop of the COST Action 274:
TARSKI. Revised Selected Papers, volume 3051 of LNCS, pages 261–272.
Springer-Verlag, 2004.