Damien Pous
email: damien.pous@ens-lyon.fr

Jurriaan Rot
email: jurriaan.rot@ru.nl

Jana Wagemaker
email: jana.wagemaker@ru.nl

On Tools for Completeness of Kleene Algebra with Hypotheses

Keywords: Kleene algebra, Completeness, Reduction

In the literature on Kleene algebra, a number of variants have been proposed which impose additional structure specified by a theory, such as Kleene algebra with tests (KAT) and the recent Kleene algebra with observations (KAO), or make specific assumptions about certain constants, as for instance in NetKAT. Many of these variants fit within the unifying perspective offered by Kleene algebra with hypotheses, which comes with a canonical language model constructed from a given set of hypotheses. For the case of KAT, this model corresponds to the familiar interpretation of expressions as languages of guarded strings. A relevant question therefore is whether Kleene algebra together with a given set of hypotheses is complete with respect to its canonical language model. In this paper, we revisit, combine and extend existing results on this question to obtain tools for proving completeness in a modular way. We showcase these tools by reproving completeness of KAT and KAO, and prove completeness of a new variant of KAT where the collection of tests only forms a distributive lattice.

Introduction

Kleene algebras (KA) [START_REF] Kleene | Representation of events in nerve nets and finite automata[END_REF][START_REF] Conway | Regular Algebra and Finite Machines[END_REF] are algebraic structures involving an iteration operation, Kleene star, corresponding to reflexive-transitive closure in relational models and to language iteration in language models. Its axioms are complete w.r.t. relational models and language models [START_REF] Kozen | A completeness theorem for Kleene Algebras and the algebra of regular events[END_REF][START_REF] Krob | Complete systems of B-rational identities[END_REF][START_REF] Boffa | Une remarque sur les systèmes complets d'identités rationnelles[END_REF], and the resulting equational theory is decidable via automata algorithms (in fact, PSpace-complete [START_REF] Meyer | The equivalence problem for regular expressions with squaring requires exponential space[END_REF]).

These structures were later extended in order to deal with common programming constructs. For instance, Kleene algebras with tests (KAT) [START_REF] Kozen | Kleene algebra with tests[END_REF], which combine Kleene algebra and Boolean algebra, make it possible to represent the control flow of while programs. Kleene star is used for while loops, and Boolean tests are used for the conditions of such loops, as well as the conditions in ifthen-else statements. Again, the axioms of KAT are complete w.r.t. appropriate classes of models, and its equational theory remains in PSpace. Proving so is non-trivial: Kozen's proof reduces completeness of KAT to completeness of KA, via a direct syntactic transformation on terms.

Another extension is Concurrent Kleene algebra (CKA) [START_REF] Hoare | Concurrent Kleene algebra and its foundations[END_REF], where a binary operator for parallelism is added. The resulting theory is characterised by languages of pomsets rather than languages of words, and is ExpSpace-complete [START_REF] Brunet | On decidability of Concurrent Kleene Algebra[END_REF]. Trying to have both tests and concurrency turned out to be non-trivial, and called for yet another notion: Kleene algebras with observations (KAO) [START_REF] Kappé | Kleene algebra with observations[END_REF], which are again complete w.r.t. appropriate models, and decidable.

When used in the context of program verification, e.g., in a proof assistant, such structures make it possible to write algebraic proofs of correctness, and to mechanise some of the steps: when two expressions e and f representing two programs happen to be provably equivalent in KA, KAT, or KAO, one does not need to provide a proof, one can simply call a certified decision procedure [START_REF] Braibant | An efficient Coq tactic for deciding Kleene algebras[END_REF][START_REF] Krauss | Proof pearl: Regular expression equivalence and relation algebra[END_REF][START_REF] Pous | Kleene Algebra with Tests and Coq tools for while programs[END_REF]. However, this is often not enough [START_REF] Kozen | Certification of compiler optimizations using Kleene algebra with tests[END_REF][START_REF] Angus | Kleene algebra with tests and program schematology[END_REF][START_REF] Hardin | On the elimination of hypotheses in Kleene algebra with tests[END_REF]: most of the time, the expressions e and f are provably equal only under certain assumptions on their constituants. For instance, to prove that (a + b) * and a * b * are equal, one may have to use that in the considered instance, we have ba = ab. In other words, one would like to prove equations under some assumptions, to have algorithms for the Horn theory of Kleene algebra and its extensions rather than just their equational theories.

Unfortunately, those Horn theories are typically undecidable [START_REF] Kozen | Kleene algebra with tests and commutativity conditions[END_REF][START_REF] Kozen | On the complexity of reasoning in Kleene algebra[END_REF], even with rather restricted forms of hypotheses (e.g., commutation of two letters, as in the above example). Nevertheless, important and useful classes of hypotheses can be 'eliminated', by reducing to the plain and decidable case of the equational theory. This is for instance the case of Hoare hypotheses [START_REF] Kozen | On Hoare logic and Kleene algebra with tests[END_REF], of the shape e = 0, which make it possible to encode Hoare triples for partial correctness in KAT.

In some cases, one wants to exploit hypotheses about specific constituants (e.g, a and b in the above example). In other situations, one wants to exploit assumptions on the whole structure. For instance, in commutative Kleene algebra [START_REF] Redko | On the algebra of commutative events[END_REF][START_REF] Conway | Regular Algebra and Finite Machines[END_REF][START_REF] Brunet | A note on commutative Kleene algebra[END_REF], one assumes that the product is commutative everywhere.

Many of these extensions of Kleene algebra (KAT, KAO, commutative KA, specific hypotheses) fit into the generic framework of Kleene algebra with hypotheses [START_REF] Doumane | Kleene algebra with hypotheses[END_REF], providing in each case a canonical model in terms of closed languages.

We show that we recover standard models in this way, and we provide tools to establish completeness and decidability of such extensions, in a modular way. The key notion is that of reduction from one set of hypotheses to another. We summarise existing reductions and we provide a toolbox for combining those reductions together. We use this toolbox in order to obtain new and modular proofs of completeness for KAT and KAO, as well as for the fragment of KAT where tests are only assumed to form a distributive lattice.

Note however that there are Kleene algebra extensions like action algebras [START_REF] Pratt | Action logic and pure induction[END_REF] or action lattices [START_REF] Kozen | On action algebras[END_REF], which do not seem to fit into the framework of Kleene algebra with hypotheses: it is not clear how to interpret the additional operations as letters with additional structure.

Kleene algebra, hypotheses, closures

A Kleene algebra [START_REF] Conway | Regular Algebra and Finite Machines[END_REF][START_REF] Kozen | A completeness theorem for Kleene algebras and the algebra of regular events[END_REF] is a tuple (K, +, •, * , 0, 1) such that (K, +, •, 0, 1) is an idempotent semiring, and * is a unary operator on K such that for all x, y ∈ K the following axioms are satisfied:

1 + x • x * ≤ x * x + y • z ≤ z ⇒ y * • x ≤ z x + y • z ≤ y ⇒ x • z * ≤ y
There, as later in the paper, we write x ≤ y as a shorthand for x + y = y. Given the idempotent semiring axioms, ≤ is a partial order in every Kleene algebra, and all operations are monotone w.r.t. that order.

We let e, f range over regular expressions over an alphabet Σ, defined by: e, f ::

= e + f | e • f | e * | 0 | 1 | a ∈ Σ
We write T(Σ) for the set of such expressions, or simply T when the alphabet is clear from the context. Given alphabets Σ and Γ , a function h : Σ → T(Γ ) extends uniquely into a homomorphism h : T(Σ) → T(Γ ), which we refer to as the homomorphism generated by h. As usual, every regular expression e gives rise to a language e ∈ P(Σ * ). Given two regular expressions, we moreover write KA e = f when e = f is derivable from the axioms of Kleene algebra. (Equivalently, when the equation e = f holds universally, in all Kleene algebras.)

The central theorem of Kleene algebra is the following:

Theorem 2.1 (Soundness and Completeness of KA [START_REF] Kozen | A completeness theorem for Kleene Algebras and the algebra of regular events[END_REF][START_REF] Krob | Complete systems of B-rational identities[END_REF][START_REF] Boffa | Une remarque sur les systèmes complets d'identités rationnelles[END_REF]). For all e, f ∈ T, we have KA e = f if and only if e = f .

As a consequence, the equational theory of Kleene algebras is decidable.

Our goal is to extend this result to the case where we have additional hypotheses on some of the letters of the alphabet, or axioms restricting the behaviour of certain operations. Those are represented by sets of inequations, i.e., pairs (e, f ) of regular expressions written e ≤ f for the sake of clarity. Given a set H of such inequations, we write KA H e ≤ f when the inequation e ≤ f is derivable from the axioms of Kleene algebra and the hypotheses in H (similarly for equations). By extension, we write KA H H when KA H e ≤ f for all e ≤ f in H .

Note that we consider letters of the alphabet as constants rather than variables. In particular, while we have KA ba≤ab (a+b) * ≤ a * b * , we do not have KA ba≤ab (a + c) * ≤ a * c * . Formally, we use a notion of derivation where there is no substitution rule, and where we have all instances of Kleene algebra axioms as axioms. When we want to consider hypotheses that are universally valid, it suffices to use all their instances. For example, to define commutative Kleene algebra, we simply use the infinite set {ef ≤ f e | e, f ∈ T}.

We associate a canonical language model to KA with a set of hypotheses H, defined by closure under H. For u, v ∈ Σ * and L ⊆ Σ * , let uLv {uxv | x ∈ L}. Definition 2.2 (H-closure). Let H be a set of hypotheses and L ⊆ Σ * a language. The H-closure of L, denoted as cl H (L), is the smallest language containing L s.t. for all e ≤ f ∈ H and u, v

∈ Σ * , if u f v ⊆ cl H (L), then u e v ⊆ cl H (L).
Fixpoint theory makes it possible to characterise the H-closure of a language L as the least (pre)fixpoint of the function st

H,L (X) = st H (X) ∪ L, where st H (X) = {u e v | e ≤ f ∈ H, u, v ∈ Σ * , u f v ⊆ X} .
This least fixpoint can be characterised more explicitly by transfinite iteration: we have cl H (L) = α st α H (L) where st α+1 H (L) = st H (st α H (L)) for every ordinal α, and st λ H (L) = α<λ st α H (L) for every limit ordinal λ. This notion of closure gives a closed interpretation of regular expressions, cl H ( -), for which KA H is sound:

Theorem 2.3 ([10, Theorem 2]). If KA H e = f , then cl H ( e ) = cl H ( f ).
In the sequel, we shall prove the converse implication, completeness, for specific choices of H: we say that KA H is complete if for all expressions e, f :

cl H ( e ) = cl H ( f ) implies KA H e = f .
We could hope that completeness always holds, notably because the notion of closure is invariant under inter-derivability of the considered hypotheses, as a consequence of the following lemma: Unfortunately, there are concrete instances for which KA H is known not to be complete. For instance, there is a finitely presented monoid (thus a finite set H 0 of equations) such that {(e, f ) | cl H0 ( e ) = cl H0 ( f )} is not r.e. [START_REF] Kozen | Kleene algebra with equations[END_REF]Theorem 1]. Since derivability in KA H is r.e. as soon as H is, KA H0 cannot be complete.

