[a] [a] [b]

# MSO Queries on Trees: Enumerating Answers under Updates Using Forest
Algebras

Sarah Kleest-Meißner0000-0002-4133-7975  ,  Jonas Marasus0000-0001-9298-2360
and  Matthias Niewerth0000-0003-2032-5374  Humboldt-Universität zu Berlin,
Germany  Universität Bayreuth, Germany

###### Abstract.

We describe a framework for maintaining forest algebra representations that
are of logarithmic height for unranked trees. Such a representations can be
computed in ${\mathcal{O}}(n)$ time and updated in ${\mathcal{O}}(\log(n))$
time. The framework is of potential interest for data structures and
algorithms for trees whose complexity depend on the depth of the tree
(representation). We provide an exemplary application of the framework to the
problem of efficiently enumerating answers to MSO-definable queries over trees
which are subject to local updates. We exhibit an algorithm that uses an
${\mathcal{O}}(n)$ preprocessing phase and enumerates answers with
${\mathcal{O}}(\log(n))$ delay between them. When the tree is updated, the
algorithm can avoid repeating expensive preprocessing and restart the
enumeration phase within ${\mathcal{O}}(\log(n))$ time. Our algorithms and
complexity results in the paper are presented in terms of node-selecting tree
automata representing the MSO queries.

###### Key words and phrases:

MSO, query enumeration, trees, forest algebras

##  1\. Introduction

Efficient query evaluation is one of the most central problems in databases.
Given a query $Q$ and a database $D$, we are asked to compute the set $Q(D)$
of tuples of $Q$ on $D$. In general, the number of tuples in $Q(D)$ can be
extremely large: when $Q$ has arity $k$ and $D$ has size $n$, then $Q(D)$ can
contain up to $n^{k}$ tuples. Since databases are typically very large, it may
be unfeasible to compute $Q(D)$ in its entirety.

A straightforward solution to this problem is top-$k$ query answering, where
one is interested in the $k$ most relevant answers according to some metric.
Another way to deal with this problem is to produce the answers one by one
without repetition. This is known as _query enumeration_ (see, e.g., [Bag06,
Cou09, DS11, KS13a, KS13b, Seg13]). More precisely, query enumeration aims at
producing a small number of answers first and then, on demand, producing
further small batches of answers as long as the user desires or until all
answers are depleted. Most existing algorithms for query enumeration consist
of two phases: the _preprocessing phase_ , which lasts until the first answer
is produced, and the _enumeration phase_ in which next answers are produced
without repetition. It is natural to try to optimize two kinds of time
intervals in this procedure: the time of the preprocessing phase and the
_delay_ between answers, which is the time required between two answers in the
enumeration phase. Thus, when one can answer $Q(D)$ with preprocessing time
$p$ and delay $d$, one can compute $Q(D)$ in time $p+d\cdot|Q(D)|$, where
$|Q(D)|$ is the number of answers.

Much attention has been given to finding algorithms that answer queries with a
linear-time preprocessing phase and constant-time delay between answers
[Seg13]. The preprocessing phase is usually used to build an index that allows
for efficient enumeration. Since databases can be subjected to frequent
updates and preprocessing typically costs linear time, it is usually not an
option to recompute the index after every update. We want to address this
concern and investigate what can be done if one wants to deal with such
updates more efficiently than simply re-starting the preprocessing phase.

We cannot expect efficient algorithm for query enumeration in the general
case, as even deciding whether a (Boolean) query has an answer is NP-hard.
Therefore, we have to restrict the problem. In the literature, there are two
general directions towards tractable query enumeration under updates:
restricting the class of queries or restricting the structure of the data.

There is quite recent progress on enumerating certain classes of conjunctive
queries with constant delay and sublinear update time [BKS17, BKS18b].
Similarly, there are algorithms that can enumerate FO+MOD queries with
constant delay and constant update time on bounded degree databases [BKS18a].

In this article, we follow the second approach and study the enumeration
problem for MSO queries with free node variables over _trees_. Furthermore,
the trees can be subjected to local updates. We consider updates that relabel
a node or insert/delete a leaf. Our aim is to provide an index structure that
can be efficiently updated, when the underlying tree changes. This makes the
enumeration phase _insensitive to such updates_ : when our algorithm is
producing answers with a small delay in the enumeration phase and the
underlying data $D$ is updated, we can update the index and re-start
enumerating on the new data within the same delay.

The complexity results in this article are presented in terms of the size of
the tree; the arity $k$ of the query; and the number of states of a non-
deterministic node-selecting finite tree automaton for the query. The
connection between run-based node-selecting automata and MSO-queries is well
known, see, e.g. [NPTT05, TW68].

When measuring complexity in terms of query size, we have to keep in mind that
MSO queries can be non-elementary smaller than their equivalent non-
deterministic node-selecting tree automata. Therefore, our enumeration
algorithm is non-elementary in terms of the MSO formula, which cannot be
avoided unless P $=$ NP [FG04]. For this reason, MSO is usually not used as a
query language in practice; although it is widely regarded as a good yardstick
for expressiveness.

Our complexities are exponential in the arity $k$ of the queries. However for
practical scenarios, $k$ is usually very small. We note that $k=2$ suffices
for modeling XPath queries, which are central in XML querying.

Although we do not obtain constant-delay algorithms as in previous work on
static trees, we can prove that, in the dynamic setting
${\mathcal{O}}(\log(n))$ delay is possible. This means that, after receiving
an update, we do not need to restart the ${\mathcal{O}}(n)$ preprocessing
phase but only require ${\mathcal{O}}(\log(n))$ time to produce the first
answer on the updated tree and continue enumerating from there. We allow
updates to arrive at any time: If an update arrives during the enumeration
phase, we immediately start the enumeration phase for the new structure.

In [ABMN19] it has been shown that the constant delay enumeration approach for
MSO queries over static trees from [ABJM17, ABM18] can be extended to allow
updates, if the trees are represented by balanced forest algebra formulas that
are described in this article and where already depicted in a preliminary
version [Nie18].

### Previous Results on MSO Queries on Trees

Update | Delay | Remarks | Reference
---|---|---|---
${\mathcal{O}}(\log^{2}(n))$ | — | only Boolean queries; ${\mathcal{O}}(\log(n))$ on strings | [BPV04]
${\mathcal{O}}(\log^{2}(n))$ | — | Boolean XPath queries | [BGM10]
— | ${\mathcal{O}}(1)$ | updates in ${\mathcal{O}}(n)$ by recomputation | [Bag06]
— | ${\mathcal{O}}(1)$ | different proof using decomposition forests | [KS13b]
— | ${\mathcal{O}}(1)$ | different proof using circuits | [ABJM17]
${\mathcal{O}}(\log^{2}(n))$ | ${\mathcal{O}}(\log^{2}(n))$ | complexities drop to ${\mathcal{O}}(\log(n))$ on strings | [LM14]
${\mathcal{O}}(\log(n))$ | ${\mathcal{O}}(1)$ | only works on strings; huge constants | [NS18]
${\mathcal{O}}(\log(n))$ | ${\mathcal{O}}(1)$ | only relabel updates; uses circuits | [ABM18]
${\mathcal{O}}(\log(n))$ | ${\mathcal{O}}(1)$ | uses the techniques developed in this article | [ABMN19]
${\mathcal{O}}(\log(n))$ | ${\mathcal{O}}(\log(n))$ | uses forest algebras | this work
Table 1. Data complexity of existing solutions. Preprocessing time is always
in ${\mathcal{O}}(n)$.

We have collected previous results on evaluation and enumeration of MSO
queries on strings and trees in Table 1.

For MSO sentences, this problem has been studied by Balmin, Papakonstantinou,
and Vianu [BPV04]. Balmin et al. show how one can efficiently maintain
satisfaction of a finite tree automaton (and therefore, an MSO property) on a
tree $t$ which is subjected to updates. More precisely, when an update
transforms $t$ to $t^{\prime}$, they want to be able to decide very quickly
after the update whether $t^{\prime}$ is accepted by the automaton. Taking $n$
as the size of $t$, they show that, using a one-time preprocessing phase of
time ${\mathcal{O}}(n)$ to construct an auxiliary data structure, one can
always decide within time ${\mathcal{O}}(\log^{2}(n))$ after the update
whether $t^{\prime}$ is accepted. The delay between answers is irrelevant in
the setting of Balmin et al. since their queries always have a Boolean answer.
Björklund et al. show a similar result for XPath queries, which are less
expressive than MSO but can be exponentially more succinct than tree automata,
which leads to better constants. Losemann and Martens [LM14] extended the work
of Balmin et al. to enumeration of $k$-ary queries under updates with
${\mathcal{O}}(\log^{2}(n))$ delay and update time. Our goal is to improve the
delay and update time to ${\mathcal{O}}(\log(n))$.

The enumeration problem of static trees was studied by Bagan [Bag06], who
showed that (fixed) monadic second-order (MSO) queries can be evaluated with
linear time preprocessing and constant delay over structures of bounded tree-
width. Independently, another constant delay algorithm (but with
${\mathcal{O}}(n\log(n))$ preprocessing time) was obtained by Courcelle et al.
[Cou09]. Recently, Kazana and Segoufin [KS13b] provided an alternative proof
of Bagan’s result based on a deterministic factorization forest theorem by
Colcombet [Col07], which is itself based on a result of Simon [Sim90]. Such
(deterministic) factorization forests provide a good divide-and-conquer
strategy for words and trees, but it is unclear how they can be maintained
under updates. It seems that they would have to be recomputed entirely after
an update which is too expensive for our purposes.

With exception of [Bag06], which presents an algorithm that is cubic in terms
of the tree automaton, these papers present complexities in terms of the size
of the trees only, that is, they consider the MSO formula to be constant. To
the best of our knowledge, the data structures in these approaches cannot be
updated efficiently if the underlying tree is updated. An overview of
enumeration algorithms with constant delay was given in [Seg13].

### Heavy Path Decomposition vs. Forest Algebras

A main idea in [BPV04] is a decomposition of trees into heavy paths which
allows one to decompose the problem for trees into ${\mathcal{O}}(\log(n))$
similar problems on words, for which a solution was given by Patnaik and
Immerman in [PI97]. This allows to solve the incremental evaluation problem
with ${\mathcal{O}}(n)$ preprocessing time and ${\mathcal{O}}(\log^{2}(n))$
update time, where one $\log$ factor stems from the heavy path decomposition
and the other from solving the problem over strings using monoids of finite
string automata.

The approach of [BPV04] was later extended to enumeration of MSO queries by
Losemann and Martens [LM14]. They tweaked the monoid to contain additional
information needed to find the symbols that appear in query results, which
allows logarithmic delay and update time. Just as Balmin et al., Losemann and
Martens use heavy path decomposition to lift the algorithm from words to trees
resulting again in an additional logarithmic factor in the delay and update
time.

We adapt the algorithm of Losemann and Martens from monoids to forest algebras
in Section 6. This saves us a logarithmic factor compared to their results. We
believe that the framework we introduce in Section 3 to compute and maintain
forest algebra formulas with logarithmic height can be applied in other areas
to lift results from strings to trees.

### Tree Decomposition vs. Forest Algebras

In [ABM18], Amarilli et al. use tree decompositions [BH98] to convert
arbitrary trees to trees of logarithmic height. Having a tree of logarithmic
height is central in their algorithm to allow enumeration of MSO queries over
trees under relabeling updates. According to Amarilli et al., the biggest
obstacle in generalizing their work to allow structural updates
(insertion/deletion of nodes) of the tree was the inability to update the tree
decomposition when the input tree changes.

Following up on the preliminary version of this article [Nie18], it has been
shown in [ABMN19] that the enumeration algorithm from [ABM18] can be
generalized to allow structural updates on the tree using the methods we
develop in sections 3 and 4.

### Further Related Work

There are implementations for and experimental results on incremental
evaluation of XML documents wrt. DTDs [BML+04] and regular expressions with
counters on strings [BMT15]. The query evaluation problem has also been
studied from a descriptive complexity point of view, e.g., for conjunctive
queries [ZS14] and the reachability query on graphs [DKM+15].

### Contributions

We depict a mechanism for representing trees by the means of forest algebra
formulas in Section 3. Furthermore, we show how these representations can be
maintained after updates that can relabel, insert, or delete individual nodes
of the tree. We believe that these techniques are interesting on their own.
Building on top of a preliminary version of this article, [ABMN19] already
uses the techniques provided here to achieve further improvements in the
enumeration of MSO queries on trees.

Section 4 shows how forest algebras are related to tree automata through their
transition algebra. This relationship is exactly the same as the relationship
between monoids and string automata.

We provide a first application of our framework in Section 5, where we show
how forest algebra representations can be used to solve the incremental
evaluation problem for Boolean MSO formulas on trees with logarithmic update
time after linear preprocessing.

