Prove equivalence between properties of relations using fixpoint calculus

Question

The problem

Let $a$ be a binary endorelation of some countable set $S$, i.e. $a \subseteq S \times S$ .

I need to show that the following properties are equivalent:

1. $ (a^*)^{-1} ; a^* \subseteq a^* ; (a^*)^{-1} $
2. $(a \cup a^{-1})^* = a^* ; (a^*)^{-1}$

Where $(-)^*$ is the transitive-reflexive closure, $(-)^{-1}$ is the converse relation ($x R y \iff y R^{-1}x$) and $;$ is the usual relation composition.

Fixed point induction

I need to use Fixed Point Induction (Knaster-Tarski) in the proof, at least for the part (1) $\implies$ (2). Given that $a^* = \mu x . id_S \cup (a ; x)$, by Knaster-Tarski if we can show that $a^* ; (a^*)^{-1}$ is a pre-fixed point of the function $F(x) = id_S \cup (a \cup a^{-1}) ; x$ we will have also proven $(a \cup a^{-1})^* \leq a^* ; (a^*)^{-1}$. That is:

$$ id_S \cup (a \cup a^{-1}); (a^* ; (a^{*})^{-1}) \subseteq a^* ; (a^{*})^{-1} \implies (a \cup a^{-1})^* \leq a^* ; (a^*)^{-1}$$

What I then noticed is that, since it is evident that $id_S \subseteq a^* ; (a^{*})^{-1}$, we only need to prove:

$$ (a \cup a^{-1}); (a^* ; (a^{*})^{-1}) \subseteq a^* ; (a^{*})^{-1}$$

From which I'm absolutely stuck. I would appreciate even only a proof of the above formula, not necessarily the whole solution.

Answer 1

We first prove how (1) implies (2). Let $a$ be an endorelation on $A$ and assume $(a \cup a^{-1})^* = a^*; {a^{-1}}^*$. To prove that $a$ satisfies (1) it is now enough to prove ${a^{-1}}^*;a^* \leq (a \cup a^{-1})^*$. By the Kleene star being monotonic, hence laxly join preserving, we have $a^* \cup {a^{-1}}^* \leq (a \cup a^{-1})^*$. We now show that ${a^{-1}}^*;a^* \leq a^* \cup {a^{-1}}^*$. Let $t {{a^{-1}}^*;a^*} s$. That is, there exist two finite integers $m$, $n$: $$ t\,\, {\underbrace{a^{-1} ; ... ; a^{-1}}_n;{\underbrace{a ; ... ; a}_m}} \,\,s $$ We now distinguish three cases. If $m > n$ then $ t\,\, {a^*}\,\, s$, by repeated cancellation of $a$ and its converse. Similarly, if $m < n$ then $t\,\, {{a^{-1}}^*}\,\, s$. Finally, if $m = n$, we have $t\,\, {id}\,\, s$. We conclude by the following observation: $$ \begin{matrix} a^* \leq a^* \cup {a^{-1}}^*\\ {a^{-1}}^* \leq a^* \cup {a^{-1}}^*\\ id \leq a^* \cup {a^{-1}}^* \end{matrix} \text{ implies } t \,\, {a^* \cup {a^{-1}}^*} \,\, s $$ In conclusion: $$ {a^{-1}}^*;a^* \leq a^* \cup {a^{-1}}^* \leq (a \cup a^{-1})^* = a^*; {a^{-1}}$$

We now show that (1) implies (2). Assume ${a^{*}}^{-1} ; a^{*} \leq a^{*} ; {a^{*}}^{-1}$. In order to prove that $a$ is (2) we need to show the following inequalities: $$ a^*; {a^{-1}}^* \leq (a \cup a^{-1})^* $$ $$ (a \cup a^{-1})^* \leq a^*; {a^{-1}}^* $$

• By the monotonicity of the Kleene star the following holds: $$a^*; {a^{-1}}^* \leq (a \cup a^{-1})^* ; (a \cup a^{-1})^*$$ And by $R^*;R^* \leq R^*$ we conclude: $a^*; {a^{-1}}^* \leq (a \cup a^{-1})^*$
• By fixed point induction, as $b^* = \mu x .id \cup b;x$, we have: $$ id \cup (a \cup a^{-1}); a^*; {a^{-1}}^* \leq a^*; {a^{-1}}^* \implies (a \cup a^{-1})^* \leq a^*; {a^{-1}}^* $$ Firstly we have $id \leq id ; id \leq a^* ; {a^{-1}}^*$ hence we only need to prove: $$ (a \cup a^{-1}); a^*; {a^{-1}}^* \leq a^*; {a^{-1}}^* $$ Which can be proven as follows: $$ \begin{aligned} (a \cup a^{-1}); a^*; {a^{-1}}^* &= a ; a^*; {a^{-1}}^* \cup a^{-1} ; a^*; {a^{-1}}^* \\ &\leq a^*; {a^{-1}}^* \cup a^{-1} ; a^*; {a^{-1}}^* &{a; a^* \leq a^*\text{ and monot. };} \\ &\leq a^*; {a^{-1}}^* \cup {a^{-1}}^* ; a^*; {a^{-1}}^* &{a^{-1} \leq {a^{-1}}^*\text{ and monot. };} \\ &\leq a^*; {a^{-1}}^* \cup {a^{-1}}^* ; a^*; {a^{-1}}^* &{\text{Hp.}} \\ &\leq a^*; {a^{-1}}^* \cup {a}^* ; {a^{-1}}^*; {a^{-1}}^* &{\text{Hp.}} \\ &\leq a^*; {a^{-1}}^* \cup {a}^* ; {a^{-1}}^* &{R ; R \leq R} \\ &= a^*; {a^{-1}}^* \end{aligned} $$