Before turning to techniques for proving completeness, let us describe the closed interpretation of regular expressions for two specific choices of hypotheses.

Let us consider first commutative Kleene algebra, obtained as explained in the Introduction using the set {ef ≤ f e | e, f ∈ T(Σ)}. Under Kleene algebra axioms, this set is equiderivable with its restriction to letters,

C = {ab ≤ ba | a, b ∈ Σ} (a consequence of [1, Lemma 4.4]).
The associated closure can be characterised as follows:

cl C (L) = {w ∈ Σ * | ∃v ∈ L. |w| x = |v| x for all x ∈ Σ}
where |w| x denotes the number of occurences of x in w. Thus, w ∈ cl C (L) if it is a permutation of some word in L. This semantics matches precisely the one used in [START_REF] Conway | Regular Algebra and Finite Machines[END_REF] for commutative Kleene algebra: there, a functionc : T(Σ) → P(N Σ ) interprets regular expressions as subsets of N Σ , whose elements are thought of as "commutative words": these assign to each letter the number of occurences, but there is no order of letters. Let q : P(Σ * ) → P(N Σ ), q(L) = {λx.|w| x | w ∈ L}; this map computes the Parikh image of a given language L, that is, the set of multisets representing occurences of letters in words in L. Then this semantics is characterised byc = q • -.

One may observe thatc = q(cl C ( -)), since cl C only adds words to a language which have the same number of occurences of each letter as some word which is already there. Conversely, we have cl C ( -) = q (c ), where

q : P(N Σ ) → P(Σ * ), q (L) = {w | p ∈ L, ∀x ∈ Σ, |w| x = p(x)}. As a conse- quence, we have e c = f c if and only if cl C ( e ) = cl C ( f ).
From there, we can easily deduce from the completeness result in [8, Chapter 11, Theorem 4], attributed to Pilling (see also [START_REF] Brunet | A note on commutative Kleene algebra[END_REF]), that KA C is complete.

Let us now consider a single hypothesis: D = {ab ≤ 0} for some letters a and b. The D-closure of a language L consists of those words that either belong to L, or contain ab as a subword. As a consequence, we have cl D ( e ) = cl D ( f ) if and only if e and f agree on all words not containing the pattern ab.

In this example, we can easily obtain decidability and completeness of KA D . Indeed, consider the function r : T(Σ) → T(Σ), r(e) = e + Σ * abΣ * . For all e, we have KA D e = r(e), and cl D ( e ) = r(e) . As a consequence, we have

cl D ( e ) = cl D ( f ) ⇔ r(e) = r(f ) ⇔ KA r(e) = r(f ) (Theorem 2.1) ⇒ KA D e = f
The first step above establishes decidability of the closed semantics; the following ones reduce the problem of completeness for KA D to that for KA alone, which is known to hold. By soundness (Theorem 2.3), the last line implies the first one, so that these conditions are all equivalent. This second example exploits and illustrate a simple instance of the framework we design in the sequel to prove completeness of various sets of hypotheses.

Reductions

As illustrated above, the overall strategy is to reduce completeness of KA H , for a given set of hypotheses H, to completeness of Kleene algebra. The core idea is to provide a map r from expressions to expressions, which incorporates the hypotheses H in the sense that r(e) = cl H ( e ), and such that r(e) is provably equivalent to e under the hypotheses H. This idea leads to the unifying notion of reduction, developed in [START_REF] Kozen | Kleene algebra with equations[END_REF][START_REF] Doumane | Kleene algebra with hypotheses[END_REF][START_REF] Kappé | Concurrent Kleene algebra with observations: From hypotheses to completeness[END_REF]. Definition 3.1 (Reduction). Assume Γ ⊆ Σ and let H, H be sets of hypotheses over Σ and Γ respectively. We say that H reduces to H if KA H H and there exists a map r : T(Σ) → T(Γ ) such that for all e ∈ T(Σ), We often refer to such a witnessing map r itself as a reduction. Generalising the above example, we obtain the key property of reductions: Theorem 3.2. Suppose H reduces to H . If KA H is complete, then so is KA H .

Proof. Let r be the map for the reduction from H to H . For all e, f ∈ T(Σ), While we focus on completeness in this paper, note that reductions can also be used to prove decidability. More precisely, if KA H is complete and decidable, and H reduces to H via a computable reduction r, then KA H is decidable.

cl H ( e ) = cl H ( f ) ⇒ cl H ( r(e) ) = cl H ( r(f ) ) (r a reduction (item 2)) ⇒ KA H r(e) = r(f ) (completeness of H ) ⇒ KA H r(e) = r(f ) (KA H H ) ⇒ KA H e = f (
The following result from [START_REF] Kappé | Concurrent Kleene algebra with observations: From hypotheses to completeness[END_REF] (cf. Remark 3.5) gives a sufficient condition for the existence of a reduction. This is useful for reductions where the underlying map r is a homomorphism. Lemma 3.3. Assume Γ ⊆ Σ and let H, H be sets of hypotheses over Σ and Γ respectively, such that KA H H . If there exists a homomorphism r : T(Σ) → T(Γ ) such that:

1. For all a ∈ Γ , we have KA a ≤ r(a). 2. For all a ∈ Σ, we have KA H a = r(a). 3. For all e ≤ f ∈ H, we have KA H r(e) ≤ r(f ).

then H reduces to H .

Example 3.4. We consider KA together with a global "top element" and the axiom e ≤ . To make this precise in Kleene algebra with hypotheses, we assume an alphabet Σ with ∈ Σ, and take the set of hypotheses H = {e ≤ | e ∈ T(Σ)}. Then cl H (L) contains those words obtained from a word w ∈ L by replacing every occurence of in w by arbitrary words in Σ * .

We claim that H reduces to ∅. To this end, define the homomorphism r : T(Σ) → T(Σ) by r( ) = Σ * (where we view Σ as an expression consisting of the sum of its elements) and r(a) = a for a ∈ Σ with a = . Each of the conditions of Lemma 3.3 is now easy to check. Thus r is a reduction, so by Theorem 3.2, KA H is complete.

Note that this implies completeness w.r.t. validity of equations in all (regular) language models, where is interpreted as the largest language: indeed, the closed semantics cl H ( -) is generated by such a model. At the end of Section 2, we discussed commutative KA as an instance of Kleene algebra with hypotheses H. While KA H is complete in that case, there is no reduction from H to ∅, as cl H does not preserve regularity. Indeed, cl H ( (ab) * ) = {w | |w| a = |w| b } which is not regular. The completeness proof in [START_REF] Conway | Regular Algebra and Finite Machines[END_REF][START_REF] Brunet | A note on commutative Kleene algebra[END_REF] is selfcontained, and does not rely on completeness of KA.

Remark 3.5. The idea to use two sets of hypotheses in Definition 3.1 is from [START_REF] Kappé | Concurrent Kleene algebra with observations: From hypotheses to completeness[END_REF], where reductions are defined slightly differently: the alphabet is fixed (that is, Σ = Γ ), and the last condition is instead defined as cl

H ( e ) = cl H ( f ) ⇒ cl H ( r(e) ) = cl H ( r(f )
). An extra notion of strong reduction is then introduced, which coincides with our definition if Σ = Γ . By allowing a change of alphabet, we do not need to distinguish reductions and strong reductions. Lemma 3.3 is in [START_REF] Kappé | Concurrent Kleene algebra with observations: From hypotheses to completeness[END_REF]Lemma 4.23], adapted here to the case with two alphabets (this is taken care of in loc. cit. by assuming cl H preserves languages over Γ ).

Basic reductions

The following result collects several sets of hypotheses for which we have reductions to ∅. These mostly come from the literature. They form basic building blocks used in the more complex reductions that we present in the examples below. Lemma 3.6. Each of the following sets of hypotheses reduce to the empty set (of hypotheses over Σ). (iii) This is basically due to [START_REF] Cohen | Hypotheses in Kleene algebra[END_REF], but since it is phrased differently there we include a proof in Appendix B. (iv) Hypotheses of a similar form as (iv) are studied in the setting of Kleene algebra with tests in [START_REF] Hardin | On the elimination of hypotheses in Kleene algebra with tests[END_REF], we include a proof in Appendix B.

(i) {u i ≤ w i | i ∈ I} with u i , w i ∈ Σ * and |u i | ≤ 1 for all i ∈ I (ii) {1 ≤ a∈Si a | i ∈ I} with each S i ⊆ Σ finite (iii) {e ≤ 0} for e ∈ T(Σ) (iv)
Note that Item iii above covers finite sets of hypotheses of the form {e i ≤ 0} i∈I , as these can be encoded as the single hypothesis i∈I e i ≤ 0.

Compositional reductions

The previous subsection gives reductions to the empty set for single equations. However, in the examples we often start with a collection of hypotheses of different shapes, which we wish to reduce to the empty set. Therefore, we now discuss a few techniques for combining reductions.

Throughout this section, for sets of hypotheses H 1 , . . . , H n we often denote the associated closure by cl i instead of cl Hi , cl i,j instead of cl Hi∪Hj and cl i...j instead of cl i≤k≤j H k . Similarly, we write st i instead of st Hi etc. First, there are the basic observations that reductions compose (Lemma 3.7) and that equiderivable sets of hypotheses always reduce to each other, via the identity (Lemma 3.8). The following useful lemma allows to combine reductions by union, and is used in many of the examples. Its assumptions allow one to compose the reductions sequentially. A similar lemma is formulated in the setting of bi-Kleene algebra in [START_REF] Kappé | Concurrent Kleene Algebra: Completeness and Decidability[END_REF]Lemma 4.46]. Lemma 3.9. Let H 1 , . . . , H n , H be sets of hypotheses over a common alphabet Σ, with n ≥ 1. If H i reduces to H for all i, and cl

