# An example of goal-directed proof

Roland Backhouse111School of Computer Science, University of Nottingham,
Nottingham, UK, Walter Guttmann222Computer Science and Software Engineering ,
University of Canterbury, Christchurch, New Zealand and Michael
Winter333Department of Computer Science, Brock University, St. Catharines, ON,
Canada

###### Abstract

We prove a non-trivial property of relations in a way that emphasises the
creative process in its construction.

##  1 Introduction

In [BDGv22, theorem 139] it is proved that, for all relations $R$, the
equivalence relation $R^{*}\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ can
be reformulated using the identity

$R^{*}\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip
4.49982pt{=}\hskip 4.49982pt(R\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}~{}~{}.$

This identity plays a significant role in algorithms which exploit the
decomposition of a finite graph into an acyclic graph together with a
collection of strongly connected components. (The relation $R$ corresponds to
the edge relation on nodes defined by the graph. Readers unfamiliar with the
notation and/or property are referred to the appendix for a brief summary.)
However, as observed in [BDGv22], the proof left a lot to be desired since it
used the definition of the star operator (reflexive-transitive closure) as a
sum of powers of $R$ together with a quite complicated induction property.
(Attempts we had made to apply fixed-point fusion had failed.)

Recently Guttmann formulated a proof using the inductive definition of $R^{*}$
in point-free relation algebra. Winter made some improvements to Guttmann’s
proof.

Originally, the Guttmann-Winter proof was presented in the traditional
mathematical style: a bottom-up proof that miraculously ends in the final step
with the desired property. In this note, the proof has been rewritten in a way
that emphasises the heuristics that were used to construct the proof. Some
comments on how to present difficult proofs follow the calculations.

##  2 The Proof

The proof is by anti-symmetry of the equality relation. The inclusion

$(R\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip
5.99976pt{\subseteq}\hskip 5.99976ptR^{*}\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$

is straightforward: each step uses well-known properties and is self-
evident444See the appendix for a short summary of the properties that are
needed to complete the proof.. The calculation doesn’t deserve much attention.
The opposite inclusion is much more difficult to prove and that is what this
note is about.

The goal is to prove that

$R^{*}\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip
5.99976pt{\subseteq}\hskip 5.99976pt(R\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}~{}~{}.$

We aim to exploit the inductive definition of $R^{*}$. Because the other
subexpressions are more complicated, we replace them by “$S$” and “$T$”. The
goal becomes to find conditions on $S$ and $T$ such that

$R^{*}\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 5.99976pt{\subseteq}\hskip
5.99976ptT~{}~{}.$

The calculation is guided by the fact that the conditions must be satisfied by
$(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ and
$(R\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}$
but we may be lucky and find weaker conditions. (In fact, we don’t.)

  * Tab overflowTab overflow $R^{*}\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT$$R^{*}\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT$ Tab overflowTab overflowTab overflow $=$ $\\{$ Heyting Galois connection$~{}~{}~{}\\}$Heyting Galois connection$~{}~{}~{}\\}$ $R^{*}\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS{\rightarrow}T$$R^{*}\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS{\rightarrow}T$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ fixed-point definition of $R^{*}$$~{}~{}~{}\\}$fixed-point definition of $R^{*}$$~{}~{}~{}\\}$ $I\hskip 2.99988pt{\cup}\hskip 2.99988ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 7.4997pt{\subseteq}\hskip 7.4997ptS{\rightarrow}T$$I\hskip 2.99988pt{\cup}\hskip 2.99988ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 7.4997pt{\subseteq}\hskip 7.4997ptS{\rightarrow}T$ Tab overflowTab overflowTab overflow $=$ $\\{$ Heyting Galois connection$~{}~{}~{}\\}$Heyting Galois connection$~{}~{}~{}\\}$ $(I\hskip 2.99988pt{\cup}\hskip 2.99988ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T))\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT$$(I\hskip 2.99988pt{\cup}\hskip 2.99988ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T))\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT$ Tab overflowTab overflowTab overflow $=$ $\\{$ distributivity$~{}~{}~{}\\}$distributivity$~{}~{}~{}\\}$ $(I\hskip 1.49994pt{\cap}\hskip 1.49994ptS)\hskip 2.99988pt{\cup}\hskip 2.99988pt(R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS)\hskip 7.4997pt{\subseteq}\hskip 7.4997ptT$$(I\hskip 1.49994pt{\cap}\hskip 1.49994ptS)\hskip 2.99988pt{\cup}\hskip 2.99988pt(R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS)\hskip 7.4997pt{\subseteq}\hskip 7.4997ptT$ Tab overflowTab overflowTab overflow $=$ $\\{$ Galois connection defining “${\cup}$”$~{}~{}~{}\\}$Galois connection defining “${\cup}$”$~{}~{}~{}\\}$ $I\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptT\hskip 7.4997pt{\wedge}\hskip 7.4997ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT$$I\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptT\hskip 7.4997pt{\wedge}\hskip 7.4997ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ introduce condition on $T$ in order to simplify “$I\hskip 1.49994pt{\cap}\hskip 1.49994ptS$”$~{}~{}~{}\\}$introduce condition on $T$ in order to simplify “$I\hskip 1.49994pt{\cap}\hskip 1.49994ptS$”$~{}~{}~{}\\}$ $I\hskip 1.49994pt{\subseteq}\hskip 1.49994ptT\hskip 7.4997pt{\wedge}\hskip 7.4997ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT~{}~{}.$

The introduced condition fits with our goal so we proceed with the second
conjunct. We begin by seeking a condition on $S$ that enables the elimination
of “$S{\rightarrow}$”. To this end, we calculate:

  * Tab overflowTab overflow $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS$ Tab overflowTab overflowTab overflow $\subseteq$ $\\{$ modularity rule$~{}~{}~{}\\}$modularity rule$~{}~{}~{}\\}$ $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T\hskip 5.99976pt{\cap}\hskip 5.99976ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS)$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T\hskip 5.99976pt{\cap}\hskip 5.99976ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS)$ Tab overflowTab overflowTab overflow $\subseteq$ $\\{$ introduce assumption as prelude to cancellation: $\bullet~{}~{}~{}~{}R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS~{}.$$~{}~{}~{}\\}$$\bullet~{}~{}~{}~{}R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS~{}.$$~{}~{}~{}\\}$ $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T\hskip 4.49982pt{\cap}\hskip 4.49982ptS)$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T\hskip 4.49982pt{\cap}\hskip 4.49982ptS)$ Tab overflowTab overflowTab overflow $\subseteq$ $\\{$ (Heyting GC) cancellation$~{}~{}~{}\\}$(Heyting GC) cancellation$~{}~{}~{}\\}$ $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T~{}~{}.$