Finally, in Section 6, we show how forest algebras can be used to enumerate
MSO queries over trees with logarithmic delay and logarithmic update time
after a linear preprocessing step. Even if there is an improved algorithm
available in [ABMN19], we believe that the presented algorithm is useful.
First, it gives a quite simple demonstration how the general techniques
presented in Section 3 can be applied, and second it is a much simpler
algorithm that might actually be more efficient for medium sized trees than
the more complex algorithm presented in [ABMN19].

### Earlier Version

An earlier version of this article was presented at the 2018 Symposium on
Logic in Computer Science (LICS 2018) [Nie18]. The earlier version does not
contain formal proofs. Unfortunately, the unpublished proofs turned out to
have a flaw. Therefore we modified the algorithms slightly in order to show
the claimed complexity bounds. We believe that also the algorithms as
presented in [Nie18] meet the same complexity bounds, but we were not able to
prove this.

##  2\. Preliminaries

### Trees, Forests, Contexts

In this article, trees and forests are labeled by some finite alphabet
$\Sigma$, rooted, and ordered. Contexts are forests which contain a single
hole, denoted by ${\scaleobj{0.75}{\Box}}$, which may not be part of any
forest. In detail: A _forest_ is a tuple $F=(V,E,\leq,\mathsf{lab})$, where
$V$ is a finite set of nodes, $E\subseteq V\times V$ is the set of edges,
${\leq}\subseteq V\times V$ is the sibling order, and $\mathsf{lab}\colon
V\to\Sigma$ is the labeling function.

If $(v,w)\in E$, we say $w$ is a _child_ of $v$ and $v$ is the _parent_ of
$w$. If $(v,w)$ is within the transitive closure of $E$, we say $w$ is a
_descendant_ of $v$ and $v$ is an _ancestor_ of $w$. A node without parents is
called a _root_ and we denote the set of all roots of $F$ by
$\mathsf{roots}(F)$. A node without children is called a _leaf_. The
transitive closure of $E$ must be acyclic and no node may have more than one
parent. If $v_{1}\leq v_{2}$ we say, $v_{1}$ lies _left_ of $v_{2}$. For every
node $v$ $\leq$ must be a linear order on the set of all children of $v$.
Likewise $\leq$ needs to be a linear order on $\mathsf{roots}(F)$ Other than
that $\leq$ must have no additional elements. A forest with a single root is
called a _tree_.

A _context_ $C=(V,E,\leq,\mathsf{lab})$ is a forest with the exception that
$V$ contains the hole ${\scaleobj{0.75}{\Box}}$. The hole must be a leaf and
does not carry a label, i.e., $\mathsf{lab}$ is a function on
$V\setminus\\{{\scaleobj{0.75}{\Box}}\\}$.

We overload notation and use a symbol $a\in\Sigma$ to denote the forest that
contains a single node with label $a$. Similarly we use
$a_{\scaleobj{0.75}{\Box}}$ with $a\in\Sigma$ to denote the context with an
$a$-labeled root that has the hole as its only child. We use $\varepsilon$ and
${\scaleobj{0.75}{\Box}}$ to denote the empty forest and the context that only
consists of the hole, respectively.

We usually will denote forests by $F$ and contexts by $C$ possibly with
subscripts. We use $D$ (with subscripts) to denote that the object can be
either a forest or a context.

We will usually assume w.l.o.g. that for different forests and contexts the
sets of nodes are disjoint. This can be achieved by renaming the nodes of one
of the operands.

We define two operations on contexts and forests: The (horizontal)
_concatenation_ $\mathrel{{}_{\vartriangle}}$ places two forests or a forest
and a context next to each other and the (vertical) _context application_
which inserts a forest or context into a context by replacing the hole with
the roots of the inserted forest or context. Not all combinations of operands
are allowed in order for the result to be well defined. It is not possible to
concatenate two contexts and the left operand of a context application has to
be a context. We depict examples of the two operations in Figure 1. In detail
the operations are defined as follows:

$F$ (forest)

aa

$C$ (context)

b${\scaleobj{0.75}{\Box}}$a

$F\mathrel{{}_{\vartriangle}}C$ (context)

aab${\scaleobj{0.75}{\Box}}$a

$C\mathrel{{}_{\vartriangle}}F$ (forest)

baaa

Figure 1. Examples for concatenation and context application

Let $D_{1}=(V_{1},E_{1},\leq_{1},\mathsf{lab}_{1})$ and
$D_{2}=(V_{2},E_{2},\leq_{2},\mathsf{lab}_{2})$ be two forests or one forest
and a context in either order. We compute
$D=D_{1}\mathrel{{}_{\vartriangle}}D_{2}$ by taking the disjoint componentwise
union and specifying that all roots of $D_{2}$ have to be right of all roots
of $D_{1}$. Formally we define
$D_{1}\mathrel{{}_{\vartriangle}}D_{2}=(V,E,\leq,\mathsf{lab})$, where

$\displaystyle V\;\;$ $\displaystyle=\;\;V_{1}\cup V_{2}$ $\displaystyle
E\;\;$ $\displaystyle=\;\;E_{1}\cup E_{2}$ $\displaystyle\leq\;\;$
$\displaystyle=\;\;\leq_{1}\;\cup\;\leq_{2}\;\cup\;\;\\{(v_{1},v_{2})\enspace|\enspace
v_{1}\in\mathsf{roots}(D_{1}),v_{2}\in\mathsf{roots}(D_{2})\\}$
$\displaystyle\mathsf{lab}\;\;$
$\displaystyle=\;\;\mathsf{lab}_{1}\;\cup\;\mathsf{lab}_{2}$

We note that $D_{1}\mathrel{{}_{\vartriangle}}D_{2}$ is a forest if $D_{1}$
and $D_{2}$ are both forests and it is a context if one of $D_{1}$, $D_{2}$ is
a context. If $D_{1}$ and $D_{2}$ are both contexts, then
$D_{1}\mathrel{{}_{\vartriangle}}D_{2}$ is undefined.

Let $C_{1}=(V_{1},E_{1},\leq_{1},\mathsf{lab}_{1})$ be a context and
$D_{2}=(V_{2},E_{2},\leq_{2},\mathsf{lab}_{2})$ be a context or a forest. We
compute $D=C_{1}\mathrel{{}_{\vartriangle}}D_{2}$ by first removing the hole
from $C_{1}$, then taking the componentwise disjoint union and afterwards
tweaking the set of edges and sibling order of $D$ such that the ordered list
of roots of $D_{2}$ appears where the hole in $C_{1}$ was before. Let
$C_{1}^{\boxtimes}=(V_{1}^{\boxtimes},E_{1}^{\boxtimes},\leq_{1}^{\boxtimes},\mathsf{lab}_{1})$
be the forest derived from $C_{1}$ by removing the hole. Formally we define
$C_{1}\mathrel{{}_{\vartriangle}}D_{2}=(V,E,\leq,\mathsf{lab})$, where

$\displaystyle V\;\;$ $\displaystyle=\;\;V_{1}^{\boxtimes}\cup V_{2}$
$\displaystyle E\;\;$ $\displaystyle=\;\;E_{1}^{\boxtimes}\cup
E_{2}\cup\\{(v_{1},v_{2})\enspace|\enspace(v_{1},{\scaleobj{0.75}{\Box}})\in
E_{1},v_{2}\in\mathsf{roots}(C_{2})\\}$ $\displaystyle\leq\;\;$
$\displaystyle=\;\;{\leq_{1}^{\boxtimes}}\cup{\leq_{2}}\cup\\{(v_{1},v_{2})\enspace|\enspace(v_{1},{\scaleobj{0.75}{\Box}})\in{\leq_{1}},v_{2}\in\mathsf{roots}(C_{2})\text{
or
}v_{1}\in\mathsf{roots}(C_{2}),({\scaleobj{0.75}{\Box}},v_{2})\in{\leq_{1}}\\}$
$\displaystyle\mathsf{lab}\;\;$
$\displaystyle=\;\;\mathsf{lab}_{1}\cup\mathsf{lab}_{2}$

We note that $C_{1}\mathrel{{}_{\vartriangle}}D_{2}$ is a context if $D_{2}$
is a context and it is a forest if $D_{2}$ is a forest.

### Forest Algebras

Here, we introduce forest algebras that were first described by Bojańczyk and
Walukiewicz [BW07]. We prefer the syntax used in the Handbook of Automata
Theory [Boj21] that also provides a nice introduction.

A _forest algebra_

$\mathcal{F}\;\;=\;\;(H,V,{}_{HH},{}_{HV},{}_{VH},{}_{VV},{}_{VH},\varepsilon,{\scaleobj{0.75}{\Box}})$

consists of two monoids, $(H,{}_{HH},\varepsilon)$ and
$(V,{}_{VV},{\scaleobj{0.75}{\Box}})$ along with three monoidal actions:

HV $\displaystyle\colon H\times V\to V$ (left monoidal action of $H$ on $V$),
VH $\displaystyle\colon V\times H\to V$ (right monoidal action of $H$ on $V$),
and VH $\displaystyle\colon V\times H\to H$ (right monoidal action of $V$ on
$H$).

Intuitively, each element of $H$ represents a forest and each element in $V$
represents a context. The monoid operations correspond to concatenation of
forests and context application (on a context), respectively. The neutral
elements of $H$ and $V$ correspond to the empty forest and the forest
consisting only of the hole. The monoidal actions correspond to concatenation
of a forest and a context (or the other way round) and context application of
a context on a forest.

|  | Axiom |  | Name
---|---|---|---|---
(A1) | $\varepsilon{}_{HH}F_{1}\;\;=$ | $F_{1}$ | $=\;\;F_{1}{}_{HH}\varepsilon$ | neutral element
(A2) | $\varepsilon{}_{HV}C_{1}\;\;=$ | $C_{1}$ | $=\;\;C_{1}{}_{VH}\varepsilon$
(A3) | ${\scaleobj{0.75}{\Box}}{}_{VV}C_{1}\;\;=$ | $C_{1}$ | $=\;\;C_{1}{}_{VV}{\scaleobj{0.75}{\Box}}$
(A4) | ${\scaleobj{0.75}{\Box}}{}_{VH}F_{1}\;\;=$ | $F_{1}$ |
(A5) | $(F_{1}{}_{HH}F_{2}){}_{HH}F_{3}$ | $=$ | $F_{1}{}_{HH}(F_{2}{}_{HH}F_{3})$ | associativity
(A6) | $(F_{1}{}_{HH}F_{2}){}_{HV}C_{1}$ | $=$ | $F_{1}{}_{HV}(F_{2}{}_{HV}C_{1})$
(A7) | $(C_{1}{}_{VH}F_{1}){}_{VH}F_{2}$ | $=$ | $C_{1}{}_{VH}(F_{1}{}_{HH}F_{2})$
(A8) | $(F_{1}{}_{HV}C_{1}){}_{VH}F_{2}$ | $=$ | $F_{1}{}_{HV}(C_{1}{}_{VH}F_{2})$
(A9) | $(C_{1}{}_{VV}C_{2}){}_{VV}C_{3}$ | $=$ | $C_{1}{}_{VV}(C_{2}{}_{VV}C_{3})$
(A10) | $(C_{1}{}_{VV}C_{2}){}_{VH}F_{1}$ | $=$ | $C_{1}{}_{VH}(C_{2}{}_{VH}F_{1})$
(A11) | $(F_{1}{}_{HV}C_{1}){}_{VH}F_{2}$ | $=$ | $F_{1}{}_{HH}(C_{1}{}_{VH}F_{2})$ | interaction
(A12) | $(F_{1}{}_{HV}C_{1}){}_{VV}C_{2}$ | $=$ | $F_{1}{}_{HV}(C_{1}{}_{VV}C_{2})$
(A13) | $(C_{1}{}_{VH}F_{1}){}_{VH}F_{2}$ | $=$ | $(C_{1}{}_{VH}F_{2}){}_{HH}F_{1}$
(A14) | $(C_{1}{}_{VH}F_{1}){}_{VV}C_{2}$ | $=$ | $(C_{1}{}_{VV}C_{2}){}_{VH}F_{1}$
Table 2. Axioms of Forest Algebras

In Table 2 we depict the axioms that forest algebras need to satisfy. The two
upper groups of axioms are the usual axioms for monoids and monoidal actions
stating the effect of the neutral elements and the laws of associativity. The
axioms in the bottom group describe the interactions of both monoids and are
special for forest algebras. The intuitive explanation of these axioms is that
if one concatenates a forest $F_{1}$ and a context $C_{1}$ (in either order),
it is solely the context that is responsible for what happens in a subsequent
context application. Therefore a subsequent context application should have
the same effect as first doing the context application on $C_{1}$ and
afterwards doing the concatenation with $F_{1}$.

We note that the Axioms A11–A14 are not depicted in [Boj21]. This seems to be
an oversight. Without these axioms it is possible to construct a forest
algebra $\mathcal{F}$, such that there does not exist a morphism from the free
forest algebra (see below) to $\mathcal{F}$. However, [Boj21] states that such
a morphism exists for every forest algebra.