1...n = cl n • • • • • cl 1 , then i≤n H i reduces to H.
The next lemma is useful to show the second requirement in Lemma 3.9.

Lemma 3.10. Let H 1 , . . . , H n be sets of hypotheses, such that

cl i • cl j ⊆ cl j • cl i for all i, j with i < j. Then cl 1...n = cl n • • • • • cl 1 . Remark 3.11. The condition cl i • cl j ⊆ cl j • cl i in Lemma 3.10 is equivalent to cl i,j = cl j • cl i .
With the latter formulation, Lemma 3.10 is stated in the bi-Kleene algebra setting as [START_REF] Kappé | Concurrent Kleene Algebra: Completeness and Decidability[END_REF]Lemma 4.50].

We now proceed with several lemmas that help proving cl

1 • cl 2 ⊆ cl 2 • cl 1 .
In particular, these allow to use the "one-step closure" st H from the fixed point characterisation of cl H (below Definition 2.2), for cl 1 in Lemma 3.12 and additionally for cl 2 in Lemma 3.13, assuming further conditions. Lemma 3.12. For all

H 1 , H 2 , if st 1 • cl 2 ⊆ cl 2 • cl 1 , then cl 1 • cl 2 ⊆ cl 2 • cl 1 . Lemma 3.13. Let H 1 , H 2 be sets of hypotheses such that the right-hand sides of inequations in H 1 are all words. If st 1 • st 2 ⊆ cl 2 • st = 1 then cl 1 • cl 2 ⊆ cl 2 • cl 1 .
We conclude this section by returning to hypotheses of the form e ≤ 0. If H 1 = {e ≤ 0} for some term e and H 2 is an arbitrary set of hypotheses, then we have cl

1 • cl 2 ⊆ cl 2 • cl 1 .
As a consequence, we can strengthen Lemma 3.6(iii) to the following result, which gives a general treatment of hypotheses of the from e ≤ 0: we can always get rid of finite sets of hypotheses of this form. A similar result, in terms of Horn formulas and in the context of KAT, is shown in [START_REF] Hardin | Modularizing the elimination of r=0 in Kleene algebra[END_REF].

Lemma 3.14. For any set of hypotheses H and any term e, there is a reduction from H ∪ {e ≤ 0} to H.

Kleene algebra with tests

In this section we apply the machinery from the previous sections to obtain a modular completeness proof for Kleene algebra with tests [START_REF] Kozen | Kleene algebra with tests: Completeness and decidability[END_REF].

A Kleene algebra with tests (KAT) is a Kleene algebra X containing a Boolean algebra L such that the meet of L coincides with the product of X, the join of X coincides with the sum of X, the top element of L is the multiplicative identity of X, and the bottom elements of X and L coincide.

Syntactically, we fix two finite sets Σ and Ω of primitive actions and primitive tests. We denote the set of Boolean expressions over alphabet Ω by T BA :

φ, ψ ::= φ ∨ ψ | φ ∧ ψ | ¬φ | ⊥ | | o ∈ Ω
We write BA φ = φ when this equation is derivable from Boolean algebra axioms [START_REF] Birkhoff | Modern applied algebra[END_REF][START_REF] Davey | Introduction to Lattices and Order[END_REF], and similarly for inequations. We let α, β range over atoms: elements of the set At 2 Ω . Those may be seen as valuations for Boolean expressions, or as complete conjunctions of literals: α is implicitly seen as the Boolean formula α(o)=1 o ∧ α(o)=0 ¬o. They form the atoms of the Boolean algebra generated by Ω. We write α |= φ when φ holds under the valuation α. A key property of Boolean algebras is that for all atoms α and formulas φ, we have

α |= φ ⇔ BA α ≤ φ and BA φ = α|=φ α
The KAT terms over alphabets Σ and Ω are the regular expressions over the alphabet Σ + T BA : T KAT T(Σ + T BA ). We write KAT e = f when this equation is derivable from the axioms of KAT, and similarly for inequations.

The standard interpretation of KAT associates to each term a language of guarded strings. A guarded string is a sequence of the form α 0 a 0 α 1 a 1 . . . a n-1 α n with a i ∈ Σ for all i < n, and α i ∈ At for all i ≤ n. We write GS for the set At × (Σ × At) * of such guarded strings. Now, the interpretation G : T(Σ + T BA ) → 2 GS is defined as the homomorphic extension of the assignment G(a) = {αaβ | α, β ∈ At} for a ∈ Σ and G(φ) = {α | α |= φ} for φ ∈ T BA , where for sequential composition of guarded strings the coalesced product is used. The coalesced product of guarded strings uα and βv is defined as uαv if α = β and undefined otherwise. We now reprove this result using Kleene algebra with hypotheses. We start by defining the additional axioms of KAT as hypotheses. Definition 4.2. We write bool for the set of all instances of Boolean algebra axioms over T BA and glue for the following set of hypotheses relating the Boolean algebra connectives to the Kleene algebra ones

glue = {φ ∧ ψ = φ • ψ, φ ∨ ψ = φ + ψ | φ, ψ ∈ T BA } ∪ {⊥ = 0, = 1}
We then define kat = bool ∪ glue.

(Note that all these equations are actually understood as double inequations.)

We prove completeness of KA kat in Section 4.2 below, by constructing a suitable reduction. Recall that this means completeness w.r.t. the interpretation cl kat ( -) in terms of closed languages. Before proving completeness of KA kat , we compare it to the classical completeness (Theorem 4.1). First note that KA kat contains the same axioms as Kleene algebra with tests, so that provability in KA kat and KAT coincide: KA kat e = f iff KAT e = f . Comparing the interpretation cl kat ( -) to the guarded string interpretation G is slightly more subtle, and is the focus of the next subsection.

Relation to guarded string interpretation

To relate the guarded string model and the model obtained with closure under kat, we first develop the following lemmas.

The key step consists in characterising the strings that are present in the closure of a language of guarded strings (Lemma 4.3) below. First observe that a guarded string may always be seen as a word over the alphabet Σ + T BA . Conversely, a word over the alphabet Σ + T BA can always be decomposed as a sequence φ 0 a 0 • • • φ n-1 a n-1 φ n where a i ∈ Σ for all i < n and each φ i is a possibly empty sequence of Boolean expressions. We let φ range over such sequences, and we write φ for the conjunction of the elements of φ. Lemma 4.3. Let L be a language of guarded strings. We have

φ 0 a 0 • • • φ n-1 a n-1 φ n ∈ cl kat (L) ⇔ ∀ (α i ) i≤n , (∀i ≤ n, α i |= φ i ) ⇒ α 0 a 0 • • • α n-1 a n-1 α n ∈ L
Then we show that the kat-closures of e and G(e) coincide:

Lemma 4.4. For all KAT expressions e, cl kat ( e ) = cl kat (G(e)).

Let GS be the set of all guarded strings. We also have: As an immediate consequence of these two lemmas, we can finally relate the guarded strings languages semantics to the kat-closed languages one:

Corollary 4.6. Let e, f ∈ T kat . We have G(e) = G(f ) ⇔ cl kat ( e ) = cl kat ( f ).

Completeness

To prove completeness of the closed language model wrt kat, we take the following steps:

1. We reduce the hypotheses in kat to a simpler set of axioms: by putting the Boolean expressions into normal forms via the atoms, we can get rid of the hypotheses in bool. We do not remove the hypotheses in glue directly: we transform them into the following hypotheses about atoms:

atom = {α • β ≤ 0 | α, β ∈ At, α = β} ∪ {α ≤ 1 | α ∈ At} ∪ {1 ≤ α∈At α}
We thus first show that kat reduces to atom. 2. Then we use results from Section 3.1 and Section 3.2 to construct a reduction from atom to the empty set, and thereby obtain completeness of KA kat .

Let r : T(Σ + T BA ) → T(Σ + At) be the homomorphism defined by

r(x) = a x = a ∈ Σ α|=φ α x = φ ∈ T BA
We show below that r yields a reduction from kat to atom, using Lemma 3.3. In the sequel, we use atom 1 , atom 2 and atom 3 , or simply 1, 2, 3, to denote the three families of inequations in atom.

Lemma 4.7. We have KA atom 1 = α∈At α, and for all α, KA atom αα = α.

Lemma 4.8. For all e ≤ f ∈ kat, we have that KA atom r(e) ≤ r(f ).

Lemma 4.9. The homomorphism r yields a reduction from kat to atom.

Proof. We use Lemma 3.3. We first need to show KA kat atom: for α, β ∈ At with α = β, we have the following derivations in KA kat

α • β = α ∧ β = ⊥ = 0 α ≤ = 1 1 = = α|= α = α∈At α Now for a ∈ Σ + At, we have a = r(a) (syntactically): if a = a ∈ Σ, then r(a) = a; if a = α ∈ At, then r(α) = α|=α α = α.
The first condition about r is thus satisfied, and it suffices to verify the second condition about r for φ ∈ T BA . In this case, we have we have KA kat r(φ) = α|=φ α = α|=φ α = φ. The third and last condition was proven in Lemma 4.8.

Now we must reduce atom to the empty set. We can immediately get rid of atom 1 : by Lemma 3.14, atom reduces to atom 2,3 . For atom 2 and atom 3 , we have individiual reductions to the empty set via Lemma 3.6(i) and (ii), respectively. We combine those reductions via Lemma 3.9, by showing that their corresponding closures can be organised as follows: Proof. We simply write 2 and 3 for atom 2 and atom 3 . Since the right-hand sides of atom 2 are words, by Lemma 3.13 and Lemma 3.10, it suffices to prove st

2 • st 3 ⊆ cl 3 • st 2 . We actually prove st 2 • st 3 ⊆ st 3 • st 2 .
Assume w ∈ st 2 (st 3 (L)) for some language L. Hence, w = uαv for some atom α and words u, v such that and uv ∈ st 3 (L). In turn, we uv must be equal to u v for some words u , v such that for all atoms β, u βv ∈ L. By symmetry, we may assume |u| ≤ |u |, i.e., u = uw, v = wv for some word w. In this case, we have uwβv ∈ L for all β, whence uαwβv ∈ st 2 (L) for all β, whence uαv = uαwv ∈ st 3 (st 2 (L)), as required.

Putting everything together, we finally obtain completeness of KA kat .