In this way, we have derived the property that, for all $R$, $S$ and $T$,

(1)
$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip
2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip
5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip
10.49957pt{\Leftarrow}\hskip
10.49957ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip
1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS~{}~{}.$

We now continue the calculation.

  * Tab overflowTab overflow $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptT$ Tab overflowTab overflowTab overflow $=$ $\\{$ the hardest step in the calculation: as a prelude to applying (1),  we exploit the idempotency of set-intersection$~{}~{}~{}\\}$we exploit the idempotency of set-intersection$~{}~{}~{}\\}$ $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 4.49982pt{\cap}\hskip 4.49982ptS\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 7.4997pt{\subseteq}\hskip 7.4997ptT$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 4.49982pt{\cap}\hskip 4.49982ptS\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 7.4997pt{\subseteq}\hskip 7.4997ptT$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ (1) and monotonicity$~{}~{}~{}\\}$(1) and monotonicity$~{}~{}~{}\\}$ $R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 8.99963pt{\wedge}\hskip 8.99963ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 7.4997pt{\subseteq}\hskip 7.4997ptT$$R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 8.99963pt{\wedge}\hskip 8.99963ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 7.4997pt{\subseteq}\hskip 7.4997ptT$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ aiming for fixed-point definition of $T$, use modularity rule$~{}~{}~{}\\}$aiming for fixed-point definition of $T$, use modularity rule$~{}~{}~{}\\}$ $R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 8.99963pt{\wedge}\hskip 8.99963pt(R\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptT^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}){\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptT$$R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 8.99963pt{\wedge}\hskip 8.99963pt(R\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptT^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}){\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptT$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ the left conjunct is satisfied by $S\hskip 2.99988pt{=}\hskip 2.99988pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ ; we postpone introducing this as a condition but note that, with this instantiation, $S\hskip 2.99988pt{=}\hskip 2.99988ptS{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}S$$~{}~{}~{}\\}$but note that, with this instantiation, $S\hskip 2.99988pt{=}\hskip 2.99988ptS{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}S$$~{}~{}~{}\\}$ Tab overflow $R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 7.4997pt{\wedge}\hskip 7.4997ptS\hskip 2.99988pt{=}\hskip 2.99988ptS{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}S\hskip 7.4997pt{\wedge}\hskip 7.4997ptT^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\subseteq}\hskip 1.49994ptS$$R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 7.4997pt{\wedge}\hskip 7.4997ptS\hskip 2.99988pt{=}\hskip 2.99988ptS{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}S\hskip 7.4997pt{\wedge}\hskip 7.4997ptT^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\subseteq}\hskip 1.49994ptS$ Tab overflow $\wedge$ $(R\hskip 1.49994pt{\cap}\hskip 1.49994ptS){\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptT$$(R\hskip 1.49994pt{\cap}\hskip 1.49994ptS){\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptT$$(R\hskip 1.49994pt{\cap}\hskip 1.49994ptS){\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptT$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ fixed-point definition of star$~{}~{}~{}\\}$fixed-point definition of star$~{}~{}~{}\\}$ Tab overflow $R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 7.4997pt{\wedge}\hskip 7.4997ptS\hskip 2.99988pt{=}\hskip 2.99988ptS{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}S\hskip 7.4997pt{\wedge}\hskip 7.4997ptT^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\subseteq}\hskip 1.49994ptS$$R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 7.4997pt{\wedge}\hskip 7.4997ptS\hskip 2.99988pt{=}\hskip 2.99988ptS{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}S\hskip 7.4997pt{\wedge}\hskip 7.4997ptT^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{\subseteq}\hskip 1.49994ptS$ Tab overflow $\wedge$ $T\hskip 2.99988pt{=}\hskip 2.99988pt(R\hskip 1.49994pt{\cap}\hskip 1.49994ptS)^{*}$$T\hskip 2.99988pt{=}\hskip 2.99988pt(R\hskip 1.49994pt{\cap}\hskip 1.49994ptS)^{*}$$T\hskip 2.99988pt{=}\hskip 2.99988pt(R\hskip 1.49994pt{\cap}\hskip 1.49994ptS)^{*}$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ 1st conjunct: fixed-point definition of star 2nd conjunct: reflexivity and transitivity of $(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ 3rd conjunct: $(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip 1.49994pt{\subseteq}\hskip 1.49994ptR^{*}$ and $(R^{*})^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{=}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$$~{}~{}~{}\\}$3rd conjunct: $(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip 1.49994pt{\subseteq}\hskip 1.49994ptR^{*}$ and $(R^{*})^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip 1.49994pt{=}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$$~{}~{}~{}\\}$ $S\hskip 2.99988pt{=}\hskip 2.99988pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip 7.4997pt{\wedge}\hskip 7.4997ptT\hskip 2.99988pt{=}\hskip 2.99988pt(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}~{}~{}.$

In the first calculation, we have proved that

$R^{*}\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 5.99976pt{\subseteq}\hskip
5.99976ptT\hskip 10.49957pt{\Leftarrow}\hskip 10.49957ptI\hskip
1.49994pt{\subseteq}\hskip 1.49994ptT\hskip 7.4997pt{\wedge}\hskip
7.4997ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip
2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip
5.99976ptT~{}~{},$

and, in the final calculation, we have proved that

$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip
2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip
5.99976ptT\hskip 8.99963pt{\Leftarrow}\hskip 8.99963ptS\hskip
2.99988pt{=}\hskip
2.99988pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip
7.4997pt{\wedge}\hskip 7.4997ptT\hskip 2.99988pt{=}\hskip 2.99988pt(R\hskip
1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}~{}~{}.$

Noting that $I\hskip 2.99988pt{\subseteq}\hskip 2.99988pt(R\hskip
1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}$
(the condition on $T$ determined by the first calculation), the conclusion of
the combined calculations is thus

$R^{*}\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 5.99976pt{\subseteq}\hskip
5.99976ptT\hskip 7.4997pt{\Leftarrow}\hskip 7.4997ptS\hskip 2.99988pt{=}\hskip
2.99988pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip
7.4997pt{\wedge}\hskip 7.4997ptT\hskip 2.99988pt{=}\hskip 2.99988pt(R\hskip
1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}~{}~{},$

from which the desired inclusion immediately follows.

##  3 Specific Comments

Before making more general remarks, some comments on the calculation are in
order.

The central problem in both calculations is how to deal with the occurrence of
the intersection operator (“${\cap}$”) on the lower side of an inclusion
(“${\subseteq}$”).

The first calculation is quite straightforward and relatively self-evident:
$R^{*}$ is by definition a least fixed point and it is very common to use
fixed-point induction to establish less obvious properties. (Formally, fixed-
point induction is the rule that a least fixed point is a least prefix point.
In this case, the rule used is that, for all $R$ and $T$,

$R^{*}\hskip 1.49994pt{\subseteq}\hskip 1.49994ptT\hskip
7.4997pt{\Leftarrow}\hskip 7.4997ptI\hskip 1.49994pt{\cup}\hskip
1.49994ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip
2.99988pt{\subseteq}\hskip 2.99988ptT~{}~{}.$

There is a choice of which fixed-point definition of $R^{*}$ to use should the
calculation fail.) The combination of fixed-point induction with the use of a
Galois connection is also very common. In this case, the Galois connection is,
for all $R$, $S$ and $T$,

$R\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 2.99988pt{\subseteq}\hskip
2.99988ptT\hskip 8.99963pt{\equiv}\hskip 8.99963ptR\hskip
2.99988pt{\subseteq}\hskip 2.99988ptS{\rightarrow}T~{}~{}.$

We have called it the “Heyting Galois connection” because it is essentially
the same as the adjunction between ${\wedge}p$ and $p{\Rightarrow}$ (for all
predicates $p$) in intuitionistic logic, the formalisation of which is
generally attributed to Heyting. The problem of the intersection operator is
resolved by simply “shunting” it out of the way and then “shunting” it back.
The remaining steps are relatively self-evident. Since the goal is to rewrite
$T$ as $U^{*}$ for some $U$, the introduction of the condition $I\hskip
1.49994pt{\subseteq}\hskip 1.49994ptT$ on $T$ is an obvious step to take.

The second calculation is also relatively straightforward. The issue that must
be resolved is that the initial calculation has introduced “$S{\rightarrow}$”
on the left side of an inclusion. It is vital that this is eliminated. The
Heyting Galois connection suggests a line of attack: specifically, we have the
cancellation rule: for all $S$ and $T$,

$(S{\rightarrow}T)\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip
4.49982pt{\subseteq}\hskip 4.49982ptT~{}~{}.$

Aiming to apply cancellation, the calculation begins by applying the
modularity rule. In this way, (1) is easily derived.

Undoubtedly, the hardest step of all is the first step of the third
calculation: the step in which idempotency of set intersection is applied to
replace “${\cap}S$” by “${\cap}\hskip 2.99988ptS\hskip 1.49994pt{\cap}\hskip
1.49994ptS$”. Effectively, instead of (1), the equivalent property

(2)
$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip
2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip
5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip
1.49994pt{\cap}\hskip 1.49994ptS\hskip 10.49957pt{\Leftarrow}\hskip
10.49957ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip
1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS$

has been applied. In fact, (2) can be further strengthened by replacing the
inclusion on the consequent by an equality since

  * Tab overflowTab overflow $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 2.99988pt{\cap}\hskip 2.99988ptS$ Tab overflowTab overflowTab overflow $=$ $\\{$ Galois connection defining intersection$~{}~{}~{}\\}$Galois connection defining intersection$~{}~{}~{}\\}$ $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 7.4997pt{\wedge}\hskip 7.4997ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptS$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip 7.4997pt{\wedge}\hskip 7.4997ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptS$ Tab overflowTab overflowTab overflow $=$ $\\{$ $X\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS$ with $X\hskip 1.49994pt{:=}\hskip 1.49994ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T$$~{}~{}~{}\\}$$X\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS$ with $X\hskip 1.49994pt{:=}\hskip 1.49994ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T$$~{}~{}~{}\\}$ $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T$$~{}~{}~{}\\}$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T$$~{}~{}~{}\\}$ $R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)$$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ monotonicity of composition$~{}~{}~{}\\}$monotonicity of composition$~{}~{}~{}\\}$ $T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS{\rightarrow}T$$T\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS{\rightarrow}T$ Tab overflowTab overflowTab overflow $=$ $\\{$ Heyting Galois connection$~{}~{}~{}\\}$Heyting Galois connection$~{}~{}~{}\\}$ $T\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptT$$T\hskip 1.49994pt{\cap}\hskip 1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptT$ Tab overflowTab overflowTab overflow $=$ $\\{$ property of intersection$~{}~{}~{}\\}$property of intersection$~{}~{}~{}\\}$ $\mathsf{true}~{}~{}.$