We will often drop the indices of the monoid operations and monoidal actions,
i.e., we will just use and . Which operation is needed is clear from the
operands. In some cases, we do not even specify, whether we refer to
concatenation or context application. In this case, we use . Given a formula
$\Psi$ and an inner node $v$ of the parse tree, we denote by v the operation
at node $v$.

### Free Forest Algebra

The _free forest algebra_ over an alphabet $\Sigma$ is defined as

$\mathcal{F}_{\Sigma}=(H,V,\mathrel{{}_{\vartriangle}},\mathrel{{}_{\vartriangle}},\mathrel{{}_{\vartriangle}},\mathrel{{}_{\vartriangle}},\mathrel{{}_{\vartriangle}},\varepsilon,{\scaleobj{0.75}{\Box}})\;,$

where $(H,\mathrel{{}_{\vartriangle}},\varepsilon)$ is the monoid of all
forests over $\Sigma$ with the concatenation operation and
$(V,\mathrel{{}_{\vartriangle}},{\scaleobj{0.75}{\Box}})$ is the monoid of all
contexts over $\Sigma$ with the context application operation. We note that
all five operations of the algebra are provided by the two operations
$\mathrel{{}_{\vartriangle}}$ and $\mathrel{{}_{\vartriangle}}$ by restricting
them to the respective domains.

######  Lemma 1.

The free forest algebra over any alphabet $\sigma$ satisfies all axioms of
forest algebras.

######  Proof 2.1 (Proof sketch).

All axioms can be shown by applying the definition of
$\mathrel{{}_{\vartriangle}}$ and $\mathrel{{}_{\vartriangle}}$. The axioms
for the neutral elements $\varepsilon$ and ${\scaleobj{0.75}{\Box}}$ (axioms
A1–A4) hold, as the operations $\mathrel{{}_{\vartriangle}}$ and
$\mathrel{{}_{\vartriangle}}$ are defined by the means of unions where one
side of each union is empty.

For the associativity axioms of the horizontal concatenation (axioms A5–A8) it
suffices to observe that $\leq$ is constructed in a way that is compatible
with associativity. All other components of the resulting forest or context
are constructed by taking the union, which is associative.

The associativity of the context application (Axioms A9 and A10) can be shown
by distinguishing the holes in $C_{1}$ and $C_{2}$. The context application
involving $C_{3}$ or $F_{1}$ is always applied to the hole that originates
from $C_{2}$. Analogously, in the axioms A11–A14, the context application
involving $C_{2}$ or $F_{2}$ is always applied to the hole originating from
$C_{1}$.

### Parse Trees (of Formulas)

The _parse tree_ of a forest algebra formula (from some algebra
$\mathcal{F}=(V,H)$) is a binary tree with inner nodes labeled by
$\\{{}_{HH},{}_{HV},{}_{VH},{}_{VV},{}_{VH}\\}$ and leaf nodes marked by some
element of $V\cup H$. In most cases we will omit the indices from and , as the
concrete operation is implied by the types of the operands. However, we will
always assume that the concrete operation is stored in the node. This way it
is always possible to tell which operand of a concatenation contains the hole
(if any). In the case of formulas from the free forest algebra, leaves will be
labeled by elements from
$\Sigma\cup\\{a_{\scaleobj{0.75}{\Box}}\enspace|\enspace a\in\Sigma\\}$, where
elements from $\Sigma$ indicate individual nodes with the corresponding label
and elements of the form $a_{\scaleobj{0.75}{\Box}}$ indicate a node with the
given label that has as its only child the hole.

Given a formula $\Psi$, we denote by $||\Psi||$ the number of leaves in (the
parse tree of) $\Psi$. As we do not consider parse trees with nodes
corresponding to the empty forest or empty context, $||\Psi||$ is always equal
to the number of nodes in the represented forest or context. As parse trees
are always binary trees, they will have one inner node less than leaves.
Therefore, a parse tree is always of roughly twice the size than the
represented forest or context.

The _balance_ $\mathsf{balance}(v)$ of an inner node $v$ of the parse tree is
the height difference of the two trees, rooted at the children of $v$.
Positive values for $\mathsf{balance}(v)$ denote that the right subtree is
higher than the left subtree. By $\mathcal{B}(\Psi)$ we denote the sum of all
absolute balances, i.e.,

$\mathcal{B}(\Psi)\;\;=\;\;\sum_{v\in\Psi}|\mathsf{balance}(v)|\;.$

For each node $v$ in a parse tree, we denote by $\mathsf{child_{L}}(v)$ and
$\mathsf{child_{R}}(v)$, the left and right child of $v$, respectively. If
$\mathsf{balance}(v)\neq 0$, we denote with $\mathsf{child_{D}}(v)$ the child
of $v$ that belongs to the deeper subtree. For every node $v$ of a formula
$\Psi$, the _long path_ of $v$ denoted by $\mathsf{lp}(v)$ is defined
recursively as follows:

$\mathsf{lp}(v)\;\;=\;\;\begin{cases}v&\text{if $\mathsf{balance}(v)=0$}\\\
v\cdot\mathsf{lp}(\mathsf{child_{L}}(v))&\text{if $\mathsf{balance}(v)<0$}\\\
v\cdot\mathsf{lp}(\mathsf{child_{R}}(v))&\text{if
$\mathsf{balance}(v)>0$}\end{cases}$

We use $\mathsf{lp}^{-1}(v)$ to denote the upwards path starting at $v$ that
contains all nodes $u$ with $v$ being on $\mathsf{lp}(u)$.

$a_{\scaleobj{0.75}{\Box}}$$b_{\scaleobj{0.75}{\Box}}$$b$$a_{\scaleobj{0.75}{\Box}}$$b_{\scaleobj{0.75}{\Box}}$$a$$a$

$a$$b$$a$$b$$a$$a$$b$

Figure 2. Parse tree of a forest-algebra formula and its generated forest.

We use forest-algebra formulas synonymously with their parse trees. In this
sense the height of a forest-algebra formula $0pt(\Psi)$ is defined as the
height of its parse tree, i.e., the maximal number of nodes on path from the
root to a leaf.

We use $v$ and $w$ to denote nodes of either a given tree $T$, or a parse tree
of a forest algebra formula $\Psi$. To keep the notation clean, we identify
leaves of $\Psi$ with nodes of $T$, whenever we have a formula $\Psi$
describing a tree $T$. Given a node $v$ of the parse tree of $\Psi$, we use
$\Psi_{v}$ to denote the subformula of $\Psi$ rooted at $v$ and $T_{v}$ to
denote the forest or context described by $\Psi_{v}$.

### Morphisms of Forest Algebras

A homomorphism $h=(h_{H},h_{V})$ from a forest algebra
$\mathcal{F}_{1}=(H_{1},V_{1})$ to a forest algebra
$\mathcal{F}_{2}=(H_{2},V_{2})$ is given by two monoid morphisms $h_{H}\colon
H_{1}\to H_{2}$, $h_{V}\colon V_{1}\to V_{2}$ that additionally satisfy

$h_{H}(C\odot F)\;\;=\;\;h_{V}(C)\odot h_{H}(F)$

for all $C\in V_{1}$ and $F\in H_{1}$. To simplify notation, we will omit the
indices $H$ and $V$ and use $h$ for both morphisms.

For every forest algebra $\mathcal{F}=(V,H)$ one can define a morphism from
the free algebra $\mathcal{F}_{\Sigma}$ by providing a function
$h\colon\\{a_{\scaleobj{0.75}{\Box}}\enspace|\enspace a\in\Sigma\\}\rightarrow
V$, i.e. by providing the mappings for all contexts that have a single root
with the hole as its only child. The function $h$ can be extended to a
morphism from the free forest algebra by applying the algebra operations. The
mapping for a single $a$-labeled node can for example be computed as
$h(a_{\scaleobj{0.75}{\Box}}){}_{VH}\varepsilon$.

### Updates of Forests and Formulas

We consider the following _updates_ on trees:

  1. (1)

$\mathsf{relab}(v,a)$: Replace the current label of node $v$ by $a$

  2. (2)

$\mathsf{subdiv}(v,a)$: Insert a new $a$-node as the only child of $v$ making
all existing children of $v$ children of the new node

  3. (3)

$\mathsf{insert_{L}}(v,a)$, $\mathsf{insert_{R}}(v,a)$: insert a new $a$-node
as left or right sibling of node $v$

  4. (4)

$\mathsf{delete}(v)$: delete node $v$, where $v$ must correspond to a leaf in
the tree, i.e., $v$ must not have a label of the form
$a_{\scaleobj{0.75}{\Box}}$

We refer to the updates as _relabeling_ , _subdivision_ , _leaf insertion_ ,
and _deletion_. Usually we subsume leaf insertions and subdivions under the
broder term _insertions_. We note that the insertion of a node below a leaf is
a special case of a subdivision.

$a$$\vphantom{b}c$$d$$\longrightarrow$$a$$b$$\vphantom{b}c$$d$$a_{\Box}$b$c$$d$$\longrightarrow$$a_{\Box}$$b_{\Box}$b$c$$d$
(a) Subdividing the $a$-node with a new $b$-node

$a$$b$b$c$$\longrightarrow$$a$$b$b$c$$d$$a_{\Box}$$b$b$c$$\longrightarrow$$a_{\Box}$$b$b$c$$d$
(b) Inserting a $d$-node right of the $c$-node

b$a$$b$b$c$$\longrightarrow$b$a$$b$$a_{\Box}$$b$b$c$$\longrightarrow$b$a_{\Box}$$b$
(c) Deleting the $c$-node

$a$$b$$c$$\longrightarrow$$a$$b$$a_{\Box}$$b_{\Box}$b$c$$\longrightarrow$b$a_{\Box}$$b$
(d) Deleting the $c$-node (without siblings)

Figure 3. Examples depicting the tree updates considered in this paper and
their corresponding rewrites in the forest algebra formula

We depict examples of every update (except relabeling) in Figure 3. The figure
always depicts an update in a tree and the corresponding update in the formula
(see below for an description). We use unique node labels in each tree, such
that corresponding nodes in the tree and the formula can be easily identified.

We now describe how each update can be applied to a formula $\Psi$ that
represents the tree $T$. We assume that given a node $v$ in $T$ we can locate
the corresponding node $v^{\prime}$ in the formula in constant time, e.g., by
adding pointers to each node in $T$. In the following, $v^{\prime}$ is the
node in $\Psi$ that corresponds to $v$.

  1. (1)

$\mathsf{relab}(v,a)$: It suffices to locate $v^{\prime}$ in the formula and
change its label to $a$ or $a_{\scaleobj{0.75}{\Box}}$, depending on whether
$v$ is a leaf or an inner node of $T$.

  2. (2)

$\mathsf{subdiv}(v,a)$: We locate $v^{\prime}$ in the formula and add a new
node $w$ that is labeled VH (if $v$ is a leaf) or VV (if $v$ is an inner node)
at the place of $v^{\prime}$. We make $v^{\prime}$ the left child of $w$. The
right child of $w$ is a new node that has label $a$ (if $v$ was a leaf) or
$a_{\scaleobj{0.75}{\Box}}$ (if $v$ was an inner node). If $v$ was a leaf, the
label of $v^{\prime}$ needs to be changed from some label $b$ to the label
$b_{\scaleobj{0.75}{\Box}}$. An example is depicted in Figure 3(a).

  3. (3)

$\mathsf{insert_{L}}(v,a)$, $\mathsf{insert_{R}}(v,a)$: We replace
$v^{\prime}$ with $(a\oplus v^{\prime})$ or $(v^{\prime}\oplus a)$,
respectively. An example is depicted in Figure 3(b).

  4. (4)

$\mathsf{delete}(v)$: We distinguish two cases.

     * •

Case 1: The smallest subformula that strictly contains $v^{\prime}$ is of the
form $(v^{\prime}\oplus\Psi^{\prime})$ or $(\Psi^{\prime}\oplus v^{\prime})$,
where $\Psi^{\prime}$ is some subformula. In this case $v$ has at least one
sibling in $T$ and we replace the whole subformula with $\Psi^{\prime}$, i.e.,
the -node and $v^{\prime}$ are removed and $\Psi^{\prime}$ is placed at the
previous position of the -node. An example is depicted in Figure 3(c).

     * •

Case 2: The smallest subformula that strictly contains $v^{\prime}$ is of the
form $(\Psi^{\prime}\odot v^{\prime})$. In this case, $v$ does not have a
sibling in $T$. We note that $\Psi^{\prime}$ is necessarily a context, while
$(\Psi^{\prime}\odot v^{\prime})$ is a forest. Thus we cannot simply replace
$(\Psi^{\prime}\odot v^{\prime})$ by $\Psi^{\prime}$. Instead we first have to
locate the node $w^{\prime}$ corresponding to the parent $w$ of $v$ and change
its label from some label $a_{\scaleobj{0.75}{\Box}}$ to $a$ (i.e., remove the
hole below the node). Furthermore we have to adapt the labels of ancestors of
$w^{\prime}$ in $\Psi^{\prime}$, as all of these ancestors change their type
from context to forest. Therefore the labels VH and HV have to be changed to
HH and the label VV has to be changed to VH. An example is depicted in Figure
3(d).

