KleeneAlgebra.tex

\chapter{Theory Of Kleene Algebra In Agda}
Kleene algebra is an algebraic structure named after Stephen Cole Kleene, for
his contribution in the field of finite automata and regular expressions. Kleene
algebras are used in various fields such as relational algebra, automata and
formal theory, design and analysis of algorithms, program analysis and
compiler optimization \cite{kozen1997kleene}. Kleene algebra generalizes
operations from regular expressions. The axiomization of the algebra of regular
events was proposed in 1966 but it was in 1984, that a completeness theorem
for relational algebra with a proper subclass of Kleene algebra was given
\cite{kozen1994completeness}. Although there are some differences in axioms of
Kleene algebra, in this chapter we consider the axioms defined in
\cite{kozen1994completeness}

\section{Definition}
A set $S$ with two binary operations $+$ and $*$ generally called addition and
multiplication such that $(S,+,0)$ is a commutative monoid, $(S,*,1)$ is a
monoid, and $*$ distributes over $+$ with annihilating zero is called a
semiring. A semiring satisfying idempotent property is called idempotent
semiring. An idempotentSemiring $(S,+,*,0,1)$ should satisfy the following
axioms:
\begin{itemize}
  \item $(S,+,0)$ is a commutative monoid:
  \begin{itemize}
    \item Associativity: $\forall x,y,z \in S, x + (y + z) = (x + y) + z$
    \item Identity: $\forall x \in S, (x + 0) = x = (0 + x)$
    \item Commutativity: $\forall x,y \in S, (x + y) = (y + x)$
  \end{itemize}
  \item $(S,*,1)$ is a monoid:
  \begin{itemize}
    \item Associativity: $ \forall x,y,z \in S, x * (y*z) = (x*y)*z$
    \item Identity: $\forall x \in S, (x * 1) = x = (1 * x)$
  \end{itemize}
  \item Idempotent: $\forall x \in S, (x + x) = x$
  \item Multiplication distributes over addition: \(\forall x , y , z \in S, (x * (y + z)) = (x * y) + (x
  * z)\) and \( (x + y) * z = (x * z) + (y * z) \)
  \item Annihilating zero: \(\forall x \in S, (x * 0) = 0 = (0 * x)\)
\end{itemize}

A Kleene Algebra over set S that is an idempotent semiring with unary operator
$(^{*})$ that satisfies the following axioms.
\begin{equation}\label{eq_starrightexpansive}
\forall\ x\ \in\ S:\ 1\ +\ (x\ ∙\ (x^{*}))\ \leq\ x^{*}
\end{equation}
\begin{equation}\label{eq_starleftexpansive}
\forall\ x\ \in\ S:\ 1\ +\ (x^{*})\ ∙\ x\ \leq\ x^{*}
\end{equation}
\begin{equation}\label{eq_starleftdestructive}
\forall\ a,\ b,\ x\ \in\ S:\ \text{If} \ b\ +\ a\  ∙\ x\ \leq\ x\ \text{then},\ (a^{*})\ ∙\ b\ \leq\ x
\end{equation}
\begin{equation}\label{eq_starrightdestructive}
\forall\ a,\ b,\ x\ \in\ S:\ \text{If} \ b\ +\ x\ ∙\ a\ \leq\ x \  \text{then},\ b\ ∙\ (a^{*})\ \leq\ x
\end{equation}
where $\leq$ refers to the natural partial order: 
\[a \leq b \leftrightarrow a + b = b\] In Agda we define the partial order
axioms in terms of equality. \footnote{Kleene algebra with partial and pre-order
structures are defined in "Algebra.Ordered.Structures" in Agda standard
library.}