Thus, by antisymmetry of the subset ordering together with (2),

(3)
$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip
2.99988pt{\cap}\hskip 2.99988ptS\hskip 5.99976pt{=}\hskip
5.99976ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip
1.49994pt{\cap}\hskip 1.49994ptS\hskip 10.49957pt{\Leftarrow}\hskip
10.49957ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip
1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS~{}~{}.$

Although the stronger property (3) is not used directly, its derivation
provides a useful safety check: because we have derived an equality, we know
that simplifying the expression
“$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S{\rightarrow}T)\hskip
2.99988pt{\cap}\hskip 2.99988ptS$” to
“$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip
2.99988pt{\cap}\hskip 2.99988ptS$” does not incur any loss of information (so
long as the condition
$R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip
1.49994ptS\hskip 4.49982pt{\subseteq}\hskip 4.49982ptS$ is satisfied). This is
the raison d’être for the use of the idempotence of set intersection.

##  4 General Comments

So much for the details of the calculation; now more general comments.

Since the earliest days of the development of “correct-by-construction”
program design techniques, goal-directed reasoning has always been a central
theme of “program calculation”. For example, “programming as a goal-oriented
activity” was a specific topic in Gries’s textbook “The Science of
Programming” [Gri81, chapter 14], and broadening the theme to the mathematics
of program construction was the topic of Van Gasteren’s thesis [vG90]. Goal-
directed reasoning is also evident in many of Dijkstra’s “EWD”s (available
from the University of Texas) and many other publications of the last fifty
years.