We note that the above cases for $\mathsf{delete}(v)$ are indeed complete, as
the node $v^{\prime}$ has to represent a forest ($v$ is a leaf) and thus it is
not possible that $v^{\prime}$ occurs on the left side of a context
application.

The updates relabeling, subdivision and leaf insertion are local to the node
$v$. This does not hold for deletion, as the parent node $w$ of the deleted
node will be affected if its last child is deleted. In this case we have to
change all nodes on the path between $v^{\prime}$ and $w^{\prime}$ in $\Psi$.
We note that it is easy to find the node $w^{\prime}$ within the parse tree in
this case. We are in the case 2 described above, i.e., there is a subformula
$(\Psi^{\prime}\odot v^{\prime})$ in $\Psi$. We can perform a top-down search
in $\Psi^{\prime}$ always going to the left subformula at each VH-node and the
right subformula at each HV\- and VV-node. There can be no HH\- and VH-nodes
on this path.

##  3\. Maintaining Forest Algebra Formulas under Updates

This section depicts how (parse trees for) forest algebra formulas can be
maintained when the represented tree is updated. That is, the main result of
this section is:

######  Theorem 2.

Given a tree $T$, it is possible to compute in time ${\mathcal{O}}(|T|)$ a
forest algebra formula $\Psi$ in the free forest algebra, such that

  * •

$\Psi$ represents $T$;

  * •

the parse tree of $\Psi$ is of height at most $10\log(|T|)$; and

  * •

each update to $T$ can be translated to an update of $\Psi$, such that the new
formula can be computed in time ${\mathcal{O}}(\log(|T|))$ and has height at
most $10\log(|T|)$.

In Section 3.1 we depict a high level description of the proof, before we
introduce the necessary low level tools in Section 3.2. In the sections 3.3,
3.4, and 3.5, we show how we can construct a formula for a given tree in
linear time, how we can handle insertions, and how we can handle deletions,
respectively.

###  3.1. High Level Description of the Proof

To keep the parse tree of $\Psi$ shallow, we use similar rotations, as used in
AVL trees [AVL62]. Unfortunately, the well known rotations used to balance AVL
trees only work, if the underlying algebra is fully associative, which does
not hold for forest algebras, as, e.g., $c\odot(f_{1}\oplus f_{2})\neq(c\odot
f_{1})\oplus f_{2}$. Therefore, we provide additional rotations that can be
used where the traditional rotations fail.

Towards our invariant we assign colors to nodes of a formula $\Psi$ as
follows:

$\mathsf{color}(v)\;=\;\left\\{{\begin{array}[]{llll}\text{green }&\text{ if
}&0pt(\Psi_{v})&{}\;\leq\;10\log(||\Psi_{v}||)\\\ \text{yellow}&\text{ if
}&0pt(\Psi_{v})-1&{}\;\leq\;10\log(||\Psi_{v}||)\;<\;0pt(\Psi_{v})\\\
\text{red}&\text{otherwise}\end{array}}\right.$

Strong Invariant Every node is green.

Weak Invariant There are no red nodes and there is a node $v$, such that all
yellow nodes are on $\mathsf{lp}^{-1}(v)$.

A formula $\Psi$ that satisfies either invariant has logarithmic height.

The strong invariant will hold up between runs of the insertion algorithm, but
not necessarily during the runtime of the insertion algorithm. The weak
invariant is always satisfied.

We note that if the height of a subformula is increased by one (e.g., due to
an insertion), then green nodes can become yellow and yellow nodes can become
red. Similarly, if we reduce the height of a subformula by a rotation
(introduced in the next subsection), then yellow nodes will turn green.

The crucial point in our proof that we can maintain formulas of logarithmic
height under insertions is Lemma 8 that states that whenever there is some
yellow node $v$, then we can apply some rotation $\alpha$ that either directly
reduces the height of $\Psi_{v}$ or enables another rotation $\beta$. However,
as a result of $\alpha$ or $\beta$, some node in $\Psi_{v}$ can turn yellow.
As this node is strictly below the original yellow node $v$, repeating the
process a logarithmic number of times (height of the parse tree) will
reestablish the strong invariant.

To show linear time preprocessing (i.e., a linear time algorithm to compute a
formula for a given tree) in Section 3.3, we show that our Algorithm can be
modified to do a series of $n$ insertions in overall time $O(n)$. Finally, we
introduce an algorithm that handles deletions.

###  3.2. Rotations

Rotations of formulas follow a similar spirit as rotations in AVL trees. They
rewrite the formula (preserving equivalence) in such a way that one subformula
(i.e., a subtree of the parse tree) is moved one level up and another
subformula is moved one level down. Formally, rotations are defined on the
algebraic level as follows:

$\begin{array}[]{r@{\;}lc}\hline\cr\hline\cr\lx@intercol\hfil\text{Rotation}\hfil\lx@intercol&\text{Sketch
of Parse Tree}\\\
\hline\cr(x_{1}{}_{HH}x_{2}){}_{HH}x_{3}\;\;=&x_{1}{}_{HH}(x_{2}{}_{HH}x_{3})&\hbox{\multirowsetup
\leavevmode\hbox to150pt{\vbox to68.43pt{\pgfpicture\makeatletter\hbox{\hskip
38.88867pt\lower-60.09695pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{65.44142pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\ovoid$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{46.95741pt}{-24.01276pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{62.33458pt}{-3.533pt}\pgfsys@lineto{51.21504pt}{-16.17421pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{85.35835pt}{-22.7622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\ovoid$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{}{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{68.53268pt}{-3.533pt}\pgfsys@lineto{82.2672pt}{-19.2292pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{69.71962pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{82.87292pt}{-26.29521pt}\pgfsys@lineto{73.97725pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{92.48183pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{3}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{87.84378pt}{-26.29521pt}\pgfsys@lineto{96.73946pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\ovoid$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.91693pt}{-22.7622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\ovoid$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{}{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-3.09126pt}{-3.533pt}\pgfsys@lineto{-16.82578pt}{-19.2292pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-35.55566pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-22.40236pt}{-26.29521pt}\pgfsys@lineto{-31.29803pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.79346pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-17.4315pt}{-26.29521pt}\pgfsys@lineto{-8.53583pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.96875pt}{-24.01276pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{3}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{3.10684pt}{-3.533pt}\pgfsys@lineto{14.22638pt}{-16.17421pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{102.77536pt}{-48.02441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\uparrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{57.25095pt}{-25.2622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\downarrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-25.26213pt}{-48.02441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\uparrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.26228pt}{-25.2622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\downarrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}{}{{}}{}{
{}{}{}}{}{} {}{}{}{}{{{}{}}}{}{{ {\pgfsys@beginscope{} {}{}{} {} {}{}{}
\pgfsys@moveto{3.59995pt}{0.0pt}\pgfsys@curveto{2.53328pt}{0.2pt}{0.79999pt}{0.79999pt}{-0.4pt}{1.49997pt}\pgfsys@lineto{-0.4pt}{-1.49997pt}\pgfsys@curveto{0.79999pt}{-0.79999pt}{2.53328pt}{-0.2pt}{3.59995pt}{0.0pt}\pgfsys@fill\pgfsys@endscope}}
}{}{}{{}}\pgfsys@moveto{19.91693pt}{-39.83395pt}\pgfsys@lineto{41.92455pt}{-39.83395pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{41.92455pt}{-39.83395pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{29.2207pt}{-36.30095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize 1a}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}{}{{}}{}{
{}{}{}}{}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{45.52449pt}{-48.36986pt}\pgfsys@lineto{23.51688pt}{-48.36986pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{23.51688pt}{-48.36986pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{29.02628pt}{-56.76395pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize 1b}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{90.18013pt}{-22.06953pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$w$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-32.16696pt}{-22.06953pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$w$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{71.37433pt}{0.69267pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$v$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.1389pt}{0.69267pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$v$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\\\
(x_{1}{}_{VH}x_{2}){}_{VH}x_{3}\;\;=&x_{1}{}_{VH}(x_{2}{}_{HH}x_{3})\\\
(x_{1}{}_{HV}x_{2}){}_{VH}x_{3}\;\;=&x_{1}{}_{HV}(x_{2}{}_{VH}x_{3})\\\
(x_{1}{}_{HH}x_{2}){}_{HV}x_{3}\;\;=&x_{1}{}_{HV}(x_{2}{}_{HV}x_{3})\\\
(x_{1}{}_{VV}x_{2}){}_{VV}x_{3}\;\;=&x_{1}{}_{VV}(x_{2}{}_{VV}x_{3})\\\
(x_{1}{}_{VV}x_{2}){}_{VH}x_{3}\;\;=&x_{1}{}_{VH}(x_{2}{}_{VH}x_{3})\\\
\hline\cr(x_{1}{}_{HV}x_{2}){}_{VH}x_{3}\;\;=&x_{1}{}_{HH}(x_{2}{}_{VH}x_{3})&\hbox{\multirowsetup
\leavevmode\hbox to150pt{\vbox to68.43pt{\pgfpicture\makeatletter\hbox{\hskip
38.88867pt\lower-60.09695pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{65.44142pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\oplus$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{46.95741pt}{-24.01276pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{62.33458pt}{-3.533pt}\pgfsys@lineto{51.21504pt}{-16.17421pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{85.35835pt}{-22.7622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\odot$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{}{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{68.53268pt}{-3.533pt}\pgfsys@lineto{82.2672pt}{-19.2292pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{69.71962pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{82.87292pt}{-26.29521pt}\pgfsys@lineto{73.97725pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{92.48183pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{3}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{87.84378pt}{-26.29521pt}\pgfsys@lineto{96.73946pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\odot$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.91693pt}{-17.00554pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${}_{\mathrlap{HV}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{}{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-3.09045pt}{-3.533pt}\pgfsys@lineto{-16.38393pt}{-18.7251pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-35.55566pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-23.44994pt}{-27.78284pt}\pgfsys@lineto{-31.29803pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.79346pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-16.38393pt}{-27.78284pt}\pgfsys@lineto{-8.53583pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.96875pt}{-24.01276pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{3}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{3.10684pt}{-3.533pt}\pgfsys@lineto{14.22638pt}{-16.17421pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{102.77536pt}{-48.02441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\uparrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{57.25095pt}{-25.2622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\downarrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-25.26213pt}{-48.02441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\uparrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.26228pt}{-25.2622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\downarrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}{}{{}}{}{
{}{}{}}{}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{19.91693pt}{-39.83395pt}\pgfsys@lineto{41.92455pt}{-39.83395pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{41.92455pt}{-39.83395pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{29.2207pt}{-36.30095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize 2a}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}{}{{}}{}{
{}{}{}}{}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{45.52449pt}{-48.36986pt}\pgfsys@lineto{23.51688pt}{-48.36986pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{23.51688pt}{-48.36986pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{29.02628pt}{-56.76395pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize 2b}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{90.18013pt}{-22.06953pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$w$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-32.16696pt}{-22.06953pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$w$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{71.37433pt}{0.69267pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$v$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.1389pt}{0.69267pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$v$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\\\
(x_{1}{}_{HV}x_{2}){}_{VV}x_{3}\;\;=&x_{1}{}_{HV}(x_{2}{}_{VV}x_{3})\\\\[42.67912pt]
\hline\cr(x_{1}{}_{VH}x_{2}){}_{VH}x_{3}\;\;=&(x_{1}{}_{VH}x_{3}){}_{HH}x_{2}&\hbox{\multirowsetup
\leavevmode\hbox to150pt{\vbox to68.43pt{\pgfpicture\makeatletter\hbox{\hskip
38.88867pt\lower-60.09695pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ } {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{82.51282pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\oplus$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{62.59589pt}{-22.7622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\odot$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{}{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{79.42155pt}{-3.533pt}\pgfsys@lineto{65.68704pt}{-19.2292pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{46.95715pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{60.11046pt}{-26.29521pt}\pgfsys@lineto{51.21478pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{69.71936pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{3}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{65.08131pt}{-26.29521pt}\pgfsys@lineto{73.97699pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{92.48157pt}{-24.01276pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{85.61966pt}{-3.533pt}\pgfsys@lineto{96.7392pt}{-16.17421pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {{}}{{{
{}{}{}}}}{}{}\hbox{\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{0.0pt}{0.0pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\odot$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-19.91693pt}{-17.00554pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{${}_{\mathrlap{VH}}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {{{ {}{}{}}}}{}{}{
{}{}{}}{}{ {}{}{}} {{{{{}}{ {}{}}{}{}{{}{}}}}}{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}{}\pgfsys@moveto{-3.09045pt}{-3.533pt}\pgfsys@lineto{-16.38393pt}{-18.7251pt}\pgfsys@stroke\pgfsys@invoke{
}\hbox{\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-35.55566pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{1}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-23.44994pt}{-27.78284pt}\pgfsys@lineto{-31.29803pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-12.79346pt}{-46.77496pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{2}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{-16.38393pt}{-27.78284pt}\pgfsys@lineto{-8.53583pt}{-38.93642pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}}\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{{}}{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{ {}{}}
{{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{9.96875pt}{-24.01276pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$x_{3}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { { {}{}{}}{}{ {}{}{}}
{}{{{{{}}{
{}{}}{}{}{{}{}}}}}{{}}{}{}{}\pgfsys@moveto{3.10684pt}{-3.533pt}\pgfsys@lineto{14.22638pt}{-16.17421pt}\pgfsys@stroke\pgfsys@invoke{
} }\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{80.0129pt}{-48.02441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\uparrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{102.7751pt}{-25.2622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\downarrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.49992pt}{-48.02441pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\uparrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{20.26228pt}{-25.2622pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\downarrow$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}{}{{}}{}{
{}{}{}}{}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{8.536pt}{-39.83395pt}\pgfsys@lineto{33.38846pt}{-39.83395pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{33.38846pt}{-39.83395pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.26219pt}{-36.30095pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize 3a}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} { {}{}{}}{}{}{}{{}}{}{
{}{}{}}{}{}
{}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{36.9884pt}{-48.36986pt}\pgfsys@lineto{12.13594pt}{-48.36986pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{-1.0}{0.0}{0.0}{-1.0}{12.13594pt}{-48.36986pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.06776pt}{-56.76395pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{\scriptsize 3b}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{67.41766pt}{-22.06953pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$w$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-32.16696pt}{-22.06953pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$w$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{88.44572pt}{0.69267pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$v$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}} {
{}{}{}}{}{}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}{}{{ {}{}}}{
{}{}} {{}{{}}}{{}{}}{}{{}{}} { }{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-11.1389pt}{0.69267pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$v$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope{}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}} }\\\
(x_{1}{}_{VH}x_{2}){}_{VV}x_{3}\;\;=&(x_{1}{}_{VV}x_{3}){}_{VH}x_{2}\\\\[42.67912pt]
\hline\cr\hline\cr\end{array}$ Table 3. Rotations as equations (left) and
parse trees (right). Vertical arrows indicate that the respective subformula
is moved one level up or down in the rotation. We will refer to individual
rotations using the numbers on the horizontal arrows.

A _rotation_ $\alpha$ is a rewriting of a forest algebra formula $\Psi$ into
an equivalent forest algebra formula $\alpha(\Psi)$ using one of the equations
in Table 3, where $x_{1}$ to $x_{3}$ are variables that can be replaced by
arbitrary formulas of the correct type.

A rotation $\alpha$ can be applied on a node $v$ of a formula $\Psi$, if
$\Psi_{v}$ is there is a homomorphism $\mathsf{hom}$ mapping
$x_{1},x_{2},x_{3}$ to forest algebra formulas $\Psi_{1},\Psi_{2},\Psi_{3}$
such that $\mathsf{hom}(\Psi_{\mathsf{pre}})=\Psi_{v}$. The result of applying
$\alpha$ at $v$ is the formula $\alpha(\Psi,v)$, where $\Psi_{v}$ is replaced
by $\mathsf{hom}(\Psi_{\mathsf{post}})$. We like to stress that all rotations
can be applied in both directions.

In Table 3, next to the equations defining the rotations, we depict graphical
representations of the rotations. We have annotated the nodes labeled $x_{1}$,
$x_{2}$, and $x_{3}$ with arrows $\uparrow$, $\downarrow$ to denote that the
subformula is moved upwards or downwards in the rotation. For the rotations 1a
and 1b, all operations depicted by -nodes need either to be concatenations or
context applications, but no mixture. E.g., the rotations 1a in the figure
depicts 6 different rotations, as can be seen in Table 3. All -nodes could be
HH in case that $x_{1}$, $x_{2}$, and $x_{3}$ are forests, there are three
other possibilities for concatenations, where exactly one of $x_{1}$, $x_{2}$,
and $x_{3}$ depicts a context. Additionally there are two possibilities
involving context applications. The rotations 2a, 2b, 3a, and 3b change the
order in which a concatenation and a context application are performed. This
also changes the relative order of the operands $x_{2}$ and $x_{3}$ in the
rotations 3a and 3b.

Figure 4 depicts a tree $T$, a formula $\Psi$ representing $T$ and the formula
$\alpha(\Psi,v)$ that results from applying rotation 3b at the node marked
with $v$.

$a$$b$$c$$d$$\vphantom{d}e$$f$$a_{\scaleobj{0.75}{\Box}}$$b_{\scaleobj{0.75}{\Box}}$$c_{\scaleobj{0.75}{\Box}}$$d$$\vphantom{d}e$$f$$a_{\scaleobj{0.75}{\Box}}$$b_{\scaleobj{0.75}{\Box}}$$c_{\scaleobj{0.75}{\Box}}$$f$$d$$\vphantom{d}e$$v$$w$
Figure 4. Example of rotation 3b applied at node $v$

######  Lemma 3.

The rotations depicted in Table 3 are valid operations, i.e. the equations
hold for all possible substitutions of $x_{1}$ to $x_{3}$ with formulas of the
correct type.

######  Proof 3.1.

The equations in Table 3 follow immediately from the axioms of associativity
and interaction in Table 2.

Technically, a rotation is applicable at a node $v$ of a formula $\Psi$
whenever the structure of $\Psi_{v}$ corresponds to the structure required by
the rotation. E.g., rotation 1a is applicable whenever the node $v$ and its
left child are both labeled with or both are labeled with . Obviously,
applying a rotation does not always increase the “balancedness” of the
formula. In order to increase the balancedness of a formula, we only apply a
rotation, if the balances of $v$ and $w$ are as indicated in Table 4. As
depicted in the table, depending on the balances, we classify the rotations
into height reducing rotations and height preserving rotations.

rotation |  | height reducing |  | height preserving
---|---|---|---|---
|  | $\mathsf{balance}(v)$ | $\mathsf{balance}(w)$ |  | $\mathsf{balance}(v)$ | $\mathsf{balance}(w)$
1a |  | $\leq-2$ | $<0$ |  | $\leq-2$ | $>0$
1b |  | $\geq+2$ | $>0$ |  |  |
2a |  | $\leq-2$ | $<0$ |  | $\leq-2$ | $>0$
2b |  | $\geq+2$ | $>0$ |  |  |
3a |  | $\leq-2$ | $>0$ |  | $\leq-2$ | $<0$
3b |  | $\leq-2$ | $>0$ |  |  |
Table 4. Balance conditions for height reducing and normalizing rotations

We now have two lemmas further characterizing the effects of height reducing
and height preserving rotations. To ease the presentation of the lemmas and
their proofs we introduce some more notation. We depict the subformulas of the
rotations by their movement, i.e., we depict by $\Psi_{\uparrow}$ the
subformula (among $x_{1}$, $x_{2}$, and $x_{3}$, see Table 3) that is moved
one level up. Similarly we depict by $\Psi_{\downarrow}$ the subformula that
is moved one level down and by $\Psi_{\rightarrow}$ the subformula that stays
on the same level. E.g. for rotation 1a, $\Psi_{\uparrow}=x_{1}$,
$\Psi_{\downarrow}=x_{3}$, and $\Psi_{\rightarrow}=x_{2}$ and for rotation 1b,
the roles of $\Psi_{\uparrow}$ and $\Psi_{\downarrow}$ are reversed, i.e.,
$\Psi_{\uparrow}=x_{3}$ and $\Psi_{\downarrow}=x_{1}$. Furthermore, we use
$v^{\prime}$ and $w^{\prime}$ to denote the nodes $v$ and $w$ after the
rotation.

Using this notation, we have that for all rotations it holds that prior to the
rotation, $\Psi_{\uparrow}$ and $\Psi_{\rightarrow}$ are the two children of
$w$ and $\Psi_{\downarrow}$ is the other child of $v$ (i.e., the sibling of
$w$). Similarly, after the rotation $\Psi_{\uparrow}$ is a child of
$v^{\prime}$ and $\Psi_{\downarrow}$ and $\Psi_{\rightarrow}$ are the children
of $w^{\prime}$.

######  Lemma 4.

Let $\alpha$ be a height reducing rotation that is applicable at $v$, then

  1. (1)

$\alpha$ reduces the height of $\Psi_{v}$ by one, i.e.,
$0pt(\alpha(\Psi_{v}))=0pt(\Psi_{v})-1$;

  2. (2)

$\alpha$ decreases the balance of $\Psi_{v}$ by at least two, i.e.,
$\mathcal{B}(\alpha(\Psi_{v}))\leq\mathcal{B}(\Psi_{v})-2$;

  3. (3)

all yellow nodes on $\mathsf{lp}^{-1}(v)$ change their color to green;

  4. (4)

all nodes on $\mathsf{lp}^{-1}(v)$ except $v$ decrease their absolute balance
by one; and

  5. (5)

the color of $w^{\prime}$ is yellow or green if all nodes in $\Psi_{v}$ are
green.

We remind that $\mathcal{B}(\Psi)$ denotes the sum of the absolute balances of
all nodes in $\Psi$.

######  Proof 3.2.

We first observe that by the condition on the balances, we have that

$0pt(\Psi_{\uparrow})\quad>\quad\max\big{(}0pt(\Psi_{\downarrow}),0pt(\Psi_{\rightarrow})\big{)}\;.$
($\dagger$)

  1. (1)

The statement follows from ($\dagger$ ‣ 3.2) and the fact that
$\Psi_{\uparrow}$ is moved one level up.

  2. (2)

We now compute the change of $\mathcal{B}(\Psi_{v})$. As the balances of the
subformulas $\Psi_{\uparrow}$, $\Psi_{\downarrow}$, and $\Psi_{\rightarrow}$
do not change, it is enough to look at the balances of $v$ and $w$. As we are
only interested in changes of the absolute value of the balances, it does not
matter which child is the left/right child of $v$ and $w$.

$\displaystyle|\mathsf{balance}(v)|$ $\displaystyle=$ $\displaystyle
0pt(\Psi_{\uparrow})+1-0pt(\Psi_{\downarrow})$
$\displaystyle|\mathsf{balance}(w)|$ $\displaystyle=$ $\displaystyle
0pt(\Psi_{\uparrow})-0pt(\Psi_{\rightarrow})$
$\displaystyle|\mathsf{balance}(v^{\prime})|$ $\displaystyle=$ $\displaystyle
0pt(\Psi_{\uparrow})-\max\big{(}0pt(\Psi_{\downarrow}),0pt(\Psi_{\rightarrow})\big{)}-1$
$\displaystyle|\mathsf{balance}(w^{\prime})|$ $\displaystyle=$
$\displaystyle|0pt(\Psi_{\rightarrow})-0pt(\Psi_{\downarrow})|$

We note that the right sides of the first three equations cannot be negative
because of ($\dagger$ ‣ 3.2), which is why we can avoid taking the absolute
value. Using the fact that $a+b+|a-b|=2\max(a,b)$ for arbitrary numbers $a$
and $b$, we can now compute the change of overall balance as

$\displaystyle\mathcal{B}(\Psi_{v})-\mathcal{B}(\Psi_{v^{\prime}})\;\;$
$\displaystyle=\;\;|\mathsf{balance}(v)|+|\mathsf{balance}(w)|-|\mathsf{balance}(v^{\prime})|-|\mathsf{balance}(w^{\prime})|$
$\displaystyle=\;\;0pt(\Psi_{\uparrow})-\max\big{(}0pt(\Psi_{\downarrow}),0pt(\Psi_{\rightarrow})\big{)}+2\;.$

By ($\dagger$ ‣ 3.2), we get that $\mathcal{B}(\Psi_{v})$ is decreased by at
least 2.

  3. (3)

As by (a), the height of $\Psi_{v}$ is reduced by one, the height of each
$\Psi_{u}$ with $u\in\mathsf{lp}^{-1}(v)$ is decreased by one. As the number
of leaves does not change, the definition of colors implies that yellow nodes
on $\mathsf{lp}^{-1}(v)$ turn green.

  4. (4)

It is a direct consequence of (a), that all nodes on $\mathsf{lp}^{-1}(v)$
except $v$ decrease their absolute balance by one.

  5. (5)

It is a trivial observation from the definition of colors that the parent node
$w$ of two green nodes has to be green or yellow. The height of $\Psi_{w}$ is
exactly one more than the height of the deeper subtree (which is colored
green) and $\Psi_{w}$ contains more leaves than this subtree.

The overall idea of our algorithm is to use height reducing rotations whenever
the height of some (sub)formula was increased by the insertion of a new node
or some (sub)formula needs to be reduced in height after some deletions.
However, there are some situations in which no height reducing rotation can be
applied, even if the formula is severely imbalanced. In these cases we use
height preserving rotations in order to restructure the formula in such a way
that afterwards height reducing rotations can be applied.

######  Lemma 5.

Let $\alpha$ be a height preserving rotation that is applicable at $v$, then

  1. (1)

$0pt(\alpha(\Psi_{v}))=0pt(\Psi_{v})$;

  2. (2)

$|\mathsf{balance}(v^{\prime})|=|\mathsf{balance}(w)|+1$;

  3. (3)

$|\mathsf{balance}(w^{\prime})|=|\mathsf{balance}(v)|-1$;

  4. (4)

$\mathcal{B}(\alpha(\Psi_{v}))=\mathcal{B}(\Psi_{v})$; and

  5. (5)

the color of $w^{\prime}$ is green if there is a node $u\in\mathsf{lp}(v)$
with $|\mathsf{balance}(u)|\leq 1$ at most six levels below $v$ and all nodes
in $\Psi_{u}$ are green or yellow.

######  Proof 3.3.

Again, we denote by $\Psi_{\uparrow}$, $\Psi_{\downarrow}$, and
$\Psi_{\rightarrow}$ the subformulas that moves one level up, moves one level
down, and stays on the same level, respectively. The condition on balances for
height preserving rotations state that
$0pt(\Psi_{\downarrow})<\max(0pt(\Psi_{\uparrow}),0pt(\Psi_{\rightarrow}))$
and $0pt(\Psi_{\rightarrow})>0pt(\Psi_{\uparrow})$. We can conclude

$0pt(\Psi_{\rightarrow})\quad>\quad\max\big{(}0pt(\Psi_{\uparrow}),0pt(\Psi_{\downarrow})\big{)}\;.$
($\ddagger$)

Now we show the individual statements:

  1. (1)

The statement follows from ($\ddagger$ ‣ 3.3) and the fact that
$\Psi_{\rightarrow}$ stays on the lower level.

  2. (2)

$\begin{aligned}
\phantom{|\mathsf{balance}(w^{\prime})|}\mathllap{|\mathsf{balance}(v^{\prime})|}\;\;&=\;\;|0pt(\Psi_{\uparrow})-\max\big{(}1+0pt(\Psi_{\rightarrow}),1+0pt(\Psi_{\downarrow})\big{)}|\\\
&=\;\;0pt(\Psi_{\rightarrow})-0pt(\Psi_{\uparrow})+1\\\
&=\;\;|\mathsf{balance}(w)|+1\end{aligned}$

  3. (3)

$\begin{aligned}
|\mathsf{balance}(w^{\prime})|\;\;&=\;\;0pt(\Psi_{\rightarrow})-0pt(\Psi_{\downarrow})\\\
&=\;\;|\max\big{(}0pt(\Psi_{\rightarrow}),0pt(\Psi_{\uparrow})\big{)}+1-0pt(\Psi_{\downarrow})|-1\\\
&=\;\;|\mathsf{balance}(v)|-1\end{aligned}$

  4. (4)

This follows from (b) and (c), as no other nodes in $\Psi_{v}$ change their
balance.

  5. (5)

We bound the number of leaves in $\Psi_{w^{\prime}}$ as follows:

$\displaystyle||w^{\prime}||\;\;$
$\displaystyle>\;\;||\Psi_{\mathsf{child_{L}}(u)}||+||\Psi_{\mathsf{child_{R}}(u)}||$
$\Psi_{u}$ is a subformula of $\Psi_{w^{\prime}}$
$\displaystyle\geq\;\;2^{\frac{0pt(\Psi_{\mathsf{child_{L}}(u)})}{10}}+2^{\frac{0pt(\Psi_{\mathsf{child_{R}}(u)})}{10}}$
definition of colors
$\displaystyle\geq\;\;2^{\frac{0pt(\Psi_{w^{\prime}})-7}{10}}+2^{\frac{0pt(\Psi_{w^{\prime}})-8}{10}}$
relative height of nodes $\displaystyle>\;\;2\cdot
2^{\frac{0pt(\Psi_{v})-8}{10}}\;\;=\;\;2^{\frac{0pt(\Psi_{v})+2}{10}}$

The statement follows now from the definition of colors.

In some cases, we use double rotations, which are exactly the double rotations
used in AVL trees. We only apply double rotations if there are three
consecutive -nodes $v_{1}$, $v_{2}$, $v_{3}$ on $\mathsf{lp}(v_{1})$ where the
direction of the balances alternates. A double rotation then consists of a
height preserving rotation at $v_{2}$ followed by a height reducing rotation
at $v_{1}$. We depict the two possibilities for double rotations in Figure 5
and will denote them as rotations 4a and 4b respectively. From Lemma 5(e) we
get the following corollary.

$x_{1}$$x_{2}$$x_{3}$$x_{4}$$x_{1}$$x_{2}$$x_{3}$$x_{4}$$x_{1}$$x_{2}$$x_{3}$$x_{4}$$x_{1}$$x_{2}$$x_{3}$$x_{4}$$x_{1}$$x_{2}$$x_{3}$$x_{4}$1b
at $v_{2}$1a at $v_{1}$1b at $v_{1}$1a at
$v_{2}$4a4b$v_{1}$$v_{1}$$v_{1}$$v_{1}$$v_{2}$$v_{2}$$v_{3}$$v_{3}$$w_{1}$$w_{2}$
Figure 5. Double Rotations. The first rotation is always a rotation 1a or 1b
at $w$ followed by a rotation in the opposite direction at $v$. We denote
double rotations as rotations 4a and 4b, respectively.

######  Corollary 6.

If all nodes are green or yellow and a double rotation is applied at some node
$v$ that has a node $u$ with $|\mathsf{balance}(u)|\leq 1$ at most 7 levels
below on $\mathsf{lp}(v)$, then the node $w_{1}$ as indicated in Figure 5 (in
case of rotation 4a) or the node $w_{2}$ (in case of rotation 4b) is green
after the rotation.

We note that the node $w_{1}$ or $w_{2}$ is the node $w^{\prime}$ of the first
of the two rotations in the double rotation. Therefore, we can directly apply
Lemma 5(e).

Given a formula $\Psi$ and a node $v$ in $\Psi$, there is at most one rotation
$\alpha$ that can be applied at $v$ while respecting the balance conditions in
Table 4.

The following two lemmas are heavily used in all our algorithms. They
establish that whenever the formula is heavily imbalanced, then the balance
can be improved as some rotation is possible.

######  Lemma 7.

Let $\Psi$ be a formula that only has green and yellow nodes and $v$ be a
yellow node. Let $\mathsf{lp}(v)=v_{1}\cdots v_{k}$ be the long path starting
at $v$. Then $k\geq 8$ and for $1\leq i\leq 8$ it holds that $|B(v_{i})|\geq
2$.

######  Proof 3.4.

Let $h=0pt(\Psi_{v})$ be the height of $\Psi_{v}$ and $j\in\\{1,\dots,k\\}$ be
the smallest number such that $|\mathsf{balance}(v_{j})|<2$. As every long
path ends with a node of balance 0, such a $j$ exists. By definition of
balances and paths in trees, we have that the height of $\Psi_{v_{j}}$ is
$h-j$ and the heights of the two subformulas of $\Psi_{v_{j}}$ are $h-j-1$ and
$h-j-1-|\mathsf{balance}(v_{j})|$. As both subformulas of $\Psi_{v_{j}}$ only
have green and yellow nodes, we can conclude that $\Psi_{v_{j}}$ has at least

$2^{\frac{h-j-1}{10}}+2^{\frac{h-j-1-|\mathsf{balance}(v_{j})|}{10}}\;\;\geq\;\;2\cdot
2^{\frac{h-j-2}{10}}\;\;=\;\;2^{\frac{h-j+8}{10}}$

many leaves, where $h-j$ and $h-j-|\mathsf{balance}(v_{j})|$ are the heights
of the children of $v_{j}$. The inequality follows by
$|\mathsf{balance}(v_{j})|\leq 1$. As $v$ is yellow, i.e.,
$||\Psi_{v}||<2^{\frac{h}{10}}$, and $||\Psi_{v_{j}}||<||\Psi_{v}||$, we can
conclude that $j$ has to be at least 9. This concludes the proof.

######  Lemma 8.

Let $\Psi$ be a formula and $v$ be a node in $\Psi$ such that the first 8
nodes on $\mathsf{lp}(v)$ have an absolute balance of at least two. Then there
is a node $u\in\mathsf{lp}(v)$, such that either

  * •

a height reducing rotation is applicable at $u$;

  * •

a height reducing double rotation is applicable at $u$; or

  * •

$u$ is a -node, $\mathsf{balance}(u)\leq-2$ and a height preserving rotation
is applicable at $u$.

######  Proof 3.5.

We denote the nodes on $\mathsf{lp}(v)$ by $v_{1},\dots,v_{k}$. By
precondition, we have $|\mathsf{balance}(v_{i})|\geq 2$ for $1\leq i\leq 8$.
We show the statement by a series of case distinctions on the balances and
labels of the nodes $v_{1},\dots,v_{8}$.

The first case is that there is a -node $v_{i}$ with $i<8$ and
$\mathsf{balance}(v_{i})\leq-2$. In this case we can apply one of the
rotations $1a$ (if $v_{i+1}$ is a -node), $2a$ (if $v_{i+1}$ is a HV-node), or
$3a$ (if $v_{i+1}$ is a VH-node). We note that $v_{i+1}$ cannot be a HH-node
as $\Psi_{v_{i+1}}$ must represent a context. This rotation is either height
reducing or height preserving, depending on the sign of
$\mathsf{balance}(v_{i+1})$.

From now on, we assume that all -nodes from $v_{1},\dots,v_{7}$ have a
positive balance, as otherwise the first case would apply. We note that by
assumption none of these nodes can have a balance of $-1$, $0$, or $+1$.

The second case is that there are two consecutive -nodes $v_{i}$ and $v_{i+1}$
with $i\leq 6$. In this case, we can apply the height reducing rotation 1b at
$v_{i}$.

The third case is that there are three consecutive -nodes $v_{i}$, $v_{i+1}$,
and $v_{i+2}$ with $i\leq 5$. In this case, we can apply one of the rotations
1a, 1b, 4a, or 4b, depending on the signs of $\mathsf{balance}(v_{i})$ and
$\mathsf{balance}(v_{i+1})$.

Case 4: If none of the first three cases apply, then there are neither two
consecutive -nodes nor three consecutive -nodes on $v_{1},\dots,v_{7}$. But
then there have to be two -nodes $v_{i}$ and $v_{j}$ both immediately followed
by -nodes $v_{i+1}$ and $v_{j+1}$ with $1\leq i<j\leq 6$.

Case 4a: $v_{i}$ is a HH-node, $v_{i}$ is a VH-node with
$\mathsf{balance}(v_{i})<0$, or $v_{i}$ is a HV-node with
$\mathsf{balance}(v_{i})>0$. In this case we can either apply height reducing
rotation 2b or height reducing rotation 3b. We remind that the -node $v_{i+1}$
has a positive balance, as otherwise case 1 would apply.

Case 4b: The remaining cases are that $v_{i}$ is a VH-node with
$\mathsf{balance}(v_{i})>0$ or $v_{i}$ is a HV-node with
$\mathsf{balance}(v_{i})<0$. In both cases, $\Psi_{v_{i+1}}$ represents a
forest. If $\Psi_{v_{i+1}}$ represents a forest, then all nodes $v_{\ell}$
with $i<\ell\leq 7$ are either HH or VH nodes. A formula that represents a
forest must have either a HH-node or a VH-node at the top. For a HH-node, both
subformulas have to represent forests, and for a VH-node, the right subformula
has to represent a forest. And on $\mathsf{lp}(v)$ we are always going to the
right subformula at each -node, as we assume that these nodes have positive
balance. Therefore, $v_{j}$ has to be a HH-node and we can either apply 2b or
3b. This concludes the proof.

###  3.3. Preprocessing in Linear Time

This subsection is devoted to prove the following theorem:

######  Theorem 9.

Given a tree $T$, one can construct a formula $\Psi$ of height $O(\log(|T|))$
that represents $T$ in time $O(|T|)$.

We depicted the algorithm as Algorithm 1. The function construct should be
called with the root of $T$ and a formula $\Psi$ that consists of just the
single node representing the root. The function does a preorder traversal of
$T$ and inserts each node into $\Psi$, using either subdivision (to insert the
first child of some node) or leaf insertion (to insert all other children). As
the insertion increases the height of the subformula $\Psi_{v}$, the algorithm
calls the function optimizeUpwards that goes upwards and searches for a place
to apply a height reducing rotation. A height reducing rotation at some node
$u$ neutralizes the height increase due to the insertions for the ancestors of
$u$. If optimizeUpwards does not find a possibility for a height reducing
rotation, it does not modify the formula. It stops once it reaches a node
whose height did not change, because the insertion was in the shallower
subtree. For a more detailed description of how optimizeUpwards works, we
refer to the following proofs, especially the proof of Lemma 12.

After a complete formula is constructed, the algorithm optimizes the complete
formula by doing a postorder traversal of the formula and applying all
possible rotations. This optimizing step is necessary, as the construction
does not apply all possible rotations and might create subformulas that are of
height linear in the number of nodes in the subformula. Especially if we allow
deletions later, this might lead to formulas that are heavily unbalanced.

Algorithm 1 Construct Formula $\Psi$

1:function construct($v_{t}$: a node of $T$, $v$: leaf of $\Psi$ corresponding
to $v_{t}$)

2: if $v_{t}$ has a child then

3: $\mathsf{subdiv}(v,\mathsf{lab}(\text{first-child}(v_{t})))$
$\triangleright$ see Section 2

4: $\textsc{optimizeUpwards}(\mathsf{Parent}(v))$

5: $\textsc{construct}(\text{first-child}(v_{t}),\mathsf{child_{R}}(v))$

6: if $v_{t}$ has a right sibling then

7: $\mathsf{insert_{R}}(v,\mathsf{lab}(\text{next-sibling}(v_{t})))$
$\triangleright$ see Section 2

8: $\textsc{optimizeUpwards}(\mathsf{Parent}(v))$

9: $\textsc{construct}(\text{next-sibling}(v_{t}),\mathsf{child_{R}}(v))$

10: $\textsc{optimizeAll}(\mathsf{root}(\Psi))$

11:function optimizeUpwards($v$: node in some formula $\Psi$)

12: while $v\neq\bot$ and no height reducing rotation was done do

13: if $\textsc{hr-rotationPossible}(v)$ then

14: $\textsc{DoRotation}(v)$

15: else if $v$ is a -node with $\mathsf{balance}(v)\leq-7$ then

16: while height preserving rotation possible at $v$ do

17: $\textsc{DoRotation}(v)$

18: $v\leftarrow\mathsf{child_{D}}(v)$ $\triangleright$ Go to the deeper
subformula

19: else

20: $v\leftarrow\begin{cases}\mathsf{Parent}(v)&\text{if
$v=\mathsf{child_{D}}(\mathsf{Parent}(v))$}\\\
\bot&\text{otherwise}\end{cases}$ $\triangleright$ [t]10cmstop if $\Psi_{v}$
is not deeper

21:than its sibling

22:function optimizeAll($v$: node in some formula $\Psi$)

23: if $v$ is an inner node then

24: $\textsc{optimizeAll}(\mathsf{child_{L}}(v))$

25: $\textsc{optimizeAll}(\mathsf{child_{R}}(v))$

26: $\textsc{doAllRotations}(\Psi,v)$

27:function doAllRotations($v$: node in some formula $\Psi$)

28: while $\textsc{rotationPossible}(v)$ do

29: $\textsc{DoRotation}(v)$

30: $\textsc{doAllRotations}(\Psi,\mathsf{child_{L}}(v))$

31: $\textsc{doAllRotations}(\Psi,\mathsf{child_{R}}(v))$

######  Lemma 10.

Algorithm 1 is correct, i.e., after the algorithm the formula $\Psi$
represents the tree $T$.

######  Proof 3.6.

It is straightforward to verify that the function construct does indeed
construct a correct formula if one ignores all calls to optimizeUpwards and
the call to optimizeAll. The function does a preorder traversal of $T$ and
inserts each node it finds into the formula.

The only changes applied to the formula by the functions optimizeUpwards and
optimizeAll are rotations. By Lemma 3, which says that rotations do not change
the represented tree, we get that Algorithm 1 does indeed construct a formula
that represents $T$.

Furthermore, it is easy to see that after the algorithm is finished, no
rotation can be applied. Therefore, lemmas 7 and 8 give us the following:

######  Corollary 11.

Algorithm 1 produces a formula that satisfies the strong invariant.

It remains to show that the algorithm runs in linear time in the size of $T$.
Even if phrased differently, the main idea of the proof follows the line of an
amortized analysis that Mehlhorn and Tsakilidis [MT86] did for AVL trees. We
first analyze the behavior of optimizeUpwards at -nodes with a big negative
balance.

######  Lemma 12.

If the function optimizeUpwards arrives at a -node $u$ with
$\mathsf{balance}(u)\leq-7$, then it applies a series of height preserving
rotations, followed by a height reducing rotation on $\mathsf{lp}(u)$.

######  Proof 3.7.

In the proof we use nodes $v$ and $w$ of a rotation as defined in Table 3 and
nodes $v^{\prime}$ and $w^{\prime}$ to refer to the nodes $v$ and $w$ after
the rotation.

Let $u$ be a -node with $\mathsf{balance}(u)\leq-7$. We first observe that at
a -node with a balance less than minus one, the only possibility that no
rotation is applicable is that the left child has balance 0. Otherwise we
could apply one of the rotations 1a, 1b, 2a, or 3a. However, it is impossible
that the deep child of the current node has balance 0, as the Algorithm would
have stopped before reaching this child (see Line 21). If the possible
rotation is height reducing, we are done. Otherwise, the rotation is height
preserving and the node $w^{\prime}$ of the rotation is the deep child of
$v^{\prime}$ after the rotation. The balance of $w^{\prime}$ is one more
(i.e., it is less negative) than the balance of $v$ was before the rotation
(Lemma 5(c)), and this node $w^{\prime}$ has to be a -node. The algorithm
continues until either a height reducing rotation is possible at the current
node or it has done at least six height preserving rotations in a row, as the
balance of the next node it looks at is always exactly one more than the
previous one (Lemma 5(c)). In the former case, we apply the height reducing
rotation and are done. In the latter case, the nodes where the algorithm
applied height preserving rotations are consecutive on
$\mathsf{lp}^{-1}(u^{\prime})$, where $u^{\prime}$ is the lowest node where a
height preserving rotation was performed. By Lemma 5(b) all those nodes have
an absolute balance of at least 2. Therefore, by Lemma 8, a height reducing
rotation is possible at one of these nodes. The algorithm will go upwards
again once no height preserving rotation is possible any more, apply this
height reducing rotation and stop. It will therefore not go above $u$, which
concludes the proof.

We introduce a bit of notation that helps with the following proof. For the
amortized analysis, we use the following potential function:

$\Phi(\Psi)\quad=\quad|\\{v\enspace|\enspace\mathsf{balance}(v)=0\\}|\;\;+\;\;\quad\sum_{\mathclap{\pbox{10cm}{\scriptsize\begin{aligned}
v\in\\{w\in\Psi\;|\;\mathsf{lab}(w)=\odot\text{ and }&\\\
-6\leq\mathsf{balance}(w)\leq 0\\}&\end{aligned}}}}\quad
7+\mathsf{balance}(v)$

The first term counts the number of nodes in $\Psi$ with balance 0. These
nodes can get an absolute balance of 1 by the insertion. They have to be
skipped when going upwards as no rotation is possible. The second term, i.e.,
the sum, accounts for -nodes with a balance between $-6$ and $0$. These nodes
also might have to be skipped when going upwards. How often the same node can
be skipped during consecutive insertions depends on its balance. Once the
imbalance is big enough, we know that we can perform a series of height
preserving rotations followed by one height reducing rotation. We note that
for these nodes the balance is always negative and thus
$7+\mathsf{balance}(w)$ produces numbers between 1 and 6 inclusive. The number
corresponds to how often a node might need to be skipped. Obviously,
$\Phi(\Psi)$ cannot be negative.

######  Lemma 13.

The summarized runtime of all calls to optimizeUpwards in Algorithm 1 is in
$O(|T|)$.

######  Proof 3.8.

We analyze the change of the potential $\Phi(\Psi)$ during an insertion
operation. We need to show two things, that the potential is increased by at
most a constant value during the insertion operation, and that the runtime is
linear in the overall decrease of potential. We are not allowed to calculate
with the net change of potential. Instead we have to account for increments
and decrements separately.

First of all, we calculate the increments. The insertion adds a new inner node
that has a balance of 0 and could be a -node. This increases the potential by
at most 8. If the algorithm does not perform a height reducing rotation, then
the absolute balance of the parent of the topmost node $u$ reached by the call
optimizeUpwards will decrease by 1. This can increase the potential by at most
2. All other changes of balance that directly result from the insertion (and
not from a rotation) can only increase the absolute balance of some node. Thus
they cannot increase the potential.

We already know that the algorithm performs at most one height reducing
rotation (as it will directly stop afterwards) and at most one series of
height preserving rotations, i.e., it enters the while-loop in Line 16 at most
once. After one series of height preserving operations, either a height
reducing rotation is possible at the current node, or at most six nodes above
(see discussion of the algorithm above). All nodes where we did a height
preserving rotation will have an absolute balance of at least two and if they
are a -node have a positive balance. Thus these nodes cannot have increased
their potential, due to the rotations. We only need to account for an
increased potential due to the height reducing rotation and for the $w$-node
of the last height preserving rotation. This can be at most constant. We note
that the balances of the ancestors of the highest node reached in the whole
insertion operation cannot change if we do perform a height reducing rotation,
as this rotation cancels out the height increase due to the insertion.

We still need to look at the nodes on the path from $u$ to
$\mathsf{Parent}(v)$. The absolute values of the balances of these nodes
increase by one. This will decrease the potential $\Phi(\Psi)$ by one for
every node that changes the balance from zero to some non-zero value, i.e.,
for every node on the path that prior to the insertion had a balance of zero.
Furthermore it decreases the potential by one for ever -node that has a
balance between $-6$ and $0$ (inclusive). We now show that the decrease in
potential is linear in the runtime of optimizeUpwards.

In fact, by Lemma 8, at least every seventh node on the path from $u$ to
$\mathsf{Parent}(v)$ had a balance of 0, or was a -node with a balance in the
range $-6$ to 0. We remind that all nodes on this path that had a non-zero
balance before the insertion will have an absolute balance of at least 2 after
the insertion. Therefore, if there are more than six consecutive nodes that
did not have a balance of zero prior to the insertion, nor are -nodes with a
balance in the given range, either we would stop as described in Lemma 12, or
at one of these nodes we can apply a height reducing rotation. This is a
contradiction to the assumption that $u$ is the highest node reached by the
function.

As the potential cannot become negative, is increased by at most a constant
for each insertion, and is decreased by at least a number linear in the
runtime of optimizeUpwards, the summarized runtime of all calls to
optimizeUpwards is in $O(|T|)$.

It remains to show the runtime of the optimizeAll function.

######  Lemma 14.

The runtime of optimizeAll is linear in $O(|T|)$ if called from the
construction algorithm.

######  Proof 3.9.

We first observe that the total imbalance $\mathcal{B}(\Psi)$ of the formula
$\Psi$ is linear in $O(|T|)$ just before the call to optimizeAll. In fact, for
each insertion, $\mathcal{B}(\Psi)$ is only increased by one for each node on
the path from $u$ to $\mathsf{Parent}(v)$, where $u$ is the topmost node
reached by the optimizeUpwards function. As the runtime of optimizeUpwards is
in $\Theta(0pt(\Psi_{u}))$, and the summarized runtime of all those calls is
linear in $|T|$ by Lemma 13, $\mathcal{B}(\Psi)$ is linear in $|T|$. From
Lemmas 4(b and d) and 5(d) it follows that rotations performed by
optimizeUpwards can only decrease $\mathcal{B}(\Psi)$.

Towards the lemma statement, we show that the runtime of optimizeAll is linear
in $|T|+\mathcal{B}(\Psi)$. It is obvious that optimizeAll is called exactly
once for each inner node in the formula, as this is a classic post-order
traversal. And the number of calls to doAllRotations is one for each inner
node of the formula and additionally two calls for every performed rotation.
It thus suffices to show that the number of performed rotation is linear in
$\mathcal{B}(\Psi)$.

By Lemma 4(b) and 5(d) we have that height reducing rotations decrease
$\mathcal{B}(\Psi)$, while height preserving rotations do not change
$\mathcal{B}(\Psi)$. Thus we have to bound the number of height preserving
rotations. But we already know that, if there is more than a constant number
of height preserving rotations on one downwards path, there has to be a height
reducing rotation that can be applied near the downwards end of the path, as
all the nodes on the path will have an absolute balance of at least 2 and have
positive balance if they are -nodes. Thus the algorithm will apply a height
reducing rotation which decreases the value linearly in the length of the path
(Lemma 4(d)), which corresponds to the number of performed height preserving
rotations. Altogether the runtime is bounded by the size of $T$ and the
overall imbalance of $\Psi$.

Theorem 9 now follows from Lemma 10 (soundness), Corollary 11 (height of
formula) and lemmas 13 and 14 (runtime).

###  3.4. Maintaining Parse Trees under Insertions

Our proof that we can maintain the strong invariant under insertions takes
several steps. In Lemma 15, we show that after any insertion, the formula
still satisfies the weak invariant. Afterwards, we establish in Lemma 7 that
on the long path of any yellow node, there are several consecutive nodes that
are imbalanced. This is exploited in Lemma 8 to show that we can apply some
rotation to reduce the height of $\Psi_{v}$ and change the color of the yellow
node back to green. Unfortunately, the rotation might create (at most) one
other yellow node. However, as this new yellow node is strictly deeper in the
parse tree as the previous one, at most logarithmically many repetitions
suffice to reestablish the strong invariant. This leads to Algorithm 2 that we
use to recursively reestablish the strong invariant and Algorithm 3 that
performs the insertion and makes use of Algorithm 2.

######  Lemma 15.

Let $\Psi$ be a formula that satisfies the strong invariant. Then after
applying an insertion update $\Delta$ on $\Psi$, the resulting formula
$\Delta(\Psi)$ satisfies the weak invariant and all yellow nodes of
$\Delta(\Psi)$ are on $\mathsf{lp}^{-1}(v)$, where $v$ is the parent of the
newly inserted node.

######  Proof 3.10.

In all possibilities of a node insertion in the tree (insertion of a leaf as a
left/right sibling of an existing node and subdivision), a leaf of the formula
$\Psi$ is replaced by a subformula with one inner node $v$ and two leaves. One
of these leaves is the new node. Thus for all nodes on $\mathsf{lp}^{-1}(v)$
in $\Delta(\Psi)$ it holds that the height and the number of leaves in the
subtree has increased by one. For all nodes not on $\mathsf{lp}^{-1}(v)$ the
height did not change and the number of leaves in the subtree might have
increased by one. As observed in Section 3.1, for nodes on
$\mathsf{lp}^{-1}(v)$, the color can change from yellow to red, or from green
to yellow. As all nodes are green prior to the insertion, there are no red
nodes after the insertion and all yellow nodes after the insertion have to be
on $\mathsf{lp}^{-1}(v)$. Thus the weak invariant is satisfied.

Lemma 8 allows us to state Algorithm 2 that tries to optimize the height of a
given (sub-)formula. Algorithm 2 does not check the color of any nodes.
Instead it just starts at a given nodei $v$, goes downwards on the long path
and performs rotations if possible. Lemma 8 implies that finally a height
reducing rotation has to be possible if $v$ is yellow.

The test $\textsc{simpleRotationPossible}(v)$ in Line 3 returns true, if one
of the following is true:

  * •

a height reducing rotation is possible at node $v$; or

  * •

$v$ is a -node with negative balance and a height preserving rotation is
possible at $v$.

The test $\textsc{rotationPossible}(v)$ in Line 8 returns true, if one of the
two cases above applies or a height reducing double rotation is possible at
$v$. The function $\textsc{DoRotation}(v)$ in lines 4 and 9 applies the unique
(see Observation 3.2) possible rotation at node $v$ and returns the node that
is labeled with $w$ in Table 3. In case of a double rotation, it returns the
node $w_{1}$ or $w_{2}$ (see Figure 5) that can have a non-green color. We
remind that according to Corollary 6, only one of the two nodes can have a
non-green color.

In Line 8, we assume that the lowest node $u$ is used that makes the condition
true. By Lemma 8, this node $u$ is at most 8 nodes above $v$.

We now have two lemmas that characterize the effects of Algorithm 2 and one
lemma talking about the runtime.

Algorithm 2 Try to optimize the height of a subformula $\Psi_{v}$

1:function TryReduceHeight($\Psi,v$)

2: if $|\mathsf{balance}(v)|\geq 2$ then

3: if $\textsc{simpleRotationPossible}(v)$ then

4: $w\leftarrow\textsc{DoRotation}(v)$

5: $\textsc{TryReduceHeight}(\Psi,w)$

6: else

7: $\textsc{TryReduceHeight}(\Psi,\mathsf{child_{D}}(v))$

8: else if $\textsc{rotationPossible}(u)$ for some node
$u\in\mathsf{lp}^{-1}(v)$ then

9: $w\leftarrow\textsc{DoRotation}(u)$

10: $\textsc{TryReduceHeight}(\Psi,w)$

######  Lemma 16.

Let $v$ be a yellow node in a formula $\Psi$ that consists only of green and
yellow nodes. Let $\Psi_{v}^{\prime}$ denote the subformula $\Psi_{v}$ after
the call $\textsc{TryReduceHeight}(\Psi,v)$. Then
$0pt(\Psi^{\prime}_{v})<0pt(\Psi_{v})$.

######  Proof 3.11.

We use $v_{i}$ to denote the value of $v$ in the $i$-th recursion step of the
algorithm, where $v_{1}$ is the value of $v$ in the topmost call. We assume
towards a contradiction that $v_{1}$ is yellow and the height of
$\Psi_{v_{1}}$ is not changed by the algorithm.

All recursive calls are made on $\mathsf{lp}(v_{1})$ unless we perform a
height reducing rotation at some $v_{i}$, reducing the height of each
$\Psi_{v_{j}}$ with $j\leq i$ by one. Indeed, if at some node no rotation is
performed, we stay on the long path, as we are going to the deeper child. And
if a height preserving rotation is performed, the node $w$ returned by the
call doRotation is also on the deeper subformula.

As the algorithm only stops if $|\mathsf{balance}(v_{i})|<2$ and no rotation
is possible on $\mathsf{lp}^{-1}(v_{i})$, we can conclude that either a height
reducing rotation was performed on $\mathsf{lp}(v)$ and the height of
$\Psi_{v}$ did decrease as claimed in the lemma statement or no height
reducing rotation was performed at all. In the latter case, the algorithm
stops after reaching a node $v_{i}$, such that $|\mathsf{balance}(v_{i})|\leq
1$ and no rotation is possible on $\mathsf{lp}^{-1}(v_{i})$. This contradicts
Lemma 8 that says that some rotation is possible on $\mathsf{lp}(v_{1})$. We
note that by Lemma 7 it holds that $i>8$ and all nodes between $v_{1}$ and
$v_{i}$ have an absolute balance of at least 2.

The intuition of the next lemma is, that tryReduceHeight cannot create nodes
that are more imbalanced than before. For insertions, all we need is, that
tryReduceHeight does not create new yellow nodes. The more precise statement
is needed when we also consider deletions later on.

######  Lemma 17.

Let $v$ be a node in a formula $\Psi$ that consists only of green and yellow
nodes. Let $\Psi_{v}^{\prime}$ denote the subformula $\Psi_{v}$ after the call
$\textsc{TryReduceHeight}(\Psi,v)$. For any yellow node $u^{\prime}$ in
$\Psi^{\prime}_{v}$, there is a node $u$ in $\Psi_{v}$ such that
$0pt(\Psi_{u})\geq 0pt(\Psi^{\prime}_{u^{\prime}})$ and
$||\Psi_{u}||\leq||\Psi^{\prime}_{u^{\prime}}||$.

######  Proof 3.12.

We do the proof by induction. The base case is that no recursive call is
performed. In this case any yellow node in $\Psi^{\prime}$ exists identically
in $\Psi$.

If we do a recursive call without any prior rotation, the statement follows
directly from the inductive assumption. It remains to discuss the case that
the algorithm does some rotation in Line 4 or Line 9. We start with simple
rotations. So assume that there is a simple rotation on some node $u$. The
statement follows trivially for all nodes in $\Psi_{\uparrow}$, i.e., the
subformula that is moved one level up in the rotation, as this subformula is
not touched by the algorithm. It follows for $u$ (more precisely for the node
that is at the position of $u$ after the rotation) as $||\Psi_{u}||$ does not
change and $0pt(\Psi_{u})$ either does not change or is reduced by one. If the
node $w^{\prime}$ (see Table 3) is green, the statement follows trivially for
$w^{\prime}$. If it is yellow, the statement follows for $w^{\prime}$, because
it will be green after the recursive call (see Lemma 16). If $w^{\prime}$ is
red after the rotation, then $\mathsf{child_{D}}(w^{\prime})$ has to be
yellow, i.e. it is a yellow node in $\Psi$ such that
$||\Psi_{\mathsf{child_{D}}(w^{\prime})}||\leq||\Psi^{\prime}_{w^{\prime}}||$.
And $0pt(\Psi^{\prime}_{w^{\prime}})$ will be the same as
$0pt(\Psi_{\mathsf{child_{D}}(w^{\prime})})$ after the recursive call on
$w^{\prime}$, as the recursive call will reduce the height of
$\Psi_{w^{\prime}}$ by one (see Lemma 16). Finally the statement holds for all
nodes in $\Psi_{\downarrow}$ and $\Psi_{\rightarrow}$ by the inductive
assumption.

It remains to discuss double rotations in Line 9. We discuss the two rotations
of the double rotations seperately, starting with the height preserving
rotation, i.e., the first rotation of the double rotation. By Lemma 5(e), we
have that $w^{\prime}$ is green. We remind that $u$ is at most 6 nodes above
$v$ and $|\mathsf{balance}(v)|\leq 1$. And the argumentation for the second
rotation of the double rotation is exactly the same as above. It is a height
reducing rotation applied at some node $u$. This concludes the proof.

The final property that we need for the TryReduceHeight function is its
runtime. Again the lemma statement is more detailed than needed for the
insertion algorithm, as we need the additional detail later for the deletion
algorithm.

######  Lemma 18.

The runtime of $\textsc{TryReduceHeight}(\Psi,v)$ is in
$O(\Delta_{\mathcal{B}})$, where $\Delta_{\mathcal{B}}$ is the improvement of
the balance of $\Psi_{v}$, i.e.,
$\Delta_{\mathcal{B}}=\mathcal{B}(\Psi_{v})-\mathcal{B}(\Psi^{\prime}_{v})$
with $\Psi^{\prime}_{v}$ denoting the subformula $\Psi_{v}$ after the call to
TryReduceHeight.

######  Proof 3.13.

We show that $\Delta_{\mathcal{B}}\geq\max(\frac{x}{7}-7,0)$, where $x$ is the
recursion depth counting the initial call as 1. The proof is by induction. If
the algorithm never performs a height reducing rotation, then the recursion
depth is bounded by 6 by Lemma 8. If the algorithm at some point performs a
(first) height reducing rotation in Line 4, then by Lemma 4(d),
$\mathcal{B}(\Psi)$ is decreased by at least $y$, where $y$ is the (current)
recursion depth. The argument follows by induction on the recursive call in
Line 5. Let $x$ be the total recursion depth, then the recursive call has a
remaining recursion depth of $x-y$, yielding a total improvement of balance of
at least $\max(\frac{x-y}{7},0)\geq\max(\frac{x}{7}-7,0)$ using the induction
hypothesis. Similarly, if the algorithm performs a double rotation in Line 9
at recursion level $y$, then $\mathcal{B}(\Psi)$ is decreased by at least
$\max(1,y-6)\geq\frac{y}{7}$, as the node at which the double rotation is
performed is at most $6$ nodes above the current node $v$. This implies that
the improvement is at least $\frac{y}{7}$. Again, the argument follows by
induction, concluding the proof.

A direct consequence of Lemma 18 is, that the runtime is bounded by a constant
if no height reducing rotation is performed.

The final algorithm for insertions is depicted as Algorithm 3. It inserts the
new node and then walks upwards until it either finds a possibility to reduce
the height, or reaches the end of the long path. Nodes above did not increase
height and therefore cannot change color to the worse.

Algorithm 3 Insertion Update on a Formula $\Psi$

1:function insert(update
$\Delta\in\\{\mathsf{insert_{L}}(v,a),\mathsf{insert_{R}}(v,a),\mathsf{subdiv}(v,a)\\}$,
formula $\Psi$)

2: apply the update $\Delta$

3: $v\leftarrow\mathsf{Parent}(v)$ $\triangleright$ $v$ is now the parent of
the newly inserted $a$-node

4: while $v\neq\bot$ and no height reducing rotation was done do

5: if $\textsc{rotationPossible}(v)$ then

6: $\textsc{DoRotation}(v)$

7: $v\leftarrow w^{\prime}$ $\triangleright$ $w^{\prime}$ is the node $w$
after the rotation

8: else

9: $v\leftarrow\begin{cases}\mathsf{Parent}(v)&\text{if
$v=\mathsf{child_{D}}(\mathsf{Parent}(v))$}\\\
\bot&\text{otherwise}\end{cases}$

10: if $v\neq\bot$ then $\textsc{TryReduceHeight}(\Psi,v)$

######  Lemma 19.

Algorithm 3 performs the insertion operation correctly, maintains the strong
invariant, and runs in time $O(0pt(\Psi_{v}))$, where $v$ is the topmost node
reached in the while-loop.

######  Proof 3.14.

The correctness follows from the facts that we apply the insertion operation