English
The right inversion sequence of a word ω is defined recursively by: if ω = [], then ris[] = []; otherwise ris(ω.concat i) = (π ω)^{-1} s_i π ω :: ris ω.
Русский
Последовательность правой инверсии слова ω определяется рекурсивно: ris([]) = []; ris(ω concat i) = (π ω)^{-1} s_i π ω за тем ris ω.
LaTeX
$$$\text{ris}(\omega) :\; \begin{cases} ris([]) = [],\ ris(\omega \concat i) = (\pi \omega)^{-1} \cdot s_i \cdot (\pi \omega) \;::\; \text{ris}(\omega)\end{cases}$$$
Lean4
/-- The right inversion sequence of `ω`. The right inversion sequence of a word
$s_{i_1} \cdots s_{i_\ell}$ is the sequence
$$s_{i_\ell}\cdots s_{i_1}\cdots s_{i_\ell}, \ldots,
s_{i_{\ell}}s_{i_{\ell - 1}}s_{i_{\ell - 2}}s_{i_{\ell - 1}}s_{i_\ell}, \ldots,
s_{i_{\ell}}s_{i_{\ell - 1}}s_{i_\ell}, s_{i_\ell}.$$
-/
def rightInvSeq (ω : List B) : List W :=
match ω with
| [] => []
| i :: ω => (π ω)⁻¹ * (s i) * (π ω) :: rightInvSeq ω