In contrast, the standard mathematical style is “bottom-up”. That is evident
from the fact that mathematicians almost always use _only-if_ arguments
(implication) as opposed to _if_ arguments (follows-from). In our view, it is
extremely important that the more challenging calculations are presented in a
goal-directed way, as we have tried to do above. It is important because it
helps to teach the creative process underlying the mathematics of program
construction. Of course, when a new theory is being developed the work
proceeds in a bottom-up fashion: one identifies the more straightforward
properties and builds up to properties that are not so obvious. But each step
in the process is an exploration. One seeks properties of a certain type (for
example, distributivity properties) but the exact form of the properties is
not known at the outset. It is vital that we develop a style of calculation
that exposes the creative process and that we communicate this process to our
students.

Many calculations are, of course, straightforward and don’t merit much
discussion. Less interesting calculations are ones where each step
_simplifies_ the expression under consideration (in some sense of the word
“simplify”). In contrast, the calculation above involves several
_complification_ steps. In particular, the step we have singled out as the
hardest of all is a complification step: idempotency is used in the derivation
of (1) to replace an expression of the form $X{\cap}S$ by $X{\cap}S{\cap}S$.
Idempotency is normally presented as a simplification rule whereby the number
of occurrences of the operator in question is reduced. In order to foster
creative calculation, it is also vital to avoid an undue bias in the
presentation of equational properties; equality is after all a symmetric
operator.

In summary, what we have presented is, in our view, a very good example of a
non-trivial calculation that deserves careful study. We hope that, in future,
more effort is spent in research publications and textbooks on elucidating the
process of creative calculation. Historically one argument against
calculations in the style above is the need to save space. But modern
technology —the much reduced reliance on “hard copy”— makes this argument much
less relevant.

## References

  * [BDGv22] 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.
  * [Gri81] David Gries.  The Science of Programming.  Springer-Verlag, 1981.
  * [vG90] Antonetta J.M. van Gasteren.  On the Shape of Mathematical Arguments.  Number 445 in LNCS. Springer-Verlag, 1990.

## Appendix

In the proof we use a number of properties without specific mention. These
properties will be well-known to readers well-versed in relation algebra but
for others may not be so. For this reason, we give a very brief summary of the
relevant properties.

Variables $R$, $S$ and $T$ in the proof all denote homogeneous binary
relations. The set notation we use (“${\subseteq}$”, “${\cap}$” and
“${\cup}$”) has its standard meaning and we do assume familiarity with the
properties of the set operators. (Some readers may not be familiar with the
Heyting Galois connection: the existence of an upper adjoint of ${\cap}\hskip
1.49994ptS$ (for all $S$) is a consequence of the universal distributivity of
set-intersection over set-union.)

Relation composition and converse are denoted by “$\scriptstyle\circ$” and
“${}^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}$”, respectively,
and the identity relation is denoted by $I$. All of intersection, union,
composition and converse are monotonic with respect to the subset ordering.
Also, the logical operator “${\wedge}$” is monotonic with respect to the
“${\Leftarrow}$” relation.

An example of a step that uses a number of the above properties without
specific mention is the final step in the initial calculation. In full detail,
we use the fact that $I{\cap}S\hskip 1.49994pt{\subseteq}\hskip 1.49994ptI$,
that the subset relation is transitive (so $I{\cap}S\hskip
1.49994pt{\subseteq}\hskip 1.49994ptI\hskip 2.99988pt{\wedge}\hskip
2.99988ptI\hskip 1.49994pt{\subseteq}\hskip 1.49994ptT\hskip
4.49982pt{\Rightarrow}\hskip 4.49982ptI{\cap}S\hskip
1.49994pt{\subseteq}\hskip 1.49994ptT$) and that “${\wedge}$” is monotonic
with respect to the “${\Leftarrow}$” relation. Monotonicity of composition is
used when the cancellation rule for the Heyting Galois connection is applied.

Converse is defined by the Galois connection, for all $R$ and $S$,

$R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
2.99988pt{\subseteq}\hskip 2.99988ptS\hskip 7.4997pt{\equiv}\hskip
7.4997ptR\hskip 2.99988pt{\subseteq}\hskip
2.99988ptS^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}$

together with the distributivity property, for all $R$ and $S$,

$(R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}S)^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
4.49982pt{=}\hskip
4.49982ptS^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip
1.49994ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}$

and the property that

$I^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
2.99988pt{=}\hskip 2.99988ptI~{}~{}.$

The modularity rule (aka the Dedekind rule) is used in both its forms: for all
$R$, $S$ and $T$,

$R{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}S\hskip
2.99988pt{\cap}\hskip 2.99988ptT\hskip 7.4997pt{\subseteq}\hskip
7.4997ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}(S\hskip
4.49982pt{\cap}\hskip
4.49982ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip 1.49994ptT)$

and its symmetric counterpart