Theorem 4.11. For all e, f ∈ T KAT , cl kat ( e ) = cl kat ( f ) implies KA kat e = f . Proof. kat reduces to atom (Lemma 4.9), which reduces to atom 2,3 by Lemma 3.14. The latter set reduces to the empty set by Lemma 4.10, Lemma 3.6 and Lemma 3.9. Thus kat reduces to the empty set, and we conclude via completeness of Kleene algebra (Theorem 2.1) and Theorem 3.2.

Kleene Algebra with Observations

A Kleene algebra with Observations (KAO) is a Kleene algebra which also contains a Boolean algebra, but the connection between the Boolean algebra and the Kleene algebra is different than for KAT: instead of having the axiom φ∧ψ = φ•ψ for all φ, ψ ∈ T BA , we only have φ ∧ ψ ≤ φ • ψ [START_REF] Kappé | Kleene algebra with observations[END_REF]. This system was introduced to allow for concurrency and tests in a Kleene algebra framework, because associating φ • ψ and φ ∧ ψ in a concurrent setting is no longer appropriate: φ ∧ ψ is one event, where we instantenously test whether both φ and ψ are true, while φ • ψ performs first the test φ, and then ψ, and possibly other things can happen between those tests in another parallel thread. Hence, the behaviour of φ ∧ ψ should be included in φ • ψ, but they are no longer equivalent. (Note that even if we add the axiom 1 = , in which case we have that φ • ψ is below both ψ and φ, this is not enough to collapse φ • ψ and φ ∧ ψ, because φ • ψ need not be an element of the Boolean algebra.)

Algebraically this constitutes a small change, and an ad-hoc completeness proof is in [START_REF] Kappé | Kleene algebra with observations[END_REF]. Here we show how to obtain completeness within our framework. We also show how to add the additional and natural axiom 1 = , which is not present in [START_REF] Kappé | Kleene algebra with observations[END_REF], and thereby emphasise the modular aspect of the approach.

Similar to KAT, we add the additional axioms of KAO to KA as hypotheses. The additional axioms of KAO are the axioms of Boolean algebra and the axioms specifying the interaction between the two algebras. The KAO-terms are the same as the KAT-terms: regular expression over the alphabet Σ + T BA . Definition 5.1. We define the set of hypotheses kao = bool ∪ glue , where

glue = {φ ∧ ψ ≤ φ • ψ, φ ∨ ψ = φ + ψ | φ, ψ ∈ T BA } ∪ {⊥ = 0}
We prove completeness with respect to the closed interpretation under hypotheses: cl kao ( -). As shown below, this also implies completeness for the language model presented in [START_REF] Kappé | Kleene algebra with observations[END_REF]. We take similar steps as for KAT:

1. Reduce kao to the simpler set of axioms contr = {α ≤ α • α | α ∈ At}, where At = 2 Ω is the set of atoms, as in Section 4. 2. Use results from Section 3.1 to reduce contr to the empty set.

For the first step, we use the same homomorphism r as for KAT.

Lemma 5.2. For all e ≤ f ∈ kao, we have KA contr r(e) ≤ r(f ).

Lemma 5.3. The homomorphism r yields a reduction from kao to contr.

Proof. Like for Lemma 4.9, we use Lemma 3.3. We show KA kao contr: for α ∈ At, we have KA kao α = α ∧ α ≤ α • α. The first and second condition about r are obtained like in the KAT case: the glueing equations for ∧ were not necessary there. The third and last condition was proven in Lemma 5.2.

Theorem 5.4. For all e, f ∈ T KAT , cl kao ( e ) = cl kao ( f ) implies KA kao e = f . Proof. kao reduces to contr (Lemma 5.3), which reduces to ∅ by Lemma 3.6(i), as both α and α • α are words and α is a word of length 1.

Note that the semantics defined in [START_REF] Kappé | Kleene algebra with observations[END_REF] actually corresponds to cl contr ( r(-) ) rather than cl kao ( -). These semantics are nonetheless equivalent, kao reducing to contr via r (the proof of Theorem 3.2 actually establishes that when H reduces to H via r and KA H is complete, we have cl

H ( e ) = cl H ( f ) iff cl H ( r(e) ) = cl H ( r(f ) ) for all expressions e, f ).
Because we set up KAO in a modular way, we can now easily extend it with the extra axiom = 1. Combining the proofs that r is a reduction from kat to atom and from kao to contr, we can easily see that r is also a reduction from kao ∪ { = 1} to contr ∪ atom 2 ∪ atom 3 . To obtain completeness, it thus suffices to explain how to combine the closures w.r.t. contr, atom 2 , and atom 3 .

Kleene algebra with positive tests

In KAT, tests are assumed to form a Boolean algebra. Here we study the structure obtained by assuming that they only form a distributive lattice. A Kleene algebra with positive tests (KAPT) is a Kleene algebra X containing a lattice L such that the meet of L coincides with the product of X, the join of X coincides with the sum of X, and all elements of L are below the multiplicative identity of X. (We discuss the variant where we have a bounded lattice at the end, see Remark 6.6). Since the product distributes over sums in X, L must be a distributive lattice. Also note that there might be elements of X below 1 that do not belong to L.

As before, we fix two finite sets Σ and Ω of primitive actions and primitive tests. Then we consider regular expressions over the alphabet Σ + T DL , where T DL is the set of lattice expressions over Ω: expressions built from elements of Ω and two binary connectives ∨ and ∧.

We write dl for the set of all instances of distributive lattice axioms over T DL [START_REF] Davey | Introduction to Lattices and Order[END_REF], and we set kapt dl ∪ glue where

glue {φ ∧ ψ = φ • ψ, φ ∨ ψ = φ + ψ | φ, ψ ∈ T DL } ∪ {φ ≤ 1 | φ ∈ T DL }
Like for Boolean algebras, the free distributive lattice over Ω is finite and can be described easily. An atom α is a non-empty subset of Ω, and we write At for the set of such atoms as before. However, while an atom {a, b} of Boolean algebra was implicitly interpreted as the term a ∧ b ∧ ¬c (when Ω = {a, b, c}), the same atom in the context of distributive lattices is implicitly interpreted as the term a ∧ b-there are no negative literals in distributive lattices. Again similarly to the case of Boolean algebras, the key property for atoms in distributive lattices is the following: for all atoms α and formulas φ, we have

α |= φ ⇔ DL α ≤ φ and DL φ = α|=φ α
Like for KAT, such a property makes it possible to reduce kapt to the following set of equations on the alphabet Σ + At.

atom {α • β = α ∪ β | α, β ∈ At} ∪ {α ≤ 1 | α ∈ At}
(Note that in the right-hand side of the first equation, α ∪ β is a single atom, whose implicit interpretation is α ∧ β.) Lemma 6.1. There is a reduction from kapt to atom , witnessed by the homomorphism r : T(Σ + T DL ) → T(Σ + At) defined by

r(x) = a x = a ∈ Σ α|=φ α x = φ ∈ T DL
As a consequence, in order to get decidability and completeness for KAPT (i.e., kapt), it suffices to reduce atom to the empty set. Let us number the three kinds of inequations that appear in this set:

1={α∪β ≤ α•β | α, β ∈ At} 2={α•β ≤ α∪β | α, β ∈ At} 3={α ≤ 1 | α ∈ At} Lemma 3.6(i)
gives reductions to the empty set for 1 and 3, but so far we have no reduction for 2. We actually do not know if there is a reduction from 2 to the empty set. Instead, we establish a reduction from 2 together with 3 to 3 alone. Lemma 6.2. There is a reduction from 2,3 to 3, witnessed by the homomorphism r : T(Σ + At) → T(Σ + At) defined by

r(x) = a x = a ∈ Σ {α 1 • . . . • α n | α = i≤n α i , i = j ⇒ α i = α j } x = α ∈ At
(Note that the above reduction requires 3 in its target, and cannot be extended directly into a reduction from 1,2,3 to 3:

r(α ∪ β) ≤ r(α • β) cannot be proved in KA 3 -take α = {a}, β = {b}, then ba is a term in r(α ∪ β) which is not provably below ab = r(α • β).)
Composed with the existing reduction from 3 to the empty set (Lemma 3.6(i)), we thus have a reduction from 2,3 to the empty set. It remains to combine this reduction to the one from 1 to the empty set (Lemma 3.6(i) again). To this end, we would like to use Lemma 3.9, which simply requires us to prove that the closure cl atom = cl 1,2,3 is equal either to cl 1 • cl 2,3 or to cl 2,3 • cl 1 . Unfortunately, this is not the case. To see this, suppose we have two atomic tests a and b. For the first option, consider the singleton language {ab} (a word consisting of two atoms); we have ba ∈ cl 1,2,3 ({ab}) (because (a ∧ b) ∈ cl 1 ({ab}), and then using cl 2 ) but ba ∈ cl 1 (cl 2,3 ({ab})). For the second option, consider the singleton language {a}; we have (a ∧ b) ∈ cl 1,2,3 ({a}), because ab ∈ cl 3 ({a}), but (a ∧ b) ∈ cl 2,3 (cl 1 ({a})) because cl 1 ({a}) is just {a}, and cl 2,3 does not make it possible to forge conjunctions.

In order to circumvent this difficulty, we use a fourth family of equations:

4 = {α ∪ β ≤ α | α, β ∈ At}
These axioms are immediate consequences of 1 and 3. Therefore, 1,2,3 reduces to 1,2,3,4. Moreover they consist of 'letter-letter' inequations, which are covered by Lemma 3.6(i): 4 reduces to the empty set. We shall further prove that cl 1,2,3,4 = cl 4 • cl 3 • cl 2 • cl 1 and cl 2,3 = cl 3 • cl 2 , so that Lemma 3.9 applies to obtain a reduction from 1,2,3,4 to the empty set.

Lemma 6.3. We have the following inclusions of functions:

(i) st 1 • st 2 ⊆ st 2 • st 1 + id (ii) st 1 • st 3 ⊆ st 3 • st 1 + st 4 (iii) st 1 • st 4 ⊆ st 4 • st 1 (iv) st 2 • st 3 ⊆ st 3 • st 2 + st 3 • st 3 (v) st 2 • st 4 ⊆ st 4 • st 2 + st 4 • st 4 • st 2 (vi) st 3 • st 4 ⊆ st 4 • st 3 Lemma 6.4. We have cl 1,2,3,4 = cl 4 • cl 3 • cl 2 • cl 1 = cl 4 • cl 2,3 • cl 1 .
Proof. We use Lemma 3.10 and Lemma 3.13 repeatedly, on (combinations of) the inclusions provided by Lemma 6.3. See the proof in Appendix E.