\begin{minted}[breaklines,samepage]{Agda}
StarRightExpansive : A → Op₂ A → Op₂ A → Op₁ A → Set _
StarRightExpansive e _+_ _∙_ _* = ∀ x → (e + (x ∙ (x *))) + (x *) ≈ (x *)
\end{minted}
\begin{minted}[breaklines,samepage]{Agda}
StarLeftExpansive : A → Op₂ A → Op₂ A → Op₁ A → Set _
StarLeftExpansive e _+_ _∙_ _* = ∀ x → (e + ((x *) ∙ x)) + (x *) ≈ (x *)
\end{minted}
\begin{minted}[breaklines,samepage]{Agda}
StarExpansive : A → Op₂ A → Op₂ A → Op₁ A → Set _
StarExpansive e _+_ _∙_ _* = (StarLeftExpansive e _+_ _∙_ _*) × (StarRightExpansive e _+_ _∙_ _*)
\end{minted}
\begin{minted}[breaklines,samepage]{Agda}
StarLeftDestructive : Op₂ A → Op₂ A → Op₁ A → Set _
StarLeftDestructive _+_ _∙_ _* = ∀ a b x → (b + (a ∙ x)) + x ≈ x → ((a *) ∙ b) + x ≈ x
\end{minted}
\begin{minted}[breaklines,samepage]{Agda}
StarRightDestructive : Op₂ A → Op₂ A → Op₁ A → Set _
StarRightDestructive _+_ _∙_ _* = ∀ a b x → (b + (x ∙ a)) + x ≈ x → (b ∙ (a *)) + x ≈ x
\end{minted}
\begin{minted}[breaklines,samepage]{Agda}
StarDestructive : Op₂ A → Op₂ A → Op₁ A → Set _
StarDestructive _+_ _∙_ _* = (StarLeftDestructive _+_ _∙_ _*) × (StarRightDestructive _+_ _∙_ _*)
\end{minted}

The Kleene algebra can be defined using idempotent semiring. In the Agda
standard library, $+$ and $*$ operations are used to denote addition and
multiplication. To keep the same template, ⋆ is selected to denote the unary
star operation. 