$R\hskip 2.99988pt{\cap}\hskip
2.99988ptS{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip
7.4997pt{\subseteq}\hskip 7.4997pt(R\hskip
1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip
1.49994ptT^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}\hskip
4.49982pt{\cap}\hskip
4.49982ptS){\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T~{}~{}.$

The rule is important because composition does not distribute over
intersection: it gives a handle on expressions involving both operators where
the intersection is on the lower side of a set inclusion.

$R^{*}$ denotes the reflexive, transitive closure of $R$. The inductive
definition of $R^{*}$ used here555An alternative fixed-point definition
—alluded to in the text— is the direct formalisation of the property that
$R^{*}$ is the least reflexive, transitive relation that contains $R$. is the
property that, for all $T$,

$R^{*}\hskip 2.99988pt{\subseteq}\hskip 2.99988ptT\hskip
7.4997pt{\Leftarrow}\hskip 7.4997ptI\hskip 2.99988pt{\cup}\hskip
2.99988ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T\hskip
4.49982pt{\subseteq}\hskip 4.49982ptT~{}~{}.$

That is, $R^{*}$ is the least prefix point of the function mapping $T$ to
$I\hskip 2.99988pt{\cup}\hskip
2.99988ptR{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}T$. We don’t
directly use the fact that $R^{*}$ is a fixed point of this function but we do
use the (derived) properties that, for all $R$,

$I\hskip 2.99988pt{\subseteq}\hskip 2.99988ptR^{*}\hskip
11.99951pt{\wedge}\hskip 11.99951pt(R^{*})^{*}\hskip 4.49982pt{=}\hskip
4.49982ptR^{*}\hskip 11.99951pt{\wedge}\hskip 11.99951ptR^{*}\hskip
1.49994pt{\mbox{\raisebox{0.86108pt}{$\scriptstyle\circ$}}}\hskip
1.49994ptR^{*}\hskip 5.99976pt{=}\hskip 5.99976ptR^{*}\hskip
11.99951pt{\wedge}\hskip
11.99951pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip
2.99988pt{=}\hskip
2.99988pt(R^{*})^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}~{}~{}.$

We also use the fact that the star operator is monotonic with respect to the
subset ordering. As an example of the explicit use of these properties we
present the proof of the omitted inclusion:

  * Tab overflowTab overflow $(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR^{*}\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$$(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR^{*}\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ Tab overflowTab overflowTab overflow $=$ $\\{$ Galois connection defining intersection$~{}~{}~{}\\}$Galois connection defining intersection$~{}~{}~{}\\}$ $(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip 4.49982pt{\subseteq}\hskip 4.49982ptR^{*}\hskip 10.49957pt{\wedge}\hskip 10.49957pt(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip 4.49982pt{\subseteq}\hskip 4.49982pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$$(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip 4.49982pt{\subseteq}\hskip 4.49982ptR^{*}\hskip 10.49957pt{\wedge}\hskip 10.49957pt(R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*})^{*}\hskip 4.49982pt{\subseteq}\hskip 4.49982pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ Tab overflowTab overflowTab overflow $\Leftarrow$ $\\{$ 1st conjunct: star is monotonic 2nd conjunct: $(R^{*})^{*}\hskip 4.49982pt{=}\hskip 4.49982ptR^{*}$ (with $R\hskip 1.49994pt{:=}\hskip 1.49994ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}$) and star is monotonic $~{}~{}~{}\\}$2nd conjunct: $(R^{*})^{*}\hskip 4.49982pt{=}\hskip 4.49982ptR^{*}$ (with $R\hskip 1.49994pt{:=}\hskip 1.49994ptR^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}$) and star is monotonic $~{}~{}~{}\\}$ $R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR\hskip 11.99951pt{\wedge}\hskip 11.99951ptR\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip 5.99976pt{\subseteq}\hskip 5.99976pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$$R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR\hskip 11.99951pt{\wedge}\hskip 11.99951ptR\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip 5.99976pt{\subseteq}\hskip 5.99976pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ Tab overflowTab overflowTab overflow $=$ $\\{$ Galois connection defining intersection$~{}~{}~{}\\}$Galois connection defining intersection$~{}~{}~{}\\}$ $R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$$R\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip 5.99976pt{\subseteq}\hskip 5.99976ptR\hskip 1.49994pt{\cap}\hskip 1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ Tab overflowTab overflowTab overflow $=$ $\\{$ reflexivity of the subset relation$~{}~{}~{}\\}$reflexivity of the subset relation$~{}~{}~{}\\}$ $\mathsf{true}~{}~{}.$

It is mentioned in the introduction that the identity we have proved is
central to a number of algorithms that exploit graph theory. In such
algorithms, the relation $R$ is the edge relation on nodes of a finite graph:
specifically, two nodes $u$ and $v$ are related by $R$ iff there is an edge in
the corresponding graph from $u$ to $v$. Conversely, two nodes $u$ and $v$ are
related by $R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}$ iff
there is an edge in the graph from $v$ to $u$. The graph corresponding to
$R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}$ is thus the graph
obtained by reversing the edges of the graph corresponding to $R$. Nodes $u$
and $v$ are related by $R^{*}$ iff there is a path from $u$ to $v$ in the
graph, and by
$(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ iff there is
a path from $u$ to $v$ in the graph formed of reversed edges. (Equivalently,
$u$ and $v$ are related by
$(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ if there is
a path from $v$ to $u$ in the graph. Formally, the equivalence is expressed by
the identity
$(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}\hskip
2.99988pt{=}\hskip
2.99988pt(R^{*})^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}}$.)

The relation $R^{*}\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$
holds between nodes $u$ and $v$ if there is both a path from $u$ to $v$ and a
path from $v$ to $u$ in the corresponding graph. Thus $R^{*}\hskip
1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$ is
the equivalence relation that holds between nodes $u$ and $v$ when both are in
the same strongly connected component of the graph.

The relation $R\hskip 1.49994pt{\cap}\hskip
1.49994pt(R^{\mbox{\raisebox{1.42262pt}{$\scriptscriptstyle\cup$}}})^{*}$
holds between nodes $u$ and $v$ iff there is an edge from $u$ to $v$ and a
path from $v$ to $u$. The proven identity thus states that nodes $u$ and $v$
are strongly connected iff there is a path from $u$ to $v$ in the graph
corresponding to this relation. This insight is fundamental to algorithms that
determine the strongly connected components of a graph as well as the
decomposition of a graph into its strongly connected components together with
an acyclic graph connecting such components.


# A Study of Electronic and Magnetic Properties of Transition Metal Trihalides

Shrestha Dutta, Sachin Varma U, Payel Bandyopadhyay and Rudra Banerjee
Department of Physics and Nanotechnology, SRM Institute of Science and
Technology, Kattankulathur, Tamil Nadu, 603203, India<EMAIL_ADDRESS>
###### Abstract

