arxiv: 2605.10368 · v1 · submitted 2026-05-11 · 💻 cs.FL

Recognition: 2 theorem links

· Lean Theorem

A Factorization Theorem for Forest Algebras

Shaull Almagor , Micha\"el Cadilhac , Asaf Shoham

Authors on Pith no claims yet

Pith reviewed 2026-05-12 04:25 UTC · model grok-4.3

classification 💻 cs.FL

keywords forest algebrasfactorization theoremR-alignmentmorphismsbounded-depth decompositionalgebraic automata theoryforests and trees

0 comments

The pith

Under the R-alignment condition on morphisms, every morphism into a forest algebra admits a decomposition of bounded depth; without the condition, some morphisms require unbounded depth.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper creates an analogue of Simon's factorization theorem for forests rather than words. It augments the free forest algebra and builds a recursive factorization framework to track how subforests fit together during decomposition. The central new restriction, called R-alignment, ensures that different ways of cutting a forest stay compatible at the level of the target semigroup. With this restriction in place, decompositions of bounded depth always exist; the paper also exhibits morphisms lacking the restriction for which no bounded-depth decomposition is possible. This matters for algebraic automata theory because factorization tools have long supported decision procedures for word languages and now become available for forest languages under the stated condition.

Core claim

We develop an analogue of Simon's factorization theorem for forests in the setting of forest algebras. In contrast with words, recursively factoring a forest requires keeping track of where each subforest fits. This difficulty is overcome by augmenting the free forest algebra and developing a framework that supports recursive factorization of forests along with its semantic implications. Our main result identifies a new semantic restriction on morphisms called R-alignment which ensures that different ways of cutting a forest remain compatible at the semigroup level. Under this condition, every morphism admits decompositions of bounded depth. We also prove that without this restriction, there

What carries the argument

The R-alignment condition on morphisms, which ensures semantic compatibility of different forest cuttings in the image semigroup.

If this is right

Every R-aligned morphism into a finite forest algebra admits a decomposition whose depth is bounded by a constant depending only on the algebra.
The necessity of R-alignment is witnessed by concrete morphisms that force decomposition depth to grow without bound.
Algebraic recognition of forest languages can now use bounded-depth factorizations when the recognizing morphism satisfies R-alignment.
The recursive framework supplies a uniform way to lift word-based factorization arguments to the forest setting.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

Similar alignment restrictions may be needed when extending factorization techniques to other hierarchical objects such as graphs with tree decompositions.
Decision procedures for properties of tree automata that rely on factorization could become available for the subclass of R-aligned recognizers.
The computational cost of checking R-alignment or constructing the bounded decomposition itself remains open for investigation.

Load-bearing premise

The augmentation of the free forest algebra together with the recursive factorization framework preserves semantic compatibility for all forests under R-aligned morphisms.

What would settle it

An explicit R-aligned morphism into a small finite forest algebra together with a forest whose only decompositions have depth exceeding the bound claimed by the theorem.

read the original abstract

Simon's factorization theorem is a celebrated tool in algebraic automata theory, providing bounded-depth decompositions of words with respect to morphisms into finite semigroups. We develop an analogue of Simon's theorem for \emph{forests} in the setting of forest algebras. In contrast with words, this presents a basic difficulty: recursively factoring a forest requires keeping track of where each subforest ``fits''. This difficulty ripples throughout the proof, and we overcome it by augmenting the free forest algebra and by developing a framework that supports recursive factorization of forests, along with its semantic implications. Our main result identifies a new semantic restriction on morphisms (called $\mathcal{R}$-alignment) which intuitively ensures that different ways of cutting a forest remain compatible (in a certain sense) at the semigroup level. Under this condition, we prove that every morphism admits decompositions of bounded depth. We also prove that without this restriction, there are morphisms for which no bounded-depth decomposition exists (under our notion of decomposition).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Desk Editor's Note private letter to a colleague

Extends Simon's theorem to forests with R-alignment and a counterexample, but the abstract gives no proof details to verify the augmentation step.

read the letter