Theorem 6.5. KA kapt reduces to the empty set, and is complete and decidable.

Proof. kapt reduces to atom by Lemma 6.1, which in turn reduces to 1, 2, 3, 4 by Lemma 3.8. The latter is composed of three sets of hypotheses, 1, 4, and 2, 3. All three of them reduce to the empty set: the first two by Lemma 3.6(i), and the third one by Lemma 6.2. These three reductions can be composed together by Lemma 3.9 and Lemma 6.4.

Remark 6.6. The case of Kleene algebras containing a bounded distributive lattice, with extremal elements ⊥ and coinciding with 0 and 1, may be obtained as follows. Allow the empty atom ∅ in At (interpreted as ), and add the inequation 5 = {1 ≤ ∅} to atom . Lemma 6.1 extends easily, and we have a reduction from 5 to the empty set (Lemma 3.6(i)). Therefore it suffices to find how to combine cl 5 with the other closures. We have cl 1,2,3,4,5

= cl 5 • cl 4 • cl 3 • cl 2 • cl 1 (see Lemma E.1
in Appendix E), so that we can conclude that the equational theory of Kleene algebras with a bounded distributive lattice is complete and decidable.

Related work

There is a range of papers on completeness and decidability of Kleene algebra together with specific forms of hypotheses, starting with [START_REF] Cohen | Hypotheses in Kleene algebra[END_REF]. The general case of Kleene algebra with hypotheses, and reductions to prove completeness, has been studied recently in [START_REF] Kappé | Concurrent Kleene algebra with observations: From hypotheses to completeness[END_REF][START_REF] Doumane | Kleene algebra with hypotheses[END_REF][START_REF] Kozen | Kleene algebra with equations[END_REF]. The current paper combines and extends these results, and thereby aims to provide a comprehensive overview and a showcase of how to apply these techniques to concrete case studies (KAT, KAO and the new theory KAPT). Below, we discuss each of these recent works in more detail. Kozen and Mamouras [START_REF] Kozen | Kleene algebra with equations[END_REF] define the canonical language model for KA with a set of hypotheses in terms of rewriting systems, as well as reductions and their role in completeness, and provide reductions for equations of the form 1 = w and a = w (cf. Lemma 3.6). Their general results cover completeness results which instantiate to KAT and NetKAT. In fact, the assumptions made in their technical development are tailored towards these cases; for instance, their assumption αβ ≤ ⊥ (in Assumption 2) rules out KAPT. The current paper focuses more on generality and how to construct reductions in a modular way. Doumane et al. [START_REF] Doumane | Kleene algebra with hypotheses[END_REF] also define reductions, with an emphasis on (un)decidability. In particular, they cover hypotheses of the form 1 ≤ a∈S a (cf. Lemma 3.6). A first step towards modularity may also be found in [START_REF] Doumane | Kleene algebra with hypotheses[END_REF]Proposition 3].

Kappé et al. [START_REF] Kappé | Concurrent Kleene algebra with observations: From hypotheses to completeness[END_REF] study hypotheses on top of bi-Kleene algebra, where the canonical interpretation is based on pomset languages, and ultimately prove completeness of concurrent Kleene algebra with observations; many of the results there apply to the word case as well. We follow this paper for the basic definitions and results for the general theory of Kleene algebra with hypotheses, with a small change in the actual definition of a reduction (Remark 3.5). Compositionality in the sense of Section 3.2 is treated in Kappé's PhD thesis [START_REF] Kappé | Concurrent Kleene Algebra: Completeness and Decidability[END_REF]. We extend these results with Lemmas 3.12, 3.13, which simplify the work needed to combine hypotheses. Further, we highlight the word case in this paper (as opposed to the pomset languages in concurrent Kleene algebra), by showcasing several examples.

A Additional lemmas on closures

Here we prove a few lemmas, which are used for the proofs in the remainder of this appendix.

Lemma A.1. Let H be a set of hypotheses whose right-hand sides are all words. Then st H is additive: for every family

(L i ) i∈I of languages, st H ( i∈I L i ) = i∈I st H (L i ). Moreover, in that case, cl H (L) = n∈N st n H (L).
Proof. For additivity, the right-to left containment follows by monotonicity of st H .

For the left-to-right containment, take a word w ∈ st H ( i∈I L i ). By definition of st H , there must be e ≤ f ∈ H such that w ∈ u e v for some words u, v ∈ Σ * such that u f v ⊆ i∈I L i . Since f is a word, we know that u f v = {uf v}. Hence, there exists an i ∈ I such that uf v ∈ L i . It follows that u e v ⊆ st H (L i ), and thus

w ∈ u e v ⊆ st H (L i ) ⊆ i∈I st H (L i ).
That we can stop the iteration at ω follows: we have st ω+1 H (L) ⊆ st ω H (L) by additivity.

Lemma A.2. For all sets of hypotheses H and languages L, K, we have

cl H (L)•K ⊆ cl H (L•K) L•cl H (K) ⊆ cl H (L•K) cl H (L)•cl H (K) ⊆ cl H (L•K)
Proof. The first two inclusions are symmetrical, and hold because the rules defining cl H are contextual. For the third inclusion, we use the first two in order to deduce cl

H (L)•cl H (K) ⊆ cl H (L•cl H (K)) ⊆ cl H (cl H (L•K)) = cl H (L•K).

B Proofs for Section 3 (Reductions)

For the proof of Lemma 3.3, we need the following definition.

For a map r : T(Σ) → T(Γ ), define ṙ :

P(Σ * ) → P(Γ * ) by ṙ(L) = w∈L r (w)
(Where words w are seen as regular expressions when fed to r.) We have the following property:

Lemma B.1. Let r : T(Σ) → T(Γ ) be a homomorphism. Then we have:

1. ṙ( e ) = r(e) for all e ∈ T(Σ), and

2. ṙ(L • K) = ṙ(L) • ṙ(K) for all L, K ⊆ Σ * .
Now we can prove Lemma 3.3.

Lemma 3.3. Assume Γ ⊆ Σ and let H, H be sets of hypotheses over Σ and Γ respectively, such that KA H H . If there exists a homomorphism r : T(Σ) → T(Γ ) such that:

1. For all a ∈ Γ , we have KA a ≤ r(a).

2. For all a ∈ Σ, we have KA H a = r(a).

3. For all e ≤ f ∈ H, we have KA H r(e) ≤ r(f ).

then H reduces to H .

Proof. First, we must prove KA H e = r(e) for all e ∈ T(Σ), which follows by induction on e, using that r is a homomorphism and Item 2.

Similarly, we get KA e ≤ r(e) for all e ∈ T(Γ ) from Item 1. By using soundness of KA and this latter result with words in Γ * , we obtain that for all languages

L ⊆ Γ * , L ⊆ ṙ(L) (1)
Secondly, we must prove cl H ( e ) ∩ Γ * = cl H ( r(e) ). For the right-to-left inclusion, the right-hand side is contained in Γ * by definition, and we have cl H ( r(e) ) ⊆ cl H ( r(e) )

(KA H H and Lemma 2.4)

= cl H ( e ) (KA H e = r(e) and soundness (Theorem 2.3))

For the left-to-right inclusion, we first prove that for all languages L ⊆ Σ * , ṙ(cl

H (L)) ⊆ cl H ( ṙ(L)) (2)
We do so by transfinite induction proving that for all ordinals κ,

ṙ(st κ H (L)) ⊆ cl H ( ṙ(L)) (3)
The base case is trivial. The limit case follows since ṙ is defined element-wise. For the induction step, suppose (3) holds for some κ; we have to prove ṙ(st

H (st κ H (L))) ⊆ cl H ( ṙ(L)). Let u, v, e, f be such that e ≤ f ∈ H and u f v ⊆ st κ H (L). Then we need to show that ṙ(u e v) ⊆ cl H ( ṙ(L)). Since, u f v ⊆ st κ H (L), the induction hypotheses entails ṙ(u f v) ⊆ cl H ( ṙ(L))
. We argue as follows:

ṙ(u e v) ⊆ cl H ( ṙ(u e v)) = cl H ( r(u) • r(e) • r(v) ) (Lemma B.1) ⊆ cl H ( r(u) • r(f ) • r(v) ) ( ) = cl H ( ṙ(u f v)) (Lemma B.1) ⊆ cl H (cl H ( ṙ(L))) (IH) = cl H ( ṙ(L))
Where we deduce the intermediate inclusion ( ) from soundness of KA H and a derivation KA H r(u) • r(e) • r(v) ≤ r(u) • r(f ) • r(v) obtained from monotonicity and Item 3. This concludes the proof of (3), and thus [START_REF] Birkhoff | Modern applied algebra[END_REF].

Putting everything together, we have, for all expressions e ∈ T(Σ):

cl H ( e ) ∩ Γ * ⊆ ṙ(cl H ( e ) ∩ Γ * ) (by (1)) ⊆ ṙ(cl H ( e )) ⊆ cl H ( ṙ( e )) (by (2)) = cl H ( r(e) ) (Lemma B.1)
which concludes the proof.

Lemma 3.6. Each of the following sets of hypotheses reduce to the empty set (of hypotheses over Σ). (iii) This is basically due to [START_REF] Cohen | Hypotheses in Kleene algebra[END_REF], but since it is phrased differently there we include a proof. Define r : T(Σ) → T(Σ) by r(f

(i) {u i ≤ w i | i ∈ I} with u i , w i ∈ Σ * and |u i | ≤ 1 for all i ∈ I (ii) {1 ≤ a∈Si a | i ∈ I} with each S i ⊆ Σ finite (iii) {e ≤ 0} for e ∈ T(Σ) (iv
) = f + Σ * • e • Σ * for f ∈ T(Σ)
, where Σ * is seen as the expression ( a∈Σ a) * . We claim r witnesses a reduction. First, we have KA H f ≤ r(f ) trivially, and KA H r(f ) ≤ f follows because e ≤ 0 ∈ H. Second, we have to prove that r(f ) = cl H ( f ). It is easy to check that st H • st H = st H for this H, so by the iterative characterisation of cl H we get cl

H (L) = L ∪ st H for any L ⊆ Σ * . Now, cl H (L) = L ∪ st H (L) = L ∪ {u e v | u 0 v ⊆ L} = L ∪ {u e v | u, v ∈ Σ * } for all L ⊆ Σ * . Therefore, cl H ( f ) = f ∪ {u e v | u, v ∈ Σ * } = f + Σ * eΣ * = r(f )
for all f ∈ T(Σ). (iv) Hypotheses of a similar form are studied in the setting of Kleene algebra with tests in [START_REF] Hardin | On the elimination of hypotheses in Kleene algebra with tests[END_REF]. Consider the case {ea ≤ a}. Define r as the unique homomorphism satisfying r(a) = e * a, and r(b) = b for all b ∈ Σ with b = a.

We use Lemma 3.3 to show that this witnesses a reduction.

The first two conditions are trivial for letters b ∈ Σ with a = b, since r is the identity on those letters. For a, we have KA a ≤ e * a = r(a) easily from the KA axioms. Further, we get KA H r(a) = e * a ≤ a by ea ≤ a and the (left) induction axiom for Kleene star in KA. Finally, we have to prove that KA r(ea) ≤ r(a). We have r(a) = e * a, and since e does not contain a, we have r(e) = e. Therefore, r(ea) = r(e)r(a) = ee * a, and the required inequality follows since KA ee * ≤ e * .

Lemma 3.7. Let H 1 , H 2 and H 3 be sets of hypotheses. If H 1 reduces to H 2 and H 2 reduces to H 3 then H 1 reduces to H 3 .

Proof. We have KA H1 H 2 and KA H2 H 3 , and therefore KA H1 H 3 . Let r 1 : T(Σ 1 ) → T(Σ 2 ) and r 2 : T(Σ 2 ) → T(Σ 3 ) be witnesses of the reductions from H 1 to H 2 and from H 2 to H 3 respectively. We show that r 2 • r 1 is a reduction from H 1 to H 3 .

Since KA H1 e = r 1 (e) for all e ∈ T(Σ 1 ), KA H2 e = r 2 (e) for all e ∈ T(Σ 2 ) and KA H1 H 2 , we get KA H1 e = r 1 (e) = r 2 (r 1 (e)).

Finally, we have: e ≤ f . Now, let r 1 , . . . , r n be witnesses for the reductions from H 1 , . . . , H n to H. We show that r = r n • . . . • r 1 is a reduction under these assumptions.

cl 1 ( e ) ∩ Σ * 3 = (cl 1 ( e ) ∩ Σ * 2 ) ∩ Σ * 3 = cl 2 ( r 1 (e) ) ∩ Σ * 3 = cl 3 ( r 2 (r 1 (e)) ) using that Σ 3 ⊆ Σ 2 ,
Further, it is easy to prove KA i≤k Hi e = r k • . . . • r 1 (e) for all k ≤ n, by induction on k, using that each r i is a reduction.

Finally, for the second requirement on r k • . . . r 1 to be a reduction, observe that the restriction to the codomain alphabet is void since it coincides with the alphabet in the domain, that is, we have cl i ( e ) = cl H ( r i (e) ) for each i. This implies that, for all k ≤ n, we have cl k

• . . . • cl 1 ( e ) = cl H ( r k • . . . r 1 (e) )
by induction on k. Indeed, the base case (k = 1) holds by assumption. For the inductive case, if it holds for some k with k < n, then

cl k+1 • cl k • . . . • cl 1 ( e ) = cl k+1 (cl H ( r k • . . . r 1 (e) )) (IH) = cl k+1 ( r k • . . . r 1 (e) ) = cl H ( r k+1 • r k • . . . r 1 (e) ) (
i • cl j ⊆ cl j • cl i for all i, j with i < j. Then cl 1...n = cl n • • • • • cl 1 .
Proof. The right to left inclusion is trivial. For the other inclusion, we use the fixed point characterisation of cl 1...n : given a language L, it suffices to prove that By assumption, for all i < j we have cl i • cl j ⊆ cl j • cl i . Hence, we can derive

cl n • • • • • cl 1 (L) is a pre-fixed point of st 1...n,L (Definition 2.2), i.e., st 1...n (cl n • • • • • cl 1 (L)) ∪ L ⊆ cl n • • • • • cl 1 (L) .
st i • cl n • . . . • cl 1 (L) ⊆ cl i • cl n • . . . • cl 1 (L) ⊆ cl 1 • . . . • cl i • cl i • . . . • cl n (L) = cl n • . . . • cl 1 (L) using that cl i • cl i ⊆ cl i in the last step. Lemma 3.12. For all H 1 , H 2 , if st 1 • cl 2 ⊆ cl 2 • cl 1 , then cl 1 • cl 2 ⊆ cl 2 • cl 1 . Proof. It suffices to prove that st 1 (cl 2 (cl 1 (L))) ∪ cl 2 (L) ⊆ cl 2 (cl 1 (L))
by the fixed point characterisation of cl 1 . Indeed, we have st 1 (cl 2 (cl 1 (L))) ⊆ cl 2 (cl 1 (cl 1 (L))) = cl 2 (cl 1 (L)) using the assumption. Further, we have cl 2 (L) ⊆ cl 2 (cl 1 (L)) by definition of closure. Lemma 3.13. Let H 1 , H 2 be sets of hypotheses such that the right-hand sides of inequations in H 1 are all words. If

st 1 • st 2 ⊆ cl 2 • st = 1 then cl 1 • cl 2 ⊆ cl 2 • cl 1 .
Observe that st 1 is constant:

st 1 (L) = {u e v | u, v ∈ Σ * , u 0 v ⊆ L} = {u e v | u, v ∈ Σ * } = {uwv | u, v ∈ Σ * , w ∈ e }
using in the second step that u 0 v = u∅v = ∅. Thus, for any language L, we have st

1 (cl 2 (L)) = st 1 (L) ⊆ cl 1 (L) ⊆ cl 2 (cl 1 (L)
), using that st 1 is constant in the first equality.

Lemma 3.14. For any set of hypotheses H and any term e, there is a reduction from H ∪ {e ≤ 0} to H.

Proof. Let H 1 = {e ≤ 0}. First, KA H∪H1 H is trivial. Now let r : T(Σ) → T(Σ) be a reduction from H 1 to ∅, which exists by Lemma 3.6. We claim that r is also a reduction from H ∪ {e ≤ 0} to H. For any term f , KA H∪H1 f = r(f ) holds since KA H1 f = r(f ).

For the second requirement on r, we need to show that cl H∪H1 ( f ) = cl H ( r(f ) ); note that the alphabet restriction is dropped as the domain and codomain of r are equal. By Lemma B.2 and Lemma 3.10 we have cl

H∪H1 = cl H • cl 1 . Hence, cl H∪H1 ( f ) = cl H (cl 1 ( f )) = cl H ( f ) using that r is a reduction from H 1 to ∅.
C Proofs for Section 4 (KAT) Lemma 4.3. Let L be a language of guarded strings. We have

φ 0 a 0 • • • φ n-1 a n-1 φ n ∈ cl kat (L) ⇔ ∀ (α i ) i≤n , (∀i ≤ n, α i |= φ i ) ⇒ α 0 a 0 • • • α n-1 a n-1 α n ∈ L Proof.
The proof for the left to right direction proceeds by induction on the closure (seen as the least fixed point of st kat,L -Definition 2.2). In the base case, where the word already belongs to L, and thus is already a guarded string, the φ i must all be single atoms. Since α |= β iff α = β for all atoms α, β, the condition is immediately satisfied. Otherwise, we have

φ 0 a 0 • • • φ n-1 a n-1 φ n ∈ u e v for u, v ∈ (Σ + T BA ) * with u f v ⊆ cl kat (L
) and e ≤ f ∈ kat, and we know that the induction hypothesis applies to all words in u f v. We proceed by a case distinction on the hypothesis in e ≤ f ∈ kat.

e ≤ f ∈ bool: in this case e = φ and f = ψ for some formulas φ, ψ such that BA φ = ψ. Therefore, we have α |= φ iff α |= ψ for all atoms α, so that the induction hypothesis on the unique word of uψv is equivalent to the property we have to prove about the unique word of uφv.

e = φ ∧ ψ and f = φ • ψ: there must be j such that φ j = φ(φ ∧ ψ)ψ for φ, ψ ∈ T BA * . The word of uφψv has the same decomposition as u(φ ∧ ψ)v, except that φ j is replaced by φφψψ. Since BA φφψψ = φ(φ ∧ ψ)ψ, the induction hypothesis immediately applies.

-The case for e = φ • ψ and f = φ ∧ ψ is handled similarly.

e = φ ∨ ψ and f = φ + ψ: there must be j such that φ j = φ(φ ∨ ψ)ψ for φ, ψ ∈ T BA * . We have f = {φ, ψ} and the two words of u f v have the same decomposition as u(φ ∨ ψ)v, except that φ j is replaced by φφψ or φψψ. We use the induction hypothesis and the fact that α |= φ ∨ ψ iff α |= φ or α |= ψ.

e = φ + ψ and f = φ ∨ ψ: there must be j such that w.l.o.g. φ j = φ(φ)ψ for φ, ψ ∈ T BA * . We have f = {φ ∨ ψ} and the word in u f v has the same decomposition as u(φ)v, except that φ j is replaced by φ(φ ∨ ψ)ψ. We use the induction hypothesis and the fact that if α |= φ then α |= φ ∨ ψ.

e = ⊥ and f = 0: there must be j such that ⊥ belongs to φ j , so that there are no atoms α such that α |= φ j : the condition is trivially satisfied. e = 0 and f = ⊥: in this case u e v is empty so this case is trivially satisfied.

e = and f = 1: there is j, φ, ψ such that φ j = φ ψ. The word of uv decomposes like u v, except that φ j is replaced by φψ. Since BA φψ = φ ψ, the induction hypothesis suffices to conclude.

-The case where e = 1 and f = is handled similarly.

We now prove the right-to-left implication. From the assumptions we obtain α|=φ 0 α a 0 . . .

α|=φ n-1 α a n-1 α|=φ n α ⊆ L
We deduce using the glueing inequations for ∨ and ⊥ that

  α|=φ 0 α   a 0 . . .   α|=φ n-1 α   a n-1   α|=φ n α   ∈ cl kat (L)
Since BA φ = α|=φ α for all φ, the inequations from bool yield

φ 0 a 0 . . . φ n-1 a n-1 φ n ∈ cl kat (L)
We conclude with the glueing inequations for ∧ and , which give

φ 0 a 0 . . . φ n-1 a n-1 φ n ∈ cl kat (L)
Now we turn to proving Lemma 4.4, yielding Corollary 4.6. We first prove two lemmas about kat-closures of guarded string languages.

Lemma C.1. For all guarded string languages L, K, cl kat (L • K) ⊆ cl kat (L K).

Proof. We show that L • K ⊆ cl kat (L K), which is sufficient. Take w ∈ L • K. Hence, w = xy with x ∈ L and y ∈ K. Because x and y are guarded strings, we know both of them begin and end in an atom. So we can write x = x α and y = βy for some α, β ∈ At.

-If α = β, then xαy ∈ L K. In that case, we have xy = x ααy , but then, since x and y are guarded strings and α is the only atom s. Proof. It suffices to prove L * ⊆ cl kat (L ), which in turn follows once we prove ε ∈ cl kat (L ) and Lcl kat (L ) ⊆ cl kat (L ). The former follows from the fact that KA kat 1 ≤ α α, since L contains L 0 and thus all atoms α. For the latter, we have

L • cl kat (L ) ⊆ cl kat (L • L ) (Lemma A.2) ⊆ cl kat (L L ) (Lemma C.1) ⊆ cl kat (L )
We can finally prove Lemma 4.4: Proof. It suffices to prove that e ⊆ cl kat (G(e)) and G(e) ⊆ cl kat ( e ). We prove both results via induction on e.

We start with e ⊆ cl kat (G(e)).

-0: trivial as 0 = ∅. -0: trivial as Recall that GS is the set of all guarded strings. We deduce from Lemma 4.3 that closing a guarded string language under kat does not add new guarded strings:

+ f = e ∪ f ⊆ cl kat (G(e)) ∪ cl kat (G(f )) (IH) ⊆ cl kat (G(e) ∪ G(f )) = cl kat (G(e + f )) (cl kat monotone) -e • f : we have e • f = e • f ⊆ cl kat (G(e)) • cl kat (G(f )) (IH) ⊆ cl kat (G(e) • G(f )) (Lemma A.2) ⊆ cl kat (G(e) G(f )) = cl kat (G(e • f )) (Lemma C.
G(0) = ∅. -1: G(1) = {α | α ∈ At}; for all α, KA kat α ≤ 1, whence α ∈ cl kat {ε} = cl kat 1 . -a ∈ Σ: G(a) = {αaβ | α, β ∈ At}; like above, for all α, β, αaβ ∈ cl kat {a} = cl kat a . -φ ∈ T BA : G(φ) = {α | α |= φ}, for all α such that α |= φ, KA kat α ≤ φ, whence α ∈ cl kat {φ} = cl kat φ . -e + f : we have G(e + f ) = G(e) ∪ G(f ) ⊆ cl kat ( e ) ∪ cl kat ( f ) (IH) ⊆ cl kat ( e ∪ f ) (cl kat monotone) = cl kat ( e + f )) -e • f : suppose w ∈ G(e • f ), i.
Lemma C.3. For all guarded string language L, L = cl kat (L) ∩ GS.

Proof. The left-to-right direction is trivial, as L ⊆ cl kat (L) and all strings in L are guarded. For the right-to-left direction, given a guarded string α 0 a 0 . . . a n-1 α n in cl kat (L), we simply use Lemma 4.3 with the sequence of α i themselves: we have α i |= α i for all i, so that α 0 a 0 . . . a n-1 α n actually belongs to L. Proof. We have five families of equations to consider, and thus ten families of inequations. We derive equalities directly, so that we only have to consider five cases:

-⊥ = 0: we derive As uαl m = uαv we have obtained the required result. 2. l = uα p and m = α q v for p, q ≥ 0 and p + q = n. Here we have

uα p α∈At α α q v = l α∈At α m
Hence we know that uα p αα q v ∈ l α∈At α m ⊆ st κ 3 (cl contr (L)). Via the induction hypothesis we obtain that uαv ∈ cl 3 • cl contr (L). E Proofs for Section 6 (KAPT) Lemma 6.2. There is a reduction from 2,3 to 3, witnessed by the homomorphism r : T(Σ + At) → T(Σ + At) defined by

r(x) = a x = a ∈ Σ {α 1 • . . . • α n | α = i≤n α i , i = j ⇒ α i = α j } x = α ∈ At
Proof. We use Lemma 3.3. For a letter a ∈ Σ, r(a) = a so that the first two conditions are trivial; we thus need to prove them only for atoms α ∈ At. KA α ≤ r(α) follows by using the singleton sequence α which is a term in the sum r(α). For the second condition, it thus suffices to show KA 2,3 r(α) ≤ α, i.e., KA 2,3 α 1 . . . α n ≤ α for all sequences α 1 , . . . , α n of pairwise distinct atoms whose union is α. This follows by n -1 successive applications of inequations in 2. It remains to check the last condition of Lemma 3.3; we consider the two kinds of equations separately:

There is another overlap when u = rγ, which is solved as follows, in st 2 st 1 : r(γ ∪ α)βw rγαβw

Lemma 2 . 4 (

 24 [START_REF] Kappé | Concurrent Kleene algebra with observations: From hypotheses to completeness[END_REF] Lemma 4.10]). Let H and H be sets of hypotheses such that KA H H . Then cl H ⊆ cl H .

1 .

 1 KA H e = r(e), and 2. cl H ( e ) ∩ Γ * = cl H ( r(e) ).

  {ea ≤ a} and {ae ≤ a} for a ∈ Σ, e ∈ T(Σ \ {a}) Proof. (i) This is [25, Theorem 2]. (The result mentions equations, but in the proof only the relevant inequations are used.) (ii) This is [10, Proposition 6].

Theorem 4 . 1 (

 41 [START_REF] Kozen | Kleene algebra with tests: Completeness and decidability[END_REF] Theorem 8]). For all e, f ∈ T KAT , we have KAT e = f iff G(e) = G(f ).

Lemma 4 . 5 .

 45 For all KAT expressions e, G(e) = cl kat ( e ) ∩ GS.

Lemma 4 . 10 .

 410 We have cl atom2,3 = cl atom3 • cl atom2

Lemma 5 . 5 .

 55 We have cl 2 • cl contr ⊆ cl contr • cl 2 and cl contr • cl 3 ⊆ cl 3 • cl contr Proof. See Appendix D, the second inclusion is non-trivial. Theorem 5.6. For all e, f ∈ T KAT , if cl kao∪{ =1} ( e ) = cl kao∪{ =1} ( f ) then KA kao∪{ =1} e = f . Proof. Because we know cl 2,3 = cl 3 •cl 2 (Lemma 4.10) and hence cl 2 •cl 3 ⊆ cl 3 •cl 2 , we can use Lemma 3.10 with Lemma 5.5 to deduce cl contr,2,3 = cl 3 • cl contr • cl 2 , and obtain completeness via Lemma 3.9 and the fact that contr, 2 and 3 all reduce to the empty set.

Lemma A. 3 .

 3 For all sets of hypotheses H and languages L, we have cl H (L) * ⊆ cl H (L * ) Proof. It suffices to show 1 + L • cl H (L * ) ⊆ cl H (L * ), which follows easily from Lemma A.2.

  ) {ea ≤ a} and {ae ≤ a} for a ∈ Σ, e ∈ T(Σ \ {a}) Proof. (i) This is [25, Theorem 2]. (The result mentions equations, but in the proof only the relevant inequations are used.) (ii) This is [10, Proposition 6].

  The inclusion L ⊆ cl n • . . . • cl 1 (L) holds since each cl i is a closure. For the other part, we first observe thatst 1...n (cl n • . . . • cl 1 (L)) = st 1 (cl n • . . . • cl 1 (L)) ∪ . . . ∪ st n (cl n • . . . • cl 1 (L))

  t. α |= α ∧ α, we get xy ∈ cl kat (L K) by Lemma 4.3. -Otherwise, if α = β, then a priori xy ∈ L K. However, since there are no atoms γ s.t. γ |= α ∧ β, we have xy ∈ cl kat (L K) by Lemma 4.3. Given a guarded string language L, let us denote by L the language L iterated w.r.t. the coalesced product : L = n L n , where L 0 = {α | ∈ At} and L n+1 = L L n . Lemma C.2. For all guarded string languages L, cl kat (L * ) ⊆ cl kat (L ).

Lemma 4 . 4 .

 44 For all KAT expressions e, cl kat ( e ) = cl kat (G(e)).

- 1 : 1 =

 11 {ε} and G(1) = {α | α ∈ At}, therefore ε ∈ cl kat (G(1)) by Lemma 4.3. a ∈ Σ: a = {a} and G(a) = {αaβ | α, β ∈ At}, therefore a ∈ cl kat (G(a)) by Lemma 4.3. φ ∈ T BA : φ = {φ} and G(φ) = {α | α |= φ}, hence φ ∈ cl kat (G(φ)) by Lemma 4.3. e + f : we have e

1 )

 1 e * : we have e * = e * ⊆ cl kat (G(e)) * (IH) ⊆ cl kat (G(e) * ) (Lemma A.3) ⊆ cl kat (G(e) ) = cl kat (G(e * )) (Lemma C.2) Next we prove G(e) ⊆ cl kat ( e ):

  e., w = xαy for xα ∈ G(e) and αy ∈ G(f ). Via the induction hypothesis we know that xα ∈ cl kat ( e ) and αy ∈ cl kat ( f ). Hence xααy ∈ cl kat ( e )•cl kat ( f ) ⊆ cl kat ( e • f ) via Lemma A.2. As KA kat α ≤ αα, we get that xαy ∈ cl kat ( e • f ).e * : a similar argument works.

Lemma 4 . 5 .

 45 For all KAT expressions e, G(e) = cl kat ( e ) ∩ GS. Proof. Immediate from Lemma C.3 and Lemma 4.4.

Lemma 4 . 7 .

 47 We have KA atom 1 = α∈At α, and for all α, KA atom αα = α.Proof. The first equation comes from (atom.2) and (atom.3) For the second one,KA atom α = α • 1 = α • β∈At β = β∈At α • β = α • αwhere we use (atom 1 ) in the last step.

Lemma 4 . 8 .

 48 For all e ≤ f ∈ kat, we have that KA atom r(e) ≤ r(f ).

ααn l α∈At α m = l α∈At α m ⊆ st κ 3 (

 3 KA atom r(⊥) = α|=⊥ α = 0 = r(0) -= 1: we deriveKA atom r( ) = α|= α = α∈At α = 1 = r(1)(using Lemma 4.7 for the last but one step)φ ∧ ψ = φ • ψ: we derive KA atom r(φ • ψ) = r(φ) • r(ψ) = r(φ ∧ ψ) φ ∨ ψ = φ + ψ: we derive KA atom r(φ + ψ) = r(φ) + r(ψ) = r(φ ∨ ψ)1. l = uα n l and v = l m. In this case we have uα cl contr (L)) By repeatedly applying the induction hypothesis we obtain that uαl α∈At α m ⊆ cl 3 • cl contr (L) Via definition of cl 3 this leads to {uαl m} = uαl 1 m ⊆ cl 3 • cl contr (L).

  [START_REF] Boffa | Une remarque sur les systèmes complets d'identités rationnelles[END_REF]. u = lu and m = u ααv. This case is symmetrical to case 1.Lemma D.3. cl contr • cl 3 ⊆ cl 3 • cl contr Proof. By Lemma 3.12 it is sufficient to prove that st contr • cl 3 ⊆ cl 3 • cl contr .Even though contr satisfies the conditions of Lemma 3.13, proving the necessary implication needed in that lemma turned out to be more difficult. Hence, we prove the necessary implication of Lemma 3.12 instead. In order to prove st contr• cl 3 ⊆ cl 3 • cl contr it is sufficient to show that st contr • cl 3 • cl contr (L) ⊆ cl 3 • cl contr (L).For a word w ∈ st contr •cl 3 •cl contr (L), we know that w ∈ u α v for some u, v ∈ (Σ+T BA ) * and u αα v ⊆ cl 3 • cl contr (L). Via Lemma D.2, we can immediately conclude that w = uαv ∈ cl 3 • cl contr (L).

4 :-(Lemma 6 . 4 .

 464 The remaining overlap is handled symmetrically.i = 1, j = 3. There is an overlap when u = rγ, which is solved as follows, using stThe other overlap is handled symmetrically. i = 1, j = 4. There is an overlap when u = rγ, which is solved as follows, in st 4 st 1 :r(γ ∪ α ∪ β)w rγ(α ∪ β)wThe other overlap is handled symmetrically. i = 2, j = 3. The only overlap is when u = r, which is solved as follows, in st i = 2, j = 4. The only overlap is when u = r, which is solved as follows, in st 2 Assuming γ ∪ δ = α ∪ β to obtain the horizontal st 2 reduction and then justifying the other st 2 reduction.) i = 3, j = 4. There cannot be an overlap in this case. We have cl 1,2,3,4 = cl 4 • cl 3 • cl 2 • cl 1 = cl 4 • cl 2,3 • cl 1 .

  r a reduction (item 1))An important case is when H = ∅: given a reduction from H to ∅, Theorem 3.2 gives completeness of KA H , by completeness of KA. Such reductions are what we ultimately aim for. However, in the examples later in this paper, these reductions are composed of smaller ones, which do make use of intermediate hypotheses. Section 3.2 contains general techniques for combining reductions.

  Lemma 3.7. Let H 1 , H 2 and H 3 be sets of hypotheses. If H 1 reduces to H 2 and H 2 reduces to H 3 then H 1 reduces to H 3 . Equiderivable sets of hypotheses always reduce to each other, via the identity: Lemma 3.8. Let H 1 , H 2 be sets of hypotheses over a common alphabet. If KA H1 H 2 and KA H2 H 1 then H 1 and H 2 reduce to each other.

  r 1 is a reduction, and r 2 is a reduction, respectively. Lemma 3.8. Let H 1 , H 2 be sets of hypotheses over a common alphabet. If KA H1 H 2 and KA H2 H 1 then H 1 and H 2 reduce to each other.Proof. The identity map on terms fulfills the requirements; in particular, we have cl 1 ( e ) = cl 2 ( e ) for all e by Lemma 2.4. Lemma 3.9. Let H 1 , . . . , H n , H be sets of hypotheses over a common alphabet Σ, with n ≥ 1. If H i reduces to H for all i, and cl 1...n = cl n • • • • • cl 1 , then i≤n H i reduces to H.Proof. Since KA Hi e ≤ f for each i and e ≤ f ∈ H, and there is at least one such H i , we have KA

i≤n Hi

  r k+1 is a reduction) using in the second step that cl H ⊆ cl k+1 , since KA H k+1 H (Lemma 2.4) and thus cl k+1 • cl H ⊆ cl k+1 • cl k+1 = cl k+1 (the converse inclusion cl k+1 ⊆ cl k+1 • cl H holds by definition of closure). This concludes the inductive proof. As a consequence, we have cl 1...n ( e ) = cl n • • • • • cl 1 ( e ) = r n • . . . • r 1 (e) as needed. Lemma 3.10. Let H 1 , . . . , H n be sets of hypotheses, such that cl

This version contains the appendix with the proofs. This work has been supported by the ERC (CoVeCe, grant No 678157) and by the LABEX MILYON (ANR-10-LABX-0070), within the program ANR-11-IDEX-0007.

Proof. We first prove by transfinite induction on α that for all languages L,

For the successor case, α + 1, we get

For the limit case, λ, we get

This concludes the proof of ( †). Then, for every language L, we have:

, and we conclude with Lemma 3.12.

Lemma B.2. Let H 1 = {e ≤ 0} for some term e and let H 2 be an arbitrary set of hypotheses. Then

Proof. By Lemma 3.12, it suffices to show that

φ = ψ, an instance of a Boolean algebra axiom: in this case, α |= φ iff α |= ψ for all α, so that r(φ) and r(ψ) are identical.

D Proofs for Section 5 (KAO)

Lemma 5.2. For all e ≤ f ∈ kao, we have KA contr r(e) ≤ r(f ).

Proof. Similar to the proof of Lemma 4.8. First observe that in that proof, we needed the hypotheses of kat only for the = 1 case, which is not there, and for the φ ∧ ψ = φ • ψ case, which is now only an inequation, and which is dealt with as follows:

We now prove the two parts of Lemma 5.5, in Lemma D.3 and Lemma D.1 below.

Take w ∈ st 2 • st 1 (L). So w = uαv for some atom α and words such that uv ∈ st 1 (L). This implies that uv = lβm for some words l, m and atom β and lββm ∈ L. From this we obtain that uv = lβm. By symmetry, we may assume that |u| ≤ |l|, i.e., l = ul , v = l βm for some word l . Then ul ββm ∈ L, so uαl ββm ∈ st = 2 (L) and subsequently uαl βm

For the commutativity of contr and atom 3 we need an auxiliary lemma.

Proof. We show that for all ordinals κ, for all natural numbers n ≥ 1 we have that

by transfinite induction on κ. For the base case, we just have the inclusion cl contr (L) ⊆ cl 3 • cl contr (L), and the limit case is trivial.

For the inductive step, assume it holds for some ordinal κ and let uα n v ∈ st 3 (st κ 3 (cl contr (L))). That means uα n v = lm for some l, m such that l α∈At α m ⊆ st κ 3 (cl contr (L)). We distinguish three cases.

α • β ≤ α ∪ β (2): we have to prove r(α) • r(β) ≤ r(α ∪ β) in KA 3 . By distributivity, this amounts to proving α 1 . . . α n β 1 . . . β m ≤ r(α ∪ β) for all sequences of pairwise distinct atoms α 1 , . . . , α n and β 1 , . . . , β m whose unions are α and β, respectively. The sequence α 1 , . . . , α n , β 1 , . . . , β m almost yields a term in r(α ∪ β): its union is α ∪ β, but it may contain duplicate entries.

We simply remove such duplicates using inequations in 3 (γ ≤ 1). α ≤ 1 (3): we have to show r(α) ≤ 1 in KA 3 . This follows by repeated applications of inequations in 3: all terms of the sum r(α) are below the identity.

Let us recall the five sets of hypotheses used for atom :

= {1 ≤ ∅} (for KAPT with , with ∅ being the atom interpreted as ).

Lemma 6.3. We have the following inclusions of functions:

Proof. A word in st i (st j (L)) has shape rs t with rst = uv w such that uvw ∈ L, where u, v, v , w, r, s, s , t are words with v ≤ v an inequation of j and s ≤ s an inequation of i. We depict this situation as follows:

In each case we have to consider how the equation rst = uv w was obtained.

When |rs| ≤ |u| or |st| ≤ |w|, we immediately get rs t ∈ st j (st i (L)): the patterns do not overlap and may be triggered in any order. We only consider the other cases in the following.

There is an overlap when r = u, s = v , t = w in which case the two reductions cancel each other:

In this case we simply have rs t ∈ id(L).

Proof. We use Lemma 3.10 and Lemma 3.13 repeatedly, on (combinations of) the inclusions provided by Lemma 6.3. Note that all inequations considered here have a word as right-hand side, so that all functions st H considered here are additive by Lemma A.1.

The second equation follows from cl 2,3 = cl 3 cl 2 , which is a consequence of item (iv) (because st 3 st 2 + st 2 3 ⊆ cl 3 st = 2 ). For the first equation, we have cl 3,4 = cl 4 cl 3 as a consequence of item (vi), so that it suffices to prove cl 1,2,3,4 = cl 3,4 cl 2 cl 1 . This follows by using Lemma 3.10 on cl 1 , cl 2 , and cl 3,4 . Indeed, we have: Proof. Given Lemma 6.4, it suffices to show that cl 5 commutes over the four other closures.

-For i ∈ {2, 3, 4}, since the right-hand sides of the corresponding inequations are words of length at most one, we easily get st i st 5 ⊆ st 5 st i , and hence cl i cl 5 ⊆ cl 5 cl i by Lemma 3.13. -For 1, we use the fact that a word belongs to cl 5 (L) iff it is obtained from a word of L by removing an arbitrary number of occurrences of ∅ (i.e., the atom denoting ), and we prove directly st 1 cl 5 ⊆ cl 5 cl 1 . Indeed a word w belongs to st 1 (cl 5 (L)) if w = u(α ∪ β)v for some u, u , v, v , α, β, n such that u α∅ n βv ∈ L and u (resp. v) is obtained from u (resp. v ) by removing some occurrences of . We deduce u (α ∪ β)v ∈ cl 1 (L) by using st 1 n + 1 times, and thus w ∈ cl 5 (cl 1 (L)) by removing the remaining additional occurrences of ∅. We finally deduce cl 1 cl 5 ⊆ cl 5 cl 1 with Lemma 3.12.