We present the electronic and magnetic structure calculations of VCl3, VBr3,
CrCl3 and CrBr3. The results are obtained by density functional theory with
plane wave basis sets. The transition metal trihalides generally optimize
either in trigonal or monoclinic structures. We have focused on the effect of
symmetry on the electronic and magnetic properties of the systems. We have
found that magnetic moments change considerably depending on the symmetry.
Both CrX3 has shown a bandgap $\approx$ 2eV while the V based systems have
shown half-metallic properties.

##  1 Introduction

The family of transition metal trihalides MX3, where M is a transition metal
cation (M=Ti, V, Cr, Fe, Mo, Ru, Rh, Ir) and X is a halogen anion (X=Cl, Br,
I), have been known for more than 50 years[1, 2]. These compounds have been in
spotlight for some amusing electronic and magnetic properties they exhibit in
their bulk and monolayer phases such as, intrinsic long-range magnetic order
in atomically thin layers[3] as well as its profound applications in
spintronics[4]. With lower dimensionalities of MX3, their bandgap can be tuned
by doping or changing their stacking orientation. This property of MX3 opens
up the opportunity in multi-purpose applications.

Structurally an X-ray and neutron diffraction study ascertained that the
single MX3 crystal adopts a monoclinic AlCl3 structure (space group $C2/m$),
termed as ($\beta$ phase)[5]. $\beta$-phase is found to be lower symmetry
crystallographic phase which is most likely to be found at higher
temperatures. Upon cooling from higher temperature, MX3 layers rearrange
themselves from $\beta$-phase to BiI3-type trigonal(space group R$\bar{3}$)
structure known as $\alpha$-phase. The transition has been reported to be a
first-order phase transition which does not involve any magnetic changes[6].
This phase transition is believed to result from interlayer interactions among
the layers[7, 8]. The interlayer interactions are caused by weak van der
Waals(vdW) bonding[7] between halogen(X) anions hence, known as vdW
structures. The vdW structures reveal themselves to be truly captivating in
the field of materials science due to the presence of intrinsic magnetism and
magnetic anisotropy[9], tunable band gap and high temperature magnetic
ordering[4]. This property of tunable band gap leads to new generation
spintronics, magnetic and magneto-optic applications[10].

Spintronics is a new generation information technology where spins of
electrons are employed as information carriers and also speeds up data
processing. Half metals, spin gapless semiconductors and bipolar magnetic
semiconductors were proposed one after another as probable property in
spintronics[11]. Half metals have been established commendatory in spin
current generation and making spintronic and other nano-electronic devices.
Dirac half metals exhibit a large bandgap in one spin channel and metallic
character in the other. We attempt to figure out half-metals among the family
of transition metals in bulk phases.

For many of the MX3 compounds downscaling the bulk phase to a stable monolayer
is still a challenge. Some studies suggest that monolayers with binding energy
smaller than 0.15 eV per atom might be feasible for exfoliation[12].

(a) R$\bar{3}$

(b) $C2/m$

Figure 1: Bulk structures of MX3 for (1(a))$R\bar{3}$ and (1(b))$C2/m$ space
groups respectively

The physical properties of a few-layer or monolayer structures of such
transition metal MX3 are quite different from that of their bulk structures as
a result of the different screening environments they experience due to the
differences in their effective dimensionality[13].

Various density functional theory(DFT) based studies of bulk and few-layer MX3
for the ground-state have been carried out theoretically[6, 14, 15, 16]. The
difference in electronic screening for bulk and few-layer MX3[17] results in
different electronic bandgaps. These studies cover the interlayer exchange
coupling[18] as well as its dependence on the stacking of layers, possible
ways to stabilize skyrmions[19], and the electric-field switching of the
magnetization[20].

Researchers have detected rich magnetic ground states in the MX3 family.
Magnetism in the ground state of a material is correlated to interlayer vdW
coupling. While vdW coupling originates from distinct stacking orders and the
signature Kagome lattice[21].

In MX3, magnetism originates from the angular momentum associated with
partially filled $d$ orbitals. It has been predicted that the in-plane
magnetic interaction among the transition metal cations is a consequence of
super-exchange through shared coordinating halogen anions. The super-exchange
interaction depends upon factors like orbital occupations and the M-X-M
angle[22].

Among the MX3 series, the Cr and V-based materials are mainly of importance.
CrCl3 has recently been shown to have an unusual magnetic easy axis normal to
the $c$-axis[23]. Further, Ebrahimian et al. has recently shown that the
magnetism in bilayer CrCl3 can be easily controlled by strain and electric
field[24]. Ahmad et al. has shown magnetism of CrCl3 can be controlled by
pressure also[25]. VCl3 has been shown to have half metallicity in 2D[26].
Doping $3d$ transition metal to VCl3 has been shown to tune its electronic and
magnetic properties very recently[27]. High tunnel magnetoresistance and spin
filtering effect are shown in CrBr3[28]. Grzeszczyk et al. has recently shown
exciton magnetization in CrBr3[29].

From the above discussion, it is clear that V and Cr-based MX3 systems play a
significant role in the development of spintronics. Hence, a detailed and
systematic study of these systems from the equivalent theoretical field is
necessary. In this study, we compare the structural and electronic properties
of the possible space groups ($R\bar{3}$ and $C2/m$) of trichlorides and
tribromides of V and Cr using ab-inito density functional theory.

##  2 Computational Details

The Density functional theory (DFT) calculations of vdW layered MX3 have been
brought about with Quantum Espresso[30, 31]. For the exchange-correlation
functional general gradient approximation (GGA) was used in the projector
augmented wave(PAW)[32] pseudopotential. We used the plane-wave cut-off energy
of 320 eV to treat interactions between the valence electrons and ion cores.
The calculations are done in $\Gamma$-point.

Since MX3 is a layered system, vdW corrections were used based on the
semiempirical Grimme’s DFT-D2[33] approach. We need to account for the strong
correlation effects of localized $3d$ electrons of transition metal atoms to
describe their electronic and magnetic properties[34] correctly. In this case,
a simplified version of the DFT+U method suggested by Dudarev[35] was
employed. We set the effective Hubbard interaction parameter Ueff of metal
atoms to 2.7 eV[36, 37]. It is acquired by comparing physical properties
directly.

##  3 Results and Discussions