The main point is that this paper gives a factorization theorem for forests under a new condition called R-alignment on morphisms into finite semigroups. Under that condition every morphism has bounded-depth decompositions, and without it there are morphisms with no such decompositions at all. They handle the extra difficulty of forests by augmenting the free forest algebra so that recursive factoring can track subforest positions, then build a framework around that augmentation and its semantic consequences. The counterexample for non-aligned morphisms is new and does not collapse to the word case in Simon's theorem. That is the actual advance here. The work is a direct attempt to carry the bounded-depth idea over to recursive structures without forcing it back into the linear word setting. The counterexample is useful because it shows the condition cannot be dropped. The abstract states the result cleanly and identifies where the proof has to diverge from the word case. On the soft spots, the abstract supplies no proof steps, no explicit construction of the augmented algebra, and no worked examples of the recursive decompositions. Without those it is impossible to check whether the augmentation really keeps the homomorphism properties and alignment of cuttings intact for arbitrarily nested forests. The stress-test concern about semantic compatibility is reasonable on the current evidence; any slip there would affect the whole recursive construction. The paper is aimed at people who already work with forest algebras or algebraic automata theory and know Simon's theorem. A reader looking for extensions to tree automata or verification might find the framework worth following up. It deserves a serious referee because the question it poses is basic and the claimed solution is non-trivial, even if the current write-up is only a sketch. I would send it to review and ask specifically for the full proof of the positive direction plus at least one concrete example of the augmentation in action.

Referee Report

2 major / 2 minor

Summary. The paper develops an analogue of Simon's factorization theorem for forests in the setting of forest algebras. It augments the free forest algebra and introduces a recursive factorization framework to handle the tracking of subforest positions. The main result is that under a new semantic restriction called R-alignment (which ensures compatibility of different cuttings of a forest at the semigroup level), every morphism admits decompositions of bounded depth. The paper also proves a converse: without R-alignment, there exist morphisms for which no bounded-depth decomposition exists under the given notion of decomposition.

Significance. If correct, this provides a useful extension of a foundational tool in algebraic automata theory from words to forests, with potential applications to tree automata and related structures. The necessity of R-alignment is established via counterexample, and the augmentation plus recursive framework represent a non-trivial technical development. The result is parameter-free in its statement and identifies a clean semantic condition.

major comments (2)

[Proof of Theorem 4.1 (augmentation construction)] The augmentation of the free forest algebra (detailed in the proof of the main theorem) must be shown to preserve homomorphism properties and semantic compatibility for nested forests under R-aligned morphisms; the recursive construction propagates any incompatibility, so an explicit lemma verifying that the new operations respect R-alignment for all subforest positions is required.
[Section 5 (necessity of R-alignment)] The counterexample morphism without bounded-depth decomposition (in the necessity direction) relies on a specific forest algebra; verify that the chosen algebra satisfies the forest algebra axioms and that the morphism is indeed not R-aligned, as any hidden compatibility would invalidate the separation from the positive result.

minor comments (2)

[Abstract] The abstract states the main result and counterexample but provides no proof outline or reference to the key lemmas; adding a one-sentence sketch of the augmentation step would improve readability.
[Preliminaries] Notation for the augmented algebra and the R-alignment predicate should be introduced with a dedicated preliminary subsection before the main theorem to avoid forward references.

Simulated Author's Rebuttal

2 responses · 0 unresolved

We thank the referee for the careful reading and constructive suggestions. We address each major comment below and describe the revisions we will make to strengthen the manuscript.

read point-by-point responses

Referee: [Proof of Theorem 4.1 (augmentation construction)] The augmentation of the free forest algebra (detailed in the proof of the main theorem) must be shown to preserve homomorphism properties and semantic compatibility for nested forests under R-aligned morphisms; the recursive construction propagates any incompatibility, so an explicit lemma verifying that the new operations respect R-alignment for all subforest positions is required.

Authors: We agree that an explicit lemma would clarify the argument. In the revised manuscript we will insert a new lemma immediately after the definition of the augmented algebra. The lemma will prove that the augmentation preserves homomorphism properties and that R-alignment is respected at every subforest position under the recursive construction, thereby ruling out propagation of incompatibilities. revision: yes
Referee: [Section 5 (necessity of R-alignment)] The counterexample morphism without bounded-depth decomposition (in the necessity direction) relies on a specific forest algebra; verify that the chosen algebra satisfies the forest algebra axioms and that the morphism is indeed not R-aligned, as any hidden compatibility would invalidate the separation from the positive result.

Authors: We will expand Section 5 with an explicit verification that the forest algebra satisfies the axioms and a direct computation showing that the morphism fails R-alignment on concrete forests. These additions will confirm the separation from the positive result. revision: yes

Circularity Check

