2.1 The min-max tree of a sequence
A min-max tree over a type \(T\) is the inductive
\[ \mathrm{mmtree}\, T \; ::=\; \mathrm{Leaf} \; \mid \; \mathrm{Node}\, (\mathrm{mmtree}\, T)\, T\, (\mathrm{mmtree}\, T). \]
Its in-order traversal is
\[ \mathrm{mmtree\_ to\_ seq}(\mathrm{Node}\, \ell \, x\, r) \; =\; \mathrm{mmtree\_ to\_ seq}(\ell ) \mathbin {+\! \! +} x :: \mathrm{mmtree\_ to\_ seq}(r). \]
For a non-empty sequence \(s\), \(\texttt{mm\_ pos}(s)\) is the position of \(s\)’s minimum if it occurs strictly before its maximum, and the position of its maximum otherwise. This is the position of the root of \(M(s)\).
For non-empty \(s\), \(\texttt{mm\_ pos}(s) {\lt} |s|\).
For every \(s \in \mathrm{seq}\, \mathbb {N}\),
\[ \mathrm{mmtree\_ to\_ seq}(\mathrm{mmtree\_ of\_ seq}(s)) = s. \]
This identifies \(M(s)\) as a faithful representation of the underlying sequence: every position in \(w\) corresponds to a \(\mathrm{Node}\) of \(M(w)\).