The MX3 system stabilizes in $R\bar{3}$ and $C2/m$ structures. We have
calculated the ground state of both structures with M=V, Cr and X=Cl, Br. The
optimized lattice parameter(a), optimized M-X bond length(dM-X), interplanar
separation(d0)and magnetic moment per formula unit(f.u.) for VCl3, VBr3, CrCl3
and CrBr3 are shown in Table (1), for FM magnetic ordering. The minimal energy
ground state of the Bravis lattice are shown in bold.

MX3 | a(Å) | dM-X(Å) | d0(Å) |  magnetic moment($\mu_{B}$/f.u.)
---|---|---|---|---
VCl3(R$\bar{3}$) | 6.12 | 2.40 | 4.48 |  2.54(2.0 [38])
VCl3($c2/m$) | 6.26 | 2.40 | 5.08 |  2.32(2.96 [5])
VBr3(R$\bar{3}$) | 6.52 | 2.56 | 4.60 |  2.84(2.6 [39])
VBr3($c2/m$) | 6.62 | 2.57 | 5.15 |  2.46(2.0 [40])
CrCl3(R$\bar{3}$) | 6.08 | 2.38 | 4.32 |  3.59(3.0 [41])
CrCl3($c2/m$) | 6.09 | 2.38 | 5.15 |  5.38 (6.0[42])
CrBr3(R$\bar{3}$) | 6.46 | 2.55 | 4.75 |  3.91(3.10[43])
CrBr3($c2/m$) | 6.39 | 2.56 | 5.34 |  3.90

Table 1: Crystal and magnetic structure information of MX3 compounds. The
magnetic moments in the bracket show their experimental values.

The magnetic moments match closely with their experimental values (given in
the bracket and reference therein). The discrepancies come from the fact that
we have done a $\Gamma$-point only calculation.

In figures (2)-(5), we have discussed the electronic structure of MX3 systems.

(a) $R\bar{3}$

(b) $c2/m$

Figure 2: DOS of VCl3 for (2(a)) $R\bar{3}$ and (2(b)) $c2/m$ structure

The DOS of VCl3 shows prominent states in the majority spin channels and a big
gap in minority spin channel for both $R\bar{3}$(Fig. (2(a))) and $c2/m$(Fig.
(2(b))) structure. This resembles the experimental and previous theoretical
findings[10].

Figure 3: DOS of VBr3 for $R\bar{3}$

VBr3 DOS also shows the same characteristics. These half-metallic behavior of
VCl3 and VBr3 is well known and sustained in bilayer systems[44].

(a) $R\bar{3}$

(b) $c2/m$

Figure 4: DOS of CrCl3 for (4(a)) $R\bar{3}$ and (4(b)) $c2/m$ structure

(a) $R\bar{3}$

(b) $c2/m$

Figure 5: DOS of CrBr3 for (5(a)) $R\bar{3}$ and (5(b)) $c2/m$ structure

With our very small Ueff, the story is completely different for Cr-based
trihalids. Both CrCl3 and CrBr3 show bandgap $\approx 2$eV in all the cases.
This is also well known feature[45]. Though our position of DOS peaks does not
matche the existing literature, the characteristics are well produced with the
small $U_{eff}$. The band gap decreases significantly from CrCl3 to CrBr3.

##  4 Conclusion

Although there are several studies on MX3 systems, there is still a gap in
understanding their stacking, structure, and electronic and magnetic
properties. Due to the recent interest in spintronic applications, it was
necessary to study those materials systematically. In this study, we have
explored the electronic and magnetic properties of CrCl3, CrBr3, VCl3 and VBr3
in bulk phase using DFT with plane wave basis. We have shown that the stacking
and the space group play an important role in their magnetic and electronic
properties. We are confident that this will enable us to design better MX3
based spintronic devices with bilayer and multilayer.

## References

## References

  * [1] Lin J and Miller G J 1993 Inorganic Chemistry 32 1476–1487 URL https://doi.org/10.1021%2Fic00060a025
  * [2] Michel C, Moreau J M and James W J 1971 Acta Crystallographica Section B 27 501–503 URL https://doi.org/10.1107/S0567740871002437
  * [3] Wang Q H, Bedoya-Pinto A et al. 2022 ACS Nano 16 6960–7079 URL https://doi.org/10.1021%2Facsnano.1c09150
  * [4] Basak K, Ghosh M, Chowdhury S and Jana D 2023 Journal of Physics: Condensed Matter 35 233001 URL https://doi.org/10.1088%2F1361-648x%2Facbffb
  * [5] Kratochvílová M, Doležal P, Hovančík D, Pospíšil J, Bendová A, Dušek M, Holý V and Sechovský V 2022 Journal of Physics: Condensed Matter 34 294007 URL https://doi.org/10.1088%2F1361-648x%2Fac6d38
  * [6] Craco L, Carara S S, Shao Y C, Chuang Y D and Freelon B 2021 Physical Review B 103 URL https://doi.org/10.1103%2Fphysrevb.103.235119
  * [7] McGuire M A, Clark G, KC S, Chance W M, Jellison G E, Cooper V R, Xu X and Sales B C 2017 Physical Review Materials 1 URL https://doi.org/10.1103%2Fphysrevmaterials.1.014001
  * [8] McGuire M A, Dixit H, Cooper V R and Sales B C 2015 Chemistry of Materials 27 612–620 URL https://doi.org/10.1021%2Fcm504242t
  * [9] Albaridy R, Manchon A and Schwingenschlögl U 2020 Journal of Physics: Condensed Matter 32 355702 URL https://doi.org/10.1088%2F1361-648x%2Fab8986
  * [10] Tomar S, Ghosh B, Mardanya S, Rastogi P, Bhadoria B, Chauhan Y S, Agarwal A and Bhowmick S 2019 Journal of Magnetism and Magnetic Materials 489 165384 URL https://doi.org/10.1016%2Fj.jmmm.2019.165384
  * [11] Li X and Yang J 2016 National Science Review 3 365–381 URL https://doi.org/10.1093%2Fnsr%2Fnww026
  * [12] Singh A K, Mathew K, Zhuang H L and Hennig R G 2015 The Journal of Physical Chemistry Letters 6 1087–1098 URL https://doi.org/10.1021%2Fjz502646d
  * [13] Huang B, Clark G et al. 2017 Nature 546 270–273 URL https://doi.org/10.1038%2Fnature22391
  * [14] Qin G, Li S and Shao X 2021 AIP Advances 11
  * [15] Pascazio R, Zito J and Infante I 2021 CHIMIA 75 427 URL https://doi.org/10.2533%2Fchimia.2021.427
  * [16] Kvashnin Y O, Rudenko A N, Thunström P, Rösner M and Katsnelson M I 2022 Physical Review B 105 URL https://doi.org/10.1103%2Fphysrevb.105.205124
  * [17] Acharya S, Pashov D, Rudenko A N, Rösner M, van Schilfgaarde M and Katsnelson M I 2022 npj 2D Materials and Applications 6 URL https://doi.org/10.1038%2Fs41699-022-00307-7
  * [18] Soriano D, Cardoso C and Fernández-Rossier J 2019 Solid State Communications 299 113662 URL https://doi.org/10.1016%2Fj.ssc.2019.113662
  * [19] Behera A K, Chowdhury S and Das S R 2019 Applied Physics Letters 114 232402 URL https://doi.org/10.1063%2F1.5096782
  * [20] Morell E S, León A, Miwa R H and Vargas P 2019 2D Materials 6 025020 URL https://doi.org/10.1088%2F2053-1583%2Fab04fb
  * [21] Nharangatt B and Chatanathodi R 2022 Journal of Magnetism and Magnetic Materials 564 170105 URL https://doi.org/10.1016%2Fj.jmmm.2022.170105
  * [22] Khomskii D I 2014 Transition Metal Compounds (Cambridge University Press) URL https://doi.org/10.1017%2Fcbo9781139096782
  * [23] Cai X, Song T et al. 2019 Nano Letters 19 3993–3998 URL https://doi.org/10.1021%2Facs.nanolett.9b01317
  * [24] Ebrahimian A, Dyrdał A and Qaiumzadeh A 2023 Scientific Reports 13 URL https://doi.org/10.1038%2Fs41598-023-32598-1
  * [25] Ahmad A S, Liang Y et al. 2020 Nanoscale 12 22935–22944 URL https://doi.org/10.1039%2Fd0nr04325g
  * [26] Zhou Y, Lu H, Zu X and Gao F 2016 Scientific Reports 6 URL https://doi.org/10.1038%2Fsrep19407
  * [27] Ouettar C, Yahi H, Zanat K and Chibani H 2023 Physica Scripta 98 025814 URL https://doi.org/10.1088%2F1402-4896%2Facb093
  * [28] Liu L, Ye S, He J, Huang Q, Wang H and Chang S 2021 Semiconductor Science and Technology 37 015006 URL https://doi.org/10.1088%2F1361-6641%2Fac3639
  * [29] Grzeszczyk M, Acharya S et al. 2023 Advanced Materials 35 URL https://doi.org/10.1002%2Fadma.202209513
  * [30] Giannozzi P, Baroni S et al. 2009 Journal of Physics: Condensed Matter 21 395502 URL https://doi.org/10.1088%2F0953-8984%2F21%2F39%2F395502
  * [31] Giannozzi P, Andreussi O et al. 2017 Journal of Physics: Condensed Matter 29 465901 URL https://doi.org/10.1088%2F1361-648x%2Faa8f79
  * [32] Kresse G and Joubert D 1999 Physical Review B 59 1758–1775 URL https://doi.org/10.1103%2Fphysrevb.59.1758
  * [33] Grimme S, Antony J, Ehrlich S and Krieg H 2010 The Journal of Chemical Physics 132 154104 URL https://doi.org/10.1063%2F1.3382344
  * [34] Wang Z, Qu S, Xiang H, He Z and Shen J 2020 Materials 13 1805 URL https://doi.org/10.3390%2Fma13081805
  * [35] Dudarev S L, Botton G A, Savrasov S Y, Humphreys C J and Sutton A P 1998 Physical Review B 57 1505–1509 URL https://doi.org/10.1103%2Fphysrevb.57.1505
  * [36] Sun J, Zhong X, Cui W, Shi J, Hao J, Xu M and Li Y 2020 Phys. Chem. Chem. Phys. 22 2429–2436 URL http://dx.doi.org/10.1039/C9CP05084A
  * [37] Olmos R, Alam S, Chang P H, Gandha K, Nlebedim I C, Cole A, Tafti F, Zope R R and Singamaneni S R 2022 Journal of Alloys and Compounds 911 165034 URL https://www.sciencedirect.com/science/article/pii/S0925838822014256
  * [38] Materials Project https://next-gen.materialsproject.org/materials/mp-28117 Accessed: 20 June, 2023
  * [39] Kong T, Guo S, Ni D and Cava R J 2019 Phys. Rev. Mater. 3 084419 URL https://link.aps.org/doi/10.1103/PhysRevMaterials.3.084419
  * [40] Hovančík D, Kratochvílová M, Haidamak T, Doležal P, Carva K, Bendová A, Prokleška J, Proschek P, Míšek M, Gorbunov D I, Kotek J, Sechovský V and Pospíšil J 2023 Robust intralayer antiferromagnetism and tricriticality in a van der waals compound: Vbr3 case
  * [41] Soriano D, Katsnelson M I and Fernández-Rossier J 2020 Nano Letters 20 6225–6234 pMID: 32787171
  * [42] Liu J, Sun Q, Kawazoe Y and Jena P 2016 Phys. Chem. Chem. Phys. 18 8777–8784 URL http://dx.doi.org/10.1039/C5CP04835D
  * [43] Zhang W B, Qu Q, Zhu P and Lam C H 2015 J. Mater. Chem. C 3 12457–12468 URL http://dx.doi.org/10.1039/C5TC02840J
  * [44] Liu L, Yang K, Wang G and Wu H 2020 Journal of Materials Chemistry C URL https://doi.org/10.1039%2Fd0tc03962d
  * [45] Wang H, Eyert V and Schwingenschlögl U 2011 Journal of Physics: Condensed Matter 23 116003 URL https://doi.org/10.1088%2F0953-8984%2F23%2F11%2F116003