0 steps flagged

No circularity: R-alignment and augmentation are defined independently of the bounded-depth result

full rationale

The paper introduces R-alignment as a semantic restriction on morphisms ensuring compatibility of forest cuttings at the semigroup level, then proves bounded-depth decompositions exist under this condition while exhibiting counterexamples without it. The augmentation of the free forest algebra is presented as a technical device to track subforest positions during recursive factorization, with semantic implications argued directly from the definitions rather than by reducing to fitted parameters, self-definitions, or load-bearing self-citations. No equations or steps in the provided abstract or reader's summary reduce the main theorem to its inputs by construction; the derivation chain remains self-contained against external benchmarks like Simon's theorem for words.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The result rests on standard properties of semigroups and forest algebras plus the newly introduced R-alignment condition; no free parameters or invented entities beyond the condition itself.

axioms (2)

domain assumption Forest algebras combine semigroup multiplication with horizontal and vertical composition operations on forests.
Invoked throughout the abstract as the setting for the morphisms.
ad hoc to paper R-alignment ensures compatibility of different cuttings of a forest at the semigroup level.
New semantic restriction defined in the paper to enable the bounded-depth result.

pith-pipeline@v0.9.0 · 5472 in / 1235 out tokens · 34566 ms · 2026-05-12T04:25:05.245627+00:00 · methodology

discussion (0)

Lean theorems connected to this paper

Citations machine-checked in the Pith Canon. Every link opens the source theorem in the public Lean library.

IndisputableMonolith/Foundation/AbsoluteFloorClosure.lean reality_from_one_distinction unclear

?

unclear
Relation between the paper passage and the cited Recognition theorem.

We overcome it by augmenting the free forest algebra and by developing a framework that supports recursive factorization of forests

What do these tags mean?

matches: The paper's claim is directly supported by a theorem in the formal canon.
supports: The theorem supports part of the paper's argument, but the paper may add assumptions or extra steps.
extends: The paper goes beyond the formal theorem; the theorem is a base layer rather than the whole result.
uses: The paper appears to rely on the theorem as machinery.
contradicts: The paper's claim conflicts with a theorem or certificate in the canon.
unclear: Pith found a possible connection, but the passage is too broad, indirect, or ambiguous to say the theorem truly supports the claim.

Reference graph

Works this paper leans on

61 extracted references · 61 canonical work pages

[1]

bookkeeping

doi:10.1016/0304-3975(90)90047-L. 16 Imre Simon. On semigroups of matrices over the tropical semiring. RAIRO-Theoretical Informatics and Applications, 28(3-4):277–294, 1994. 8 Technical Appendix – Organization In the following we present the details of our construction and proof. This is organized as follows. In Section 9 we define basic terminology. In S...

work page doi:10.1016/0304-3975(90)90047-l 1994
[2]

Observe that by Definition 10.1, a context C ∈ Contexts(A) has exactly one address labeled□, so this is well defined

Define sq_pos: Contexts(A)→N+ suchthatforacontext C∈Contexts(A), sq_pos(C) is the address of the unique □. Observe that by Definition 10.1, a context C ∈ Contexts(A) has exactly one address labeled□, so this is well defined. For example, in Figure 7 we havesq_pos(C1) = 00

work page
[3]

For example, in Figure 6 we have f1≡\01 f3

Forh1,h 2∈Forests(A)∪Contexts(A), we writeh1≡\x h2 whenh1 andh2 are identical apart from (possibly) their subtree rooted atx. For example, in Figure 6 we have f1≡\01 f3

work page
[4]

plucking

Forh∈Forests(A)∪Contexts(A) we denote byWidth(h) the maximal number in the domain of ForestDom(h) (i.e., the maximal “root” index in a disjoint union of trees). Notice that for a contextC and a foresth we have that the width of the forestC·h is determined by: Width(Ch) = { Width(C) sq_pos(C) /∈N Width(C) + Width(h) sq_pos(C)∈N . Intuitively, the width is ...

work page
[5]

There existh1̸=h2∈˜HA∪˜VA such thatC1(h1) =C2(h1) and C1(h2) =C2(h2)

work page
[6]

if we take a contextC with sq_pos(C) =x, and a node at addressy in some foresth, then this node moves to addressx ⊛y in C·h

sq_pos(C1) = sq_pos(C2) and there existsh∈˜HA such thatC1(h) =C2(h). Proof. The implication (1) =⇒(2) is trivial (indeed, ifC1 =C2 then C1(h) =C2(h) for everyh). (2) =⇒(3): Consider C1,C 2,h 1,h 2 such thath1̸= h2 and C1(h1) = C2(h1),C 1(h2) = C2(h2). Denotex1 = sq_pos(C1),x 2 = sq_pos(C2), we claim thatx1 =x2. Assume by way of contradiction thatx1̸=x2, w...

work page
[7]

⟨N+, ⊛, 0⟩is a monoid. S. Almagor, M. Cadilhac, A. Shoham 25

work page
[8]

collision

sq_pos:⟨˜VA,·, □⟩→⟨N+, ⊛, 0⟩is a monoid morphism. Proof. First we show that⟨N+, ⊛, 0⟩is a monoid. ⊛ is associative: we compute( x′ x·σx) ⊛ (y ⊛ ( z′ σz·z)) according to whether|y|> 1: x′⊛ ((y′·σy) ⊛z′) =x′⊛ (y′·(σy +σz)·z)) =    x·(σx +σy +σz)·z = ((x·σx) ⊛ y σy ) ⊛z′ y =σy x·(σx +σ′ y)·y′′·(σy +σz)·z = ((x·σz) ⊛ ( y    σ′ y·y′′·σy)...

work page
[9]

That is, everyx∈τ.Nodes is either a leaf, or it has exactly two children:x0 and x1

τ.Nodes is afull, binarytree domain. That is, everyx∈τ.Nodes is either a leaf, or it has exactly two children:x0 and x1. In the latter case, we refer to these children as the down and theright child, respectively

work page
[10]

For everyx∈τ.Nodes we haveτ.l(x) = (τ.forest(x),τ.ctx(x))

work page
[11]

Thus, the set of leaves is τ.type−1[L] and the set of binary nodes isτ.type−1[B]

τ.type identifies each node as aleaf (L) or abinary node(B). Thus, the set of leaves is τ.type−1[L] and the set of binary nodes isτ.type−1[B]

work page
[12]

Intuitively, this means that we pluck a nontrivial forest in each node

For everyx∈τ.Nodes and i∈{0, 1}we haveτ.forest(xi)̸=τ.forest(x). Intuitively, this means that we pluck a nontrivial forest in each node

work page
[13]

For everyx∈τ.Nodes\N∗1 (i.e., x a down-child or the root) we haveτ.ctx(x) = □

work page
[14]

decomposition

For every binary nodex∈τ.type−1[B] we haveτ.forest(x) =τ.ctx(x1)(τ.forest(x1)) and τ.forest(x0) =τ.ctx(x1)(□τ.forest(x1)). For brevity, in the remainder of the section we just write “decomposition” when referring to a binary decomposition. Also, since decompositions are in particular labeled tree domains, all the relevant definitions of Section 10.1 apply...

work page
[15]

AncEmb(τ,y1,y )(0) = sq_pos(τ.ctx(y1))

work page
[16]

If y@u→x1 then x<y and AncEmb(τ,y,x)(u) = sq_pos(τ.ctx(x1))

work page
[17]

For two nodesx < ysuch thaty̸= x1, if AncEmb(τ,y,x)(u) = sq_pos(τ.ctx(x1)) for some u∈τ.forest(y), theny@u→x1. Proof. Let τbe a decomposition

work page
[18]

By Definitions 11.5 and 12.10 we have that AncEmb(τ,y1,y )(0) = sq_pos(τ.ctx(y1)) ⊛ 0 = sq_pos(τ.ctx(y1))

Consider some binary nodey (so thaty1∈τ.Nodes). By Definitions 11.5 and 12.10 we have that AncEmb(τ,y1,y )(0) = sq_pos(τ.ctx(y1)) ⊛ 0 = sq_pos(τ.ctx(y1))

work page
[19]

Thebasecaseis y =x0

We prove this part by induction on the structure of the references, as per Definition 12.6. Thebasecaseis y =x0. Inthiscaseweindeedwehave x<y andbyDefinition12.6wealso haveu = sq_pos(τ.ctx(x1)). Therefore, by Definition 12.10 we getAncEmb(τ,x0,x )(u) = u = sq_pos(τ.ctx(x1)). For the induction step, assumey@u→x1 and thaty =zσfor somez. In particular, by De...

work page
[20]

stability

We prove the claim by induction ony. 34 A Factorization Theorem for Forest Algebras If y = x0, then by Definition 12.6 we havey@u→x1 for u = sq_pos(τ.ctx(x1)). Note that by Definition 12.10 we haveAncEmb(τ,y,x)(u) = u (since u = uz in the definition by cases). Thus, we haveu = sq_pos(τ.ctx(x1)), as needed. If y =xzσand AncEmb(τ,y,x)(u) = sq_pos(τ.ctx(x1))...

work page
[21]

rotating

By Proposition 11.6 we haves2 = (σ2·0) ⊛s′ 2. Now, sinceσ2≤M01 and σv > 0 we have (σ2·0) ⊛s′ 2̸≤LCRS ((M01 +σv)·0) ⊛v′ Indeed, otherwise by Proposition 11.10 we would have that((M01 +σv)·0) ⊛v′= (σ2·0) ⊛s′ 2 ⊛v′′for somev′′, but this is a contradiction since the right-hand side starts withσ2 <M 01 +σv. Then, by Definition 12.10 we again have AncEmb(τ,00,ϵ...

work page
[22]

Then τ′is a decomposition which for the mappingπ=   1↦→01 01↦→1 00↦→00  satisfies AncEmb(τ,y,ϵ) = AncEmb(τ′,π(y),ϵ) for every y∈{1, 01, 00}

and τ′.ctx(01) = Clink(τ,00, 1) (denoted C′ 1). Then τ′is a decomposition which for the mappingπ=   1↦→01 01↦→1 00↦→00  satisfies AncEmb(τ,y,ϵ) = AncEmb(τ′,π(y),ϵ) for every y∈{1, 01, 00}. Proof. Notice that τ′is a valid binary decomposition, with τ′.forest(1) = h01 and τ′.forest(01) =h1, and sinceτis stable (over˜V) we haveC′ 1 =τ′.ctx(01) =Clink(τ,0...

work page
[23]

allowed” set of next factors (or contexts), namely “minimality

we get AncEmb(τ2,y,x 00)(u) = u01 = AncEmb(τ1,y,x 00)(u). Recallthat τ.x00@u01→x01, andtherefore AncEmb(τ1,x 00,x 0)(u01) = sq_pos(C01) =u01. We conclude (by Definition 12.10) that τ1.y@u →x01, yielding Clink(τ2,y,x 1) = Clink(τ1,y,x 01)∈˜V. If z =x01: similarly to the previous case, we obtainClink(τ2,y,x 01) =Clink(τ1,y,x 1)∈ ˜V. We therefore conclude th...

work page
[24]

For everyC∈NxtCtx(τ,˜V,B,x 0) there existsC′∈NxtCtx(τ,˜V,B,x ) such thatC′≈C (i.e., they areunravel equivalentas per Definition 11.13). S. Almagor, M. Cadilhac, A. Shoham 49

work page
[25]

For everyC∈NxtCtx(τ,˜V,B,x 1) we haveτ.ctx(x1)·C∈NxtCtx(τ,˜V,B,x ) Proof. 1. Let C∈NxtCtx(τ,˜V,B,x 0). By Definition 14.2 there exists a partial decomposi- tion τ′∈PartialDec(˜V,B ) with τ≡\x0 τ′such thatτ′.ctx(x01) =C (and in particular τ≡\x τ′). There are now two possibilities: either the decomposition is BT or LR. More precisely, eitherτ′.x01@u→x1 (BT)...

work page
[26]

Let C ∈NxtCtx(τ,˜V,B,x 1)

Assume NxtCtx(τ,˜V,B,x 1) ̸= ∅. Let C ∈NxtCtx(τ,˜V,B,x 1). By Definition 14.2 there exists a partial decompositionτ′∈PartialDec(˜V,B ) with τ≡\x1 τ′such that τ′.ctx(x11) =C. We now have only one possible setting, namely TB. By Lemma 13.3 there is a partial decomposition τ′′such that τ′′≡\x τ′≡\x τand τ′′.ctx(x1) = τ′.ctx(x1)·C =τ.ctx(x1)·C. In particular,...

work page
[27]

φ[NxtCtx(τ,˜V,B,x 0)]⊆φ[NxtCtx(τ,˜V,B,x )]

work page
[28]

decompose away

φ(τ.ctx(x1))·φ[NxtCtx(τ,˜V,B,x 1)]⊆φ[NxtCtx(τ,˜V,B,x )] A particularly useful application of Corollary 14.8 is whenV has a zero, as follows. ▶ Corollary 14.9. Consider a semigroupV with a zero0∈V, a stable context set˜V and a morphism φ: ˜V →V, Then for everyx≤y∈τ.Nodes we have 0∈φ[NxtCtx(τ,˜V,B,y )] =⇒0∈φ[NxtCtx(τ,˜V,B,x )] Intuitively, we use this in Se...

work page
[29]

If τ.type(x) = L then x is a Leaf

work page
[30]

If τ.type(x) = B, thenx is a Binary nodesatisfying the conditions of Definition 12.2. S. Almagor, M. Cadilhac, A. Shoham 53

work page
[31]

Its set of children is unbounded (but finite), denotedS =τ.Nodes∩(x·N), and there is a binary decompositionτ′such that the following hold

If τ.type(x) = I then x is an Idempotent node. Its set of children is unbounded (but finite), denotedS =τ.Nodes∩(x·N), and there is a binary decompositionτ′such that the following hold. τ′.forest(ϵ) =τ.forest(x). There exists an idempotent elementv∈V (i.e., v2 =v) such that for the stable context set7 ˜Vx =φ−1[v]∪{□}and the basisτ.forest[S] (i.e., the set...

work page
[32]

Its set of children is unbounded (but finite), denotedS =τ.Nodes∩(x·N), and there is a binary decompositionτ′such that the following hold: τ′.forest(ϵ) =τ.forest(x)

If τ.type(x) = C then x is an Centipede node. Its set of children is unbounded (but finite), denotedS =τ.Nodes∩(x·N), and there is a binary decompositionτ′such that the following hold: τ′.forest(ϵ) =τ.forest(x). τ′.Nodes⊆0∗(ϵ+ 1) (see Figure 19). τ′does not have inherited references (as per Definition 12.6). There is a bijectiong : S→τ′.type−1[L] such tha...

work page
[33]

τ[x]∈Dec(˜V,B,τ.forest(x),φ)

work page
[34]

elementary

For a decompositionτ′∈Dec(˜V,B,τ.forest(x),φ) we haveτ[x↦→τ′]∈Dec(˜V,B,f,φ ). In contrast to Corollary 15.5, if we considerstability (Definition 12.14) as a property, then it is not local, and the corollary does not hold for it (specifically, the second item fails). As mentioned above, the parameterization of the decomposition by a basis is to facilitate ...

work page
[35]

ifS1uS1 =S1uvS 1 then uS1 =uvS 1)

uJuv =⇒uRuv (i.e. ifS1uS1 =S1uvS 1 then uS1 =uvS 1)

work page
[36]

ifS1uS1 =S1vuS 1 then S1u =S1vu)

vJuv =⇒uvLv (i.e. ifS1uS1 =S1vuS 1 then S1u =S1vu). Proof. We prove the first implication, the second is analogous. AssumeS1uS1 =S1uvS 1, then there existx,y∈S1 such thatx(uv)y =u. By Lemma 9.1 there exists an idempotent 58 A Factorization Theorem for Forest Algebras powern∈N such that(vy)n = (vy)2n. We now replaceu in the expressionx(uv)y byx(uv)y, and r...

work page
[37]

If st = 0 then s′t′= 0 for everys′,t′such thats′Ls and t′Rt

work page
[38]

If st̸= 0 then sRst and stLt. Proof. 1. By Definition 16.1 there arels,rt∈S such thats′=ls·s andt′=t·rt. Therefore, s′t′= (lss)(trt) =ls0rt = 0 9 Despite the same terminology, this notion is different from simplegroups. 10Note that the non-null requirement merely excludes the degenerate case of the semigroup{0,a}with a2 = 0. S. Almagor, M. Cadilhac, A. Shoham 59

work page
[39]

as much as possible

Since st̸= 0, then by simplicity we havesJstJt. By Lemma 16.2 we obtainsRst and stLt. ◀ Intuitively, Lemma 16.5 states that ifst = 0, then [st]H = 0. Otherwise, we have [st]H ={v|stRv∧stLv}={v|sRv∧tLv}= [s]R∩[t]L 16.2 Congruences and Ideals A congruence on S is anequivalence relation∼=⊆S×S that preserves the semigroup action. That is, ifu1∼= u2 and v1∼= v...

work page
[40]

φ[NxtTwoCtx(τ,˜V,B,x 0)]⊆φ[NxtTwoCtx(τ,˜V,B,x )]

work page
[41]

We prove each part of the lemma separately

If (u,v )∈φ[NxtTwoCtx(τ,˜V,B,x 1)] then (φ(τ.ctx(x1))·u,v )∈φ[NxtTwoCtx(τ,˜V,B,x )] Proof. We prove each part of the lemma separately. Item1. Let (C1,C 2)∈NxtTwoCtx(τ,x0), weshowthat (φ(C1),φ(C2))∈φ(NxtTwoCtx(τ,x)). We assume without loss of generality thatτattains these contexts, i.e.,τ.ctx(x01) =C1 and τ.ctx(x011) =C2 (otherwise replaceτwith an extensio...

work page
[42]

τ.ctx(x01)≈τ′.ctx(x1), and in particularφ(C1) =φ(τ′.ctx(x1))

work page
[43]

If τ.x01@∗ →x1, then we are under the reference structure of BT to TB rotation

τ′[x1] = τ[x01], and in particularC2∈NxtCtx(τ′[x01]) (since τ′[x1] is decomposed identically toτ[x01], i.e., withC2): τ′.ctx(x11) =τ′[x1].ctx(1) =τ[x01].ctx(1) =τ.ctx(x011) =C2 We readily obtain(φ(C1),φ(C2))∈NxtTwoCtx(τ′,x ), and sinceτ′≡\x τit follows that (φ(C1),φ(C2))∈NxtTwoCtx(τ,x), as required. If τ.x01@∗ →x1, then we are under the reference structur...

work page
[44]

τ′.ctx(x1) =τ.ctx(x01) =C1 6

work page
[45]

Wethereforehavethat C2 =τ.ctx(x011)∈NxtCtx(τ′,x 10), soφ(C2)∈φ[NxtCtx(τ′,x 10)]

τ′[x10] =τ[x01]. Wethereforehavethat C2 =τ.ctx(x011)∈NxtCtx(τ′,x 10), soφ(C2)∈φ[NxtCtx(τ′,x 10)]. Recall that by Corollary 14.8 thatφ[NxtCtx(τ′,x 10)]⊆φ[NxtCtx(τ,x)], so φ(C2)∈ φ[NxtCtx(τ′,x 10)]. Combining this with the second property above gives the desired (φ(C1),φ(C2))∈φ[NxtTwoCtx(τ,˜V,B,x )]. Item2. Let (C1,C 2)∈NxtTwoCtx(τ,x1), weshowthat (φ(τ.ctx(...

work page
[46]

τ′.ctx(x1) =τ.ctx(x1)·τ.ctx(x11) =τ.ctx(x1)·C1

work page
[47]

decreasing

τ′[x1] =τ[x11]. By Property 3, we have thatτ′.ctx(x11) =τ.ctx(x111) =C2. We therefore have(τ.ctx(x1)· C1,C 2) ∈NxtTwoCtx(τ′,x ), and we have the desired (φ(τ.ctx(x1))·φ(C1),φ(C2)) ∈ φ[NxtTwoCtx(τ,x)] (again, sinceτ≡\x τ′). ◀ Recall that our main interest in two consecutive plucked subforests is when these form a specific pair ofR- andL-classes under the m...

work page
[48]

LR(x0)⊆LR(x): follows directly from Lemma 17.8

work page
[49]

By Lemma 17.8 we have (φ(τ.ctx(x1))·u,v ) ∈φ[NxtTwoCtx(τ.˜V,B,x )]

LR(x1) ⊆LR(x): Let (u,v ) ∈φ[NxtTwoCtx(τ,˜V,B,x 1)]. By Lemma 17.8 we have (φ(τ.ctx(x1))·u,v ) ∈φ[NxtTwoCtx(τ.˜V,B,x )]. Due to the assumption that 0 /∈ φ[NxtCtx(τ,˜V,B,x )] we know thatφ(τ.ctx(x1))·u̸= 0. Now, by Lemma 16.5, we have thatφ(τ.ctx(x1))·uLu, and we have that([u]L, [v]R)∈LR(x) as required. ◀ S. Almagor, M. Cadilhac, A. Shoham 67 Before procee...

work page
[50]

u1̸= 0, u2̸= 0, andu1u2̸= 0

work page
[51]

([u1]L∩[u2]R)·([u1]L∩[u2]R) = ([u1]L∩[u2]R) (note the difference inL andR and u1,u 2 from Item 2). Proof. 1. By the assumption that0 /∈φ[NxtCtx(τ,ϵ)] and Corollary 14.9 we immediately get u1̸= 0 and u2̸= 0. By Corollary 14.8 we haveu1·u2∈φ[NxtCtx(τ,x)], thus also u1·u2̸= 0

work page
[52]

By Lemma 16.5 we now haveu1u2Ru1 and u1u2Lu2, sou1u2∈[u1]R∩[u2]L

work page
[53]

Identically to Item 2 above, this implies (by Lemma 16.5) thatab∈[b]L∩[a]R, but [a]R = [u2]R and [b]L = [u1]L, soab∈[u1]L∩[u2]R

Let somea,b∈[u1]L∩[u2]R then by Lemma 16.5 and becauseu1u2̸= 0 we haveab̸= 0. Identically to Item 2 above, this implies (by Lemma 16.5) thatab∈[b]L∩[a]R, but [a]R = [u2]R and [b]L = [u1]L, soab∈[u1]L∩[u2]R. We therefore have that[u1]L∩[u2]R is anH-class that is closed under multiplication. In particular, we have the inclusion ([u1]L∩[u2]R)·([u1]L∩[u2]R)⊆(...

work page
[54]

climb up

Moreover, by Corollary 14.9 and the maximality ofτ0, we have that0 /∈NxtCtx(τ0,y ) for every leaf y∈τ0.type−1[L]. We now show that each leafy can be extended to a full decomposition of depth 1 using a single C-node. Consider a leafy. By Lemma 14.6 there isτ0,y∈FullDec(˜V,B ) that is minimal belowy and τ0,y≡\y τ0. Let τ1,y =τ0,y[y] by the subtree ofτ0,y ro...

work page
[55]

canonical

This shows that any decomposition has depth at leastlogd, which is unbounded. We start by describing the forest language we use. The language can be simply described as a set of labeled trees, but unfortunately we must also formalize it as a morphism to a forest algebra, which is significantly more complicated. We work over the alphabetA ={a,b,ℓa,ℓb,ℓ}and...

work page
[56]

In particular, factoring byC does not pluck out any subforest off belowu

such that for everyf,f 1,f 0∈˜HA with f∈φ−1[aℓT,bℓT,ℓ2] and C∈φ−1[e] such that f =C(f1) and f0 =C(□f1) we have thatf0[u] =f[u] (i.e., f and f0 have identical subtrees at addressu). In particular, factoring byC does not pluck out any subforest off belowu. Proof. We prove the claim by separating to cases according toe∈E′(V )\{id}. e =aℓT+fb: notice first th...

work page
[57]

V(f0) + V(f1,ϵ)≥V(f). Proof. Consider u∈Domain(f) such that V(f) = V(f,u ) (i.e., u witnesses the location of the maximal completely binary subtree), and denote C′= f[u ↦→□]. Let f′= ForestDom−1(ForestDom(f)[u]) be the subforest of f below u, so that f = C′(f′). By the choice ofu, we haveV(f′,ϵ) = V(f). Now split to cases according to the order ofC and C′...

work page
[58]

If C and C′are incomparable, thenf′is a subtree off0, so V(f0) = V(f)

work page
[59]

If C⪯pre C′, thenf′is a subtree off1, hence V(f1) = V(f)

work page
[60]

centipede

If C′⪯pre C, then by the definition ofC′and the fact thatf′is a tree (rather than a proper forest), we have thatsq_pos(C) = u·v (for v̸= ϵ). Notice that V(f0,u ) = min{V(f),|v|+ 1}and that V(f1,ϵ)≥V(f)−|v|(since at least the subtree starting from u·v is a complete binary tree inf1). Overall we get thatV(f0) + V(f1,ϵ)≥V(f) ◀ 82 A Factorization Theorem for ...

work page
[61]

pick a side

Notice that unlikey (which is a leaf, and therefore corresponds to a child ofτ[x]), the node 0i1 in τ′does not directly correspond to a child ofτ[x]. We focus on the case thatV(τ′.forest(y))< 1 2 V(τ.forest(x)) and show thatτ′has some leaf z (in fact, the down-most leaf below0i1) such thatV(τ′.forest(z))≥1 2 V(τ.forest(x)). Intuitively, this follows from ...

work page