\begin{minted}[breaklines,samepage]{Agda}
record IsKleeneAlgebra (+ * : Op₂ A) (⋆ : Op₁ A) (0# 1# : A) : Set (a ⊔ ℓ) where
  field
    isIdempotentSemiring  : IsIdempotentSemiring + * 0# 1#
    starExpansive         : StarExpansive 1# + * ⋆
    starDestructive       : StarDestructive + * ⋆

  open IsIdempotentSemiring isIdempotentSemiring public
\end{minted}
In the above definition, \inline{IsKleeneAlgebra} structure is defined as a
record type with three fields. Since \inline{*} is used to denote binary
multiplication operation, we use \inline{⋆} for the unary star operator. The
field \inline{isIdempotentSemiring} makes an idempotent semiring with the
operator $+,*,0\#, \text{ and } 1\#$. Fields \inline{starExpansive} and
\inline{starDestructive} are used to give the axioms for the star operator. We
open \inline{isIdempotentSemiring} to bring its definitions into scope.

\section{Homomorphism}
A homomorphism of Kleene algebra is a function between two Kleene algebras that
preserves the algebraic structure of the underlying semiring and the Kleene star
operation. Homomorphisms of Kleene algebra are important in the study of regular
languages and automata, as they allow us to relate the behavior of different
automata and regular expressions to each other.

For Kleene algebra $(K_1,+_1,*_1,^{*_1},0_1,1_1)$ and
$(K_2,+_2,*_2,^{*_2},0_2,1_2)$, the homomorphism $f: K_1 \rightarrow K_2$ can be
defined by using the homomorphism of structure idempotent semiring and
preserving the $^{*}$ operator. Formally, $f: K_1 \rightarrow K_2$ is a
structure-preserving map such that:
\begin{itemize}
\item $f$ preserves binary operation $+$: $f(x +_1 y) = f(x) +_2 f(y)$
\item $f$ preserves binary operation $*$: $f(x *_1 y) = f(x) *_2 f(y)$
\item $f$ preserves additive identity: $f(0_1) = 0_2$
\item $f$ preserves multiplicative identity: $f(1_1) = 1_2$
\item $f$ preserves star operation: $f(x^{*_1}) = f(x)^{*_2}$
\end{itemize}

\begin{minted}[samepage,breaklines]{Agda}
record IsKleeneAlgebraHomomorphism (⟦_⟧ : A → B) : Set (a ⊔ ℓ₁ ⊔ ℓ₂) where
field
  isSemiringHomomorphism : IsSemiringHomomorphism ⟦_⟧
  ⋆-homo :  Homomorphic₁ ⟦_⟧ _⋆₁ _⋆₂

open IsSemiringHomomorphism isSemiringHomomorphism public
\end{minted}

By characterizing these constructs in Kleene algebra, researchers can gain
insights into the structural properties between two regular languages.

\section{Composition of Homomorphism}
If $f$ is a homomorphism such that $f\ :\ a \ \rightarrow \ b$ and $g$ is a
homomorphism such that $g\ :\ b\ \rightarrow \ c$, then composition of
homomorphisms can be defined as $g \ ∘\ f\ :\ a \ \rightarrow \ c$.

\begin{minted}[samepage,breaklines]{Agda}
isKleeneAlgebraHomomorphism
: IsKleeneAlgebraHomomorphism K₁ K₂ f
→ IsKleeneAlgebraHomomorphism K₂ K₃ g
→ IsKleeneAlgebraHomomorphism K₁ K₃ (g ∘ f)
isKleeneAlgebraHomomorphism f-homo g-homo = record
{ isSemiringHomomorphism = isSemiringHomomorphism ≈₃-trans F.isSemiringHomomorphism G.isSemiringHomomorphism
; ⋆-homo              = λ x → ≈₃-trans (G.⟦⟧-cong (F.⋆-homo x)) (G.⋆-homo (f x))
} where module F = IsKleeneAlgebraHomomorphism f-homo; module G = IsKleeneAlgebraHomomorphism g-homo
\end{minted}

In the above quasigroup homomorphism composition, \inline{f} is a homomorphism
from Kleene algebra $K₁$ to $K₂$, \inline{g} is a homomorphism from Kleene
algebra $K₂$ to $K₃$. The proof for homomorphism composition is homomorphic is
given using the proof for semiring homomorphism composition. \inline{⋆-homo}
gives composition for star operator using transitive relation such that: 
\[g (f (x^{*_1})) = (g (f x) ^{*_2}) \text{ and } (g (f x) ^{*_2}) = (g (f x))^{*_3}\] 
\[\Rightarrow g (f (x^{*_1})) = (g (f x))^{*_3}\] The composition of
monomorphism and isomorphism can be defined similar to homomorphism and can be
found in the Agda standard library.

\section{Product Algebra}
The product of two Kleene algebra structures in Agda is defined using the
product definition of idempotent semiring structure as:

\begin{minted}[breaklines,samepage]{Agda}
KleeneAlgebra : KleeneAlgebra a ℓ₁ → KleeneAlgebra b ℓ₂ → KleeneAlgebra (a ⊔ b) (ℓ₁ ⊔ ℓ₂)
KleeneAlgebra K L = record
{ isKleeneAlgebra = record
    { isIdempotentSemiring = IdempotentSemiring.isIdempotentSemiring (idempotentSemiring K.idempotentSemiring L.idempotentSemiring)
    ; starExpansive = (λ x → (K.starExpansiveˡ  , L.starExpansiveˡ) <*> x)
                    , (λ x → (K.starExpansiveʳ  , L.starExpansiveʳ) <*> x)
    ; starDestructive = (λ a b x x₁ → (K.starDestructiveˡ  , L.starDestructiveˡ) <*> a <*> b <*> x <*> x₁)
                      , (λ a b x x₁ → (K.starDestructiveʳ  , L.starDestructiveʳ) <*> a <*> b <*> x <*> x₁)
    }
} where module K = KleeneAlgebra K;  module L = KleeneAlgebra L
\end{minted}

where \inline{idempotentSemiring} is the product of two idempotent semiring
structures.
\section{Properties}
Property of union $(a+b)^{*} = a^{*}*(b*(a^{*}))^{*}$ require monotonicity to
prove \cite{broda2014kleene}. Since the identities of Kleene algebra with
partial order are defined in terms of equality ($a \leq b \leftrightarrow a + b
= b$), these properties become non-provable. For the scope of the thesis, we
omit discussing properties that require monotonicity. In this section, we prove
some properties of Kleene algebra. The proofs are adapted from
\cite{kozen1997kleene}. 

Let $(K, +, *, ^{*}, 0, 1)$ be a Kleene algebra then:
\begin{enumerate}
  \setlength{\itemindent}{0em}
  \item 
\[1\ +\ x^{*}\ =\ x^{*}\] 
\[x\ +\ x^{*}\ =\ x^{*}\]
This property allows for the repetition and concatenation of language
constructs. An application of this property is found in the development of
pattern-matching algorithms in text processing and computational linguistics
\cite{ulus2018pattern}.

\begin{minted}[breaklines,samepage]{Agda}
1+x⋆≈x⋆ : ∀ x → 1# + x ⋆ ≈ x ⋆
1+x⋆≈x⋆ x = begin
  1# + x ⋆                    ≈⟨ +-congˡ (sym(starExpansiveʳ x)) ⟩ 
  1# + (1# + x * x ⋆ + x ⋆)   ≈⟨ +-congˡ (+-assoc 1# (x * x ⋆) (x ⋆)) ⟩ 
  1# + (1# + (x * x ⋆ + x ⋆)) ≈⟨ sym(+-assoc 1# 1# (x * x ⋆ + x ⋆)) ⟩ 
  1# + 1# + (x * x ⋆ + x ⋆)   ≈⟨ +-congʳ (+-idem 1#) ⟩ 
  1# + (x * x ⋆ + x ⋆)        ≈⟨ sym(+-assoc 1# (x * x ⋆) (x ⋆) ) ⟩ 
  1# + x * x ⋆ + x ⋆          ≈⟨ starExpansiveʳ x ⟩ 
  x ⋆                         ∎
\end{minted}

\begin{minted}[breaklines,samepage]{Agda}
x+x⋆≈x⋆ : ∀ x → x + x ⋆ ≈ x ⋆
x+x⋆≈x⋆ x = begin
  x + x ⋆                         ≈⟨ +-congˡ(sym(starExpansiveʳ x)) ⟩
  x + (1# + x * x ⋆ + x ⋆)        ≈⟨ +-congʳ(sym(*-identityʳ x)) ⟩ 
  x * 1# + (1# + x * x ⋆ + x ⋆)   ≈⟨ +-congˡ((+-assoc _ _ _)) ⟩ 
  x * 1# + (1# + (x * x ⋆ + x ⋆)) ≈⟨ sym(+-assoc _ _ _ ) ⟩ 
  x * 1# + 1# + (x * x ⋆ + x ⋆)   ≈⟨ +-congʳ(+-comm (x * 1#) 1#) ⟩ 
  1# + x * 1# + (x * x ⋆ + x ⋆)   ≈⟨ +-assoc _ _ _ ⟩ 
  1# + (x * 1# + (x * x ⋆ + x ⋆)) ≈⟨ +-congˡ(sym (+-assoc _ _ _)) ⟩ 
  1# + ((x * 1# + x * x ⋆) + x ⋆) ≈⟨ +-congˡ(+-congʳ(sym(distribˡ _ _ _))) ⟩ 
  1# + (x * (1# + x ⋆) + x ⋆)     ≈⟨ +-congˡ(+-congʳ(*-congˡ(1+x⋆≈x⋆ x))) ⟩ 
  1# + (x * x ⋆ + x ⋆)            ≈⟨ sym(+-assoc _ _ _) ⟩ 
  1# + x * x ⋆ + x ⋆              ≈⟨ starExpansiveʳ x ⟩ 
  x ⋆                             ∎
\end{minted}
\item
The absorption property is used in the simplification of
regular expressions.

\[x * x^{*} + x^{*} = x^{*}\]
\[x^{*}\  + x^{*}\ *\ x\ =\ x^{*}\] 

They are used in the analysis of language hierarchies and the development of
language recognition algorithms in natural language processing and computational
linguistics \cite{desharnais2004modal}.

\begin{minted}[breaklines,samepage]{Agda}
xx⋆+x⋆≈x⋆ : ∀ x → x * x ⋆ + x ⋆ ≈ x ⋆
xx⋆+x⋆≈x⋆ x = begin
  x * x ⋆ + x ⋆                    ≈⟨ +-comm _ _ ⟩ 
  x ⋆ + x * x ⋆                    ≈⟨ +-congʳ (sym(starExpansiveʳ x)) ⟩
  1# +  x * x ⋆ + x ⋆ + x * x ⋆    ≈⟨ +-assoc _ _ _ ⟩ 
  1# + x * x ⋆ + (x ⋆ + x * x ⋆)   ≈⟨ +-congˡ(+-comm (x ⋆) ( x * x ⋆)) ⟩
  1# + x * x ⋆ + (x * x ⋆ + x ⋆)   ≈⟨ +-assoc _ _ _ ⟩ 
  1# + (x * x ⋆ + (x * x ⋆ + x ⋆)) ≈⟨ +-congˡ (sym (+-assoc _ _ _)) ⟩ 
  1# + (x * x ⋆ + x * x ⋆ + x ⋆)   ≈⟨ +-congˡ (+-congʳ (+-idem _)) ⟩ 
  1# + (x * x ⋆ + x ⋆)             ≈⟨ sym( +-assoc 1# (x * x ⋆) (x ⋆) ) ⟩ 
  1# + x * x ⋆ + x ⋆               ≈⟨ starExpansiveʳ x ⟩ 
  x ⋆                              ∎
\end{minted}

\begin{minted}[breaklines,samepage]{Agda}
x⋆+x⋆x≈x⋆ : ∀ x → x ⋆ + x ⋆ * x ≈ x ⋆
x⋆+x⋆x≈x⋆ x = begin
  x ⋆ + x ⋆ * x         ≈⟨ +-congʳ (sym (1+x⋆≈x⋆ x)) ⟩
  1# + x ⋆ + x ⋆ * x    ≈⟨ +-assoc _ _ _ ⟩
  1# + (x ⋆ + x ⋆ * x)  ≈⟨ +-congˡ (+-comm (x ⋆) (x ⋆ * x)) ⟩
  1# + (x ⋆ * x + x ⋆)  ≈⟨ sym (+-assoc _ _ _) ⟩
  1# + x ⋆ * x + x ⋆    ≈⟨ starExpansiveˡ x ⟩ 
  x ⋆                   ∎
\end{minted}
\item
Zero and one element By the zero element property simplifies to $x^{*}$. That is
the zero (and one) element does not alter the result when combined with language
elements and their Kleene star. These properties are also used in regular
expressions and pattern-matching algorithms.

\[0\ + x\ +\ x^{*}\ =\ x^{*}\]
\[1\ + x\ +\ x^{*}\ =\ x^{*} \]

\begin{minted}[breaklines,samepage]{Agda}
0+x+x⋆≈x⋆ : ∀ x → 0# + x + x ⋆ ≈ x ⋆
0+x+x⋆≈x⋆ x = begin
  0# + x + x ⋆    ≈⟨ +-assoc 0# x (x ⋆) ⟩
  0# + (x + x ⋆)  ≈⟨ +-identityˡ ((x + x ⋆)) ⟩
  (x + x ⋆)       ≈⟨ x+x⋆≈x⋆ x ⟩
  x ⋆             ∎

\end{minted}
\begin{minted}[breaklines,samepage]{Agda}
1+x+x⋆≈x⋆ : ∀ x → 1# + x + x ⋆ ≈ x ⋆
1+x+x⋆≈x⋆ x = begin
  1# + x + x ⋆   ≈⟨ +-assoc _ _ _ ⟩ 
  1# + (x + x ⋆) ≈⟨ +-congˡ (x+x⋆≈x⋆ x) ⟩ 
  1# + x ⋆       ≈⟨ 1+x⋆≈x⋆ x ⟩ 
  x ⋆            ∎
\end{minted}
\item
To prove the property: \[x^{*}\ *\ x^{*}\ +\ x^{*} =\ x^{*}\] We need to prove that $x^{*} + x *
x^{*} + x^{*} ≈ x^{*}$. This proof can be used in Agda as shown in the proof
below.

\begin{minted}[breaklines,samepage]{Agda}
x⋆+xx⋆+x⋆≈x⋆ : ∀ x → x ⋆ + x * x ⋆ + x ⋆ ≈ x ⋆
x⋆+xx⋆+x⋆≈x⋆ x = begin
  x ⋆ + x * x ⋆ + x ⋆   ≈⟨ +-assoc _ _ _ ⟩ 
  x ⋆ + (x * x ⋆ + x ⋆) ≈⟨ +-congˡ (+-comm _ _) ⟩
  x ⋆ + (x ⋆ + x * x ⋆) ≈⟨ sym (+-assoc _ _ _) ⟩ 
  x ⋆ + x ⋆ + x * x ⋆   ≈⟨ +-congʳ (+-idem _) ⟩ 
  x ⋆ + x * x ⋆         ≈⟨ +-comm _ _ ⟩
  x * x ⋆ + x ⋆         ≈⟨  xx⋆+x⋆≈x⋆ x  ⟩ 
  x ⋆                   ∎
x⋆x⋆+x⋆≈x⋆ : ∀ x → x ⋆ * x ⋆ + x ⋆ ≈ x ⋆
x⋆x⋆+x⋆≈x⋆ x =  starDestructiveˡ x (x ⋆) (x ⋆) (x⋆+xx⋆+x⋆≈x⋆ x) 
\end{minted}

\begin{comment}
  \item $1 \ +\ x^{*}\ *\ x^{*}\ + x^{*}\ =\ x^{*}$
\begin{minted}[breaklines,samepage]{Agda}
1+x⋆x⋆+x⋆≈x⋆ : ∀ x → 1# + x ⋆ * x ⋆ + x ⋆ ≈ x ⋆
1+x⋆x⋆+x⋆≈x⋆ x = begin
  1# + x ⋆ * x ⋆ + x ⋆   ≈⟨ +-assoc _ _ _ ⟩ 
  1# + (x ⋆ * x ⋆ + x ⋆) ≈⟨ +-congˡ (x⋆x⋆+x⋆≈x⋆ x) ⟩
  1# + x ⋆               ≈⟨ 1+x⋆≈x⋆ x ⟩
  x ⋆                    ∎
\end{minted}
\end{comment}

Here are some other notable properties of Kleene algebra along with their proofs
in Agda.

\item $\text{If}\ x\ =\ y\ \text{then},\ 1\ +\ x\ *\ y^{*}\ + \ y^{*}\ =\ y^{*}$

\begin{minted}[breaklines,samepage]{Agda}
x≈y⇒1+xy⋆≈y⋆ : ∀ x y → x ≈ y → 1# + x * y ⋆ + y ⋆ ≈ y ⋆
x≈y⇒1+xy⋆≈y⋆ x y eq = begin
  1# + x * y ⋆ + y ⋆   ≈⟨ +-assoc _ _ _ ⟩
  1# + (x * y ⋆ + y ⋆) ≈⟨ +-congˡ (+-congʳ (*-congʳ (eq))) ⟩
  1# + (y * y ⋆ + y ⋆) ≈⟨ sym(+-assoc _ _ _) ⟩ 
  1# + y * y ⋆ + y ⋆   ≈⟨ starExpansiveʳ y ⟩ 
  y ⋆                  ∎
\end{minted}

\item $\text{If}\ a\ *\ x\ =\ x\ *\ b\ \text{then}, a^{*}\ *\ x\ +\ x\ *\ b^{*} =\ x\ *\ b^{*}$

\begin{minted}[breaklines,samepage]{Agda}
ax≈xb⇒x+axb⋆+x⋆b≈xb⋆ : ∀ x a b → a * x ≈ x * b → (x + a * (x * b ⋆)) + x * b ⋆ ≈ x * b ⋆
ax≈xb⇒x+axb⋆+x⋆b≈xb⋆ x a b eq = begin
  (x + a * (x * b ⋆)) + x * b ⋆       ≈⟨ +-congʳ( +-congˡ (sym(*-assoc a x (b ⋆)))) ⟩
  (x + a * x * b ⋆)  + x * b ⋆        ≈⟨ +-congʳ(+-congʳ (sym (*-identityʳ x))) ⟩
  (x * 1# + a * x * b ⋆) + x * b ⋆    ≈⟨ +-congʳ (+-congˡ (*-congʳ (eq))) ⟩
  (x * 1# + x * b * b ⋆) + x * b ⋆    ≈⟨ +-congʳ (+-congˡ ( *-assoc _ _ _)) ⟩
  (x * 1# + x * (b * b ⋆)) + x * b ⋆  ≈⟨ +-congʳ(sym (distribˡ x 1# (b * b ⋆))) ⟩ 
  x * ( 1# + b * b ⋆) + x * b ⋆       ≈⟨ sym(distribˡ _ _ _) ⟩ 
  x * (1# + b * b ⋆ + b ⋆)            ≈⟨ *-congˡ (starExpansiveʳ b) ⟩ 
  x * b ⋆                             ∎ 

ax≈xb⇒a⋆x≈xb⋆ : ∀ x a b → a * x ≈ x * b → a ⋆ * x + x * b ⋆ ≈ x * b ⋆
ax≈xb⇒a⋆x≈xb⋆ x a b eq = starDestructiveˡ a x ((x * b ⋆)) (ax≈xb⇒x+axb⋆+x⋆b≈xb⋆ x a b eq)
\end{minted}


\item $(x\ *\ y)^{*}\ *\ x\ +\ x\ *\ (y\ *\ x)^{*} =\ x\ *\ (y\ *\ x)^{*}$

\begin{minted}[breaklines,samepage]{Agda}
[xy]⋆x+x[yx]⋆≈x[yx]⋆ : ∀ x y → (x * y) ⋆ * x + x * (y * x) ⋆ ≈ x * (y * x) ⋆
[xy]⋆x+x[yx]⋆≈x[yx]⋆ x y = ax≈xb⇒a⋆x≈xb⋆ x (x * y) (y * x) (*-assoc x y x)
\end{minted}

\end{enumerate}