Stefan Hetzl
email: stefan.hetzl@pps.jussieu.fr

Proofs as Tree Languages

In this work a new connection between proof theory and formal language theory is established. Cut-elimination in a class of first-order proofs is characterised by a class of tree languages in the following sense: the proof with cuts corresponds to a formal grammar, the cut-free proof to the language of the grammar and the process of cut-elimination to the computation of the language from the grammar. It is shown how to read off a grammar from a proof and vice versa how to construct a proof from a grammar such that this correspondence holds.

Introduction

Cut-elimination is one of the central techniques of proof theory. The cut-elimination theorem has first been proved for classical and intuitionistic first-order logic by Gentzen in his seminal work [START_REF] Gentzen | Untersuchungen über das logische Schließen[END_REF] where also the sequent calculus has been introduced. Since then, it has been generalised to many logics and calculi. The importance of cut-elimination for computational logic has various roots: via the Curry-Howard correspondence, cut-elimination and the related technique of normalisation correspond to the evaluation of terms in functional programming languages. In formalised mathematical proofs, the elimination of cuts has the effect of removing lemmas yielding constructive information about the theorem such as witnesses or bounds. Furthermore, a cut-elimination theorem for a logic has the cut-free completeness as a corollary which typically allows for efficient proof search procedures.

Formal language theory plays an important role in computer science with applications in various domains ranging from the specification of data formats to computer-aided verification. Traditionally, a formal language is defined to be a set of words. This notion can be generalised to considering a formal language to be a set of trees. Such tree languages posses a rich theory and many applications, see e.g. [START_REF] Comon | Tree Automata: Techniques and Applications[END_REF]. One particular application that has received considerable attention recently is the use of tree grammars for the compression of XML documents, see [START_REF] Sakr | XML compression techniques: A survey and comparison[END_REF] for a survey.

The purpose of this paper is to develop a new connection between these two subjects. The basis for this connection is the following relation between cut-free proofs and tree languages: Herbrand's theorem, in its most simple version, states that a formula ∃x A with A quantifier-free is valid iff there are terms t 1 , . . . , t n s.t. n i=1 A[x\t i ] is a propositional tautology. Such a disjunction of instances which is a tautology is called Herbrand-disjunction. It is quite straightforward to observe that from a cut-free proof it is easy to read off an Herbrand-disjunction and vice versa, how to construct a cut-free proof from an Herbrand-disjunction. Furthermore, different proofs may have the same Herbrand-disjunctions, so "having the same Herbrand-disjunction" is an equivalence relation on the set of cut-free proofs of a theorem. Moreover, this equivalence relation is natural as all the information of a proof which is mathematically interesting (in the sense of proof analyses such as [START_REF] Kreisel | Finiteness theorems in arithmetic: An application of Herbrand's theorem for Σ 2 -formulas[END_REF][START_REF] Luckhardt | Herbrand-Analysen zweier Beweise des Satzes von Roth: Polynomiale Anzahlschranken[END_REF], see also [START_REF] Kohlenbach | Applied Proof Theory: Proof Interpretations and their Use in Mathematics[END_REF]) is contained in its Herbrand-disjunction. An instance A[x\t i ] is quantifier-free and hence without binding constructs. Therefore it can be regarded as a tree over the signature compromising in addition to the first-order signature also the propositional connectives. Identifying an Herbrand-disjunction n i=1 A[x\t i ] with the set of instances {A[x\t i ] | 1 ≤ i ≤ n} shows that an Herbrand-disjunction, and therefore a natural equivalence class of cut-free proofs, is nothing but a finite tree language. Note that Herbrand-disjunctions as well as this line of reasoning can be generalised to cover more complicated quantifier-prefixes, non-prenex formulas as well as full higher-order logic by using e.g. the expansion trees of [START_REF] Miller | A Compact Representation of Proofs[END_REF].

In this paper, we will extend this connection to the class of proofs whose cuts are restricted to containing at most one quantifier each. While this is a significant restriction of the expressive power of the cuts, a natural extension to full first-order logic is suggested in the conclusion. We will show that a proof with such cuts corresponds to (and asymptotically has the same length size as) a tree grammar and that the language of this grammar is an Herbrand-disjunction. Consequently, cut-elimination corresponds to the computation of the language of such a grammar. It will turn out that the suitable kind of tree languages are rigid tree languages, a notion that has been introduced in [START_REF] Jacquemard | Rigid tree automata[END_REF][START_REF] Jacquemard | Rigid tree automata and applications[END_REF] for the purpose of verification of cryptographic protocols. Furthermore, we will describe a class of rigid tree grammars which corresponds exactly to the considered class of proofs in the sense that also a translation in the other direction, i.e. from grammars to proofs, is possible. Hence these results show that the combinatorial mechanism underlying the compression power of cuts is that of a particular kind of tree grammar. This uncovers a certainly unexpected similarity between cut-elimination and techniques used for XML compression.

In Section 2 we will develop rigid tree grammars and prove them equivalent to the rigid tree automata of [START_REF] Jacquemard | Rigid tree automata[END_REF][START_REF] Jacquemard | Rigid tree automata and applications[END_REF] as well as make several useful observations about these languages. Section 3 contains the proof-theoretic preliminaries leading to the definition of the grammar of a proof. Sections 4 and 5 are devoted to proving the main result of this paper: the language of the grammar of a proof is an Herbrand-disjunction. In Section 6 we show how to translate grammars into proofs.

Rigid Tree Languages

Tree languages are a natural generalisation of string languages to the case of trees and constitute a central notion in the theory of formal languages [START_REF] Gécseg | Tree Languages[END_REF][START_REF] Comon | Tree Automata: Techniques and Applications[END_REF]. A feature which is important for applications but not present in regular tree languages is the ability to carry out equality tests between subterms, for instance to recognise patterns of the form f (x, x). There are several classes of tree automata providing this ability: some allow to specify local equality constraints as side conditions of transition rules by giving term positions explicitly, see [START_REF] Comon | Tree Automata: Techniques and Applications[END_REF] for a survey, while others consider global constraints specified via states. An important class of the latter kind are tree automata with global equalities and disequalities (TAGED) [START_REF] Filiot | Satsifiability of a Spatial Logic with Tree Variables[END_REF][START_REF] Filiot | Tree Automata with Global Constraints[END_REF][START_REF] Filiot | Tree Automata With Global Constraints[END_REF]. For our purposes it will turn out to be natural to work with rigid tree automata (RTA) that have been introduced in [START_REF] Jacquemard | Rigid tree automata[END_REF][START_REF] Jacquemard | Rigid tree automata and applications[END_REF] and are a subclass of TAGED (characterised by having minimal equality and disequality relations). In a rigid tree automaton, certain states are designated as rigid thus demanding that only one term may appear on the different positions of this state. Definition 1. A tree automaton on a signature Σ is a tuple Q, F, ∆ where Q is a finite set of state symbols, F ⊂ Q is the set of final states and ∆ a set of transition rules of the form: f (q 1 , . . . , q n ) → q where f ∈ Σ and q, q 1 , . . . , q n ∈ Q.

A rigid tree automaton on Σ is a tuple Q, R, F, ∆ where Q, F, ∆ is a tree automaton and R ⊆ Q is the set of rigid states.

As usual a position is a list of natural numbers, Pos(t) is the set of positions of the term t, ε is the empty (root) position and concatenation of positions p 1 and p 2 is written as p 1 .p 2 . We write Pos(x, t) for the set of positions of the symbol x in t and we write x ∈ t if Pos(x, t) = ∅. A run of a tree automaton on a term t is a function r : Pos(t) → Q s.t. for all f ∈ Σ and all p ∈ Pos(f, t): f (r(p.1), . . . , r(p.n)) → r(p) ∈ ∆ for all p ∈ Pos(t). A run of a rigid tree automaton on t is a run of the underlying tree automaton satisfying the additional rigidity condition: for all p 1 , p 2 ∈ Pos(t): if r(p 1 ) = r(p 2 ) ∈ R then t| p 1 = t| p 2 . T (Σ) denotes the set of ground terms over a signature Σ. The language of an automaton A in a state q is denoted as L(A, q) and defined as the set of t ∈ T (Σ) s.t. there exists a run r on t with r(ε) = q. The language of A is defined as L(A) = q∈F L(A, q). Example 1. Let Σ = {0/0, s/1}. A simple pumping argument shows that the language L = {f (t, t) | t ∈ T (Σ)} is not regular. On the other hand, L is recognised by the rigid tree automaton Q, R, F, ∆ where Q = {q, q r , q f }, R = {q r }, F = {q f } and ∆ = {0 → q, 0 → q r , s(q) → q, s(q) → q r , f (q r , q r ) → q f }.

Our goal in this paper is the description of the computation of an Herbrand-disjunction during the process of cut-elimination. For this aim it is considerably more natural (and technically advantageous) to adopt the generative viewpoint of a grammar on a language. We will therefore first develop rigid tree grammars and prove them to be equivalent to the above rigid tree automata. Definition 2. A regular tree grammar is a tuple α, N, T, P composed of an axiom α, a set N of non-terminal symbols with arity 0 and α ∈ N , a set T of terminal symbols with T ∩ N = ∅ and a set P of production rules of the form β → t where β ∈ N and t ∈ T (T ∪ N ).

A rigid tree grammar is a tuple α, N, R, T, P where α, N, T, P is a regular tree grammar and R ⊆ N is the set of rigid non-terminal symbols.

The derivation relation → G of a regular tree grammar G is defined for s, t ∈ T (T ∪N ) as s → G t if there is a production rule β → u and a position p s.t. s| p = β and t is obtained from s by replacing β at p by u. A derivation of a term t ∈ T (T ) in a regular tree grammar is a list of terms t 1 , . . . , t n ∈ T (T ∪ N ) s.t. t 1 = α, t n = t and t i → G t i+1 for i = 1, . . . , n -1. A derivation of t in a rigid tree grammar is a derivation in the underlying regular tree grammar satisfying the additional rigidity condition: if t i → G t i+1 and t j → G t j+1 are applications of productions rules at positions p i , p j with the same left-hand side β ∈ R, then t| p i = t| p j . We will often omit the subscript G of the arrow if the grammar is clear from the context. The language of a tree grammar L(G) is the set of t ∈ T (T ) that are derivable in G. A production whose left-hand side is β will often be called β-production. A first basic but useful observation about rigid tree grammars is the following Lemma 1. Let G = α, N, R, T, P be a rigid tree grammar and let t ∈ L(G). Then there is a derivation α → • • • → t which uses at most one β-production for each β ∈ R.

Proof. Suppose both β → s 1 and β → s 2 are used at positions p 1 an p 2 respectively. Then by the rigidity condition t| p 1 = t| p 2 and we can replace the derivation at p 2 by that at p 1 (or the other way round). This transformation does not violate the rigidity condition because it only copies existing parts of the derivation.

It is a well-known result that regular tree grammars and tree automata are equivalent in the sense that they describe the same class of tree languages. We will now show the analogous result for the rigid versions. The proof essentially follows the lines of that in [START_REF] Comon | Tree Automata: Techniques and Applications[END_REF] for the regular case, however it is more involved due to the necessity of respecting the rigidity condition. Definition 3. A grammar is called normalised if every production rule has the form γ → a or γ → f (γ 1 , . . . , γ n ) for a, f ∈ T and γ, γ 1 , . . . , γ n ∈ N .

For a term t, P ⊆ Pos(t) and a substitution σ we write t • P σ for the term obtained from application of σ to the subterms of t at the positions in P .

Lemma 2. If G is a rigid tree grammar, then there is a normalised rigid tree grammar G * s.t.

L(G) = L(G * ).
Proof. Let G be a rigid tree grammar which is not normalised. W.l.o.g. G has a rigid axiom α which does not appear on the right-hand side of any production and G does not contain productions of the form β → β. Let β → f (t 1 , . . . , t n ) be a production rule where at least one t i is not a non-terminal symbol. Define a new rigid tree grammar G ′ by adding new non-rigid non-terminal symbols β 1 , . . . , β n and replacing the production rule

β → f (t 1 , . . . , t n ) by β → f (β 1 , . . . , β n ), β 1 → t 1 , . . . , β n → t n .
Then every G-derivation can obviously be transformed to a G ′ -deviation preserving rigidity. Derivations can also be transformed in the other direction: let

α = t 0 → G ′ • • • → G ′ t n = t.
As t does not contain β i , for every application of β → f (β 1 , . . . , β n ) at a position p there must be an application of β i → t i at p.i later in the derivation. On the other hand, as β i is a new symbol every application of β i → t i at p.i must be preceded by an application of β → f (β 1 , . . . , β n ). By permuting independent derivation steps one can join the corresponding rule applications thus collapsing a G ′ -derivation to a G-derivation -againpreserving rigidity. By iterating this process one eventually obtains a rigid tree grammar whose only non-normalised production rules are of the form β → γ for non-terminals β, γ. The rest of this proof will be concerned with the removal of these production rules, distinguishing cases based on rigidity of β and γ. Let the weight of a grammar w(G) be defined as the sum of the lengths of all possible derivations of the form

β 1 → • • • → β k where β i ∈ N and β i = β j for i = j.
Let G = α, N, R, T, P be a rigid tree grammar and β → γ a production with γ non-rigid, let γ → s 1 , . . . , γ → s k be all γ-productions and define G ′ = α, N, R, T, P ′ where

P ′ = (P \ {β → γ}) ∪ {β → s i | 1 ≤ i ≤ k, s i = β}. Let α = t 0 → G • • • → G t n = t. If β → γ
is applied at some position p ∈ Pos(t), there must be an application of one of the γ → s i at position p later and by permuting independent steps we can collapse β → γ → s i to β → s i to obtain a G ′ -derivation of t. If some δ ∈ R is used at a certain position in this G ′ -derivation then it is used at the same position in the G-derivation so the rigidity condition is preserved. To obtain a G-derivation from a G ′ -derivation we replace applications of β → s i by β → γ → s i . The rigidity condition is preserved as γ is not rigid, hence L(G) = L(G ′ ). Every derivation β 1 → • • • → β k with β i ∈ N and β i = β j for i = j in G ′ has a corresponding (and longer) one in G obtained from replacing β → s i by β → γ → s i but β → γ does no longer exist in G ′ so w(G ′ ) < w(G).

If β → γ is a production rule where β is non-rigid let α 1 → s 1 , . . . , α k → s k be all productions that contain β on their right-hand side and define G ′ by changing the productions P to

P ′ = (P \ {β → γ}) ∪ {α i → s i • P [β\γ] | 1 ≤ i ≤ k, P ⊆ Pos(β, s i ), s i • P [β\γ] = α i }. Let α = t 0 → • • • → t n = t be a G-derivation. If β → γ
is applied at a position p then (as β = α because β is non-rigid) a production α i → s i at or above p is applied before it in the G-derivation. After permutation of independent steps, replace applications of α i → s i and all applications of β → γ to this copy of s i by an application of α i → s i • P [β\γ] to obtain a G ′ -derivation. If a non-terminal δ is used at a certain position in the G ′ -derivation it is used at the same position in the G-derivation so the rigidity condition transfers. For the other direction one obtains a G-derivation from a G ′ -derivation from replacing α i → s i • P [β\γ] by α i → s i followed by copies of β → γ. Now if δ ∈ R is used at a certain position in the G-derivation then δ = β by assumption so δ is used at the same position in the G ′ -derivation and rigidity transfers. As above it is easy to check that w(G ′ ) < w(G).

These transformations decrease the weight, so we eventually arrive at a grammar G all of whose non-normalised productions are of the form β → γ for both β, γ rigid; let

{β i → γ i | 1 ≤ i ≤ m} be these productions. If α = t 0 → • • • → t n = t
is a G-derivation using β → γ then by Lemma 1 we can assume that it uses β → γ on all β-positions; let {p 1 , . . . , p n } be the set of β-positions of this derivation. The set M ⊆ {1, . . . , m} of indices of the β i → γ i used in the derivation is non-branching in the sense that it does not contain i, j with β i = β j but γ i = γ j . Furthermore it is also acyclic in the sense that there are no i 1 , . . . , i k ∈ M s.t. γ i j = β i j+1 for j ∈ {1, . . . , k -1} and γ i k = β i 1 because cycles can trivially be eliminated.

For such a non-branching and acyclic M denote with β * the image of the non-terminal β under exhaustive application of the productions {β i → γ i | i ∈ M }. This image is well-defined (by M being acyclic) and unique (by M being non-branching). Define G M = α, N ′ , R ′ , T, P ′ by

N ′ = N \ {β i | i ∈ M }, R ′ = N ′ ∩
R, and

P ′ = (P \ {β i → γ i | 1 ≤ i ≤ m})[β i \β * i ] i∈M .
Let α = t 0 → • • • → t n = t be a G-derivation and M its acyclic and non-branching index set, then we obtain a G M -derivation from replacing β i by β * i everywhere hence removing the applications of the β i → γ i . The rigidity condition is still fulfilled as using some δ ∈ R at a position in the G M -derivation implies that it is used at the same position in the G-derivation. For the other direction, we translate a G M -derivation to a G-derivation by inserting β i → γ iapplications. The rigidity condition for the β i is fulfilled because they are newly introduced at only the positions of the rigid β * i which ensure equality of the subterms at these positions. Define G ′ as disjoint union of the G M for all acyclic and non-branching M joined by a single axiom. Then G ′ is normalised and L(G ′ ) = L(G). Theorem 1. A set of terms is language of a rigid tree grammar iff it is language of a rigid tree automaton.

Proof. It is straightforward to translate between normalised rigid tree grammars and rigid tree automata by reversing the direction of the arrows, translating non-terminal symbols as states and the axiom as final state. The result then follows from Lemma 2. Definition 4. A rigid tree grammar α, N, R, T, P is called totally rigid if N = R.

Totally rigid tree grammars will simply be written as α, R, T, P . If G = α, R, T, P is totally rigid and t 0 = α → • • • → t n = t ∈ T (T ) is a derivation in G we can by Lemma 1 assume that for every non-terminal at most one production rule is applied. A set S of production rules induces an order < S on the non-terminals as transitive closure of α < S β if α → t ∈ S and β ∈ t. Given a derivation in G, the order induced by its set S of production rules is acyclic. For suppose it would be cyclic, then either because it permits a derivation α → • • • → α which can be removed or because one of the form α → • • • → s where α = s but α ∈ s. But in this case the derivation cannot finish with a term built from terminals only due to the rigidity of α.

So while every single derivation induces an acyclic order, this is not necessarily the case for the whole set of productions of a grammar as can be seen in the simple example

α → h(β)|h(γ), β → f (γ)|a, γ → g(β)|b by deriving h(f (b)) and h(g(a)).
Definition 5. A grammar is called acyclic if the order induced by the set of its productions is.

So an acyclic totally rigid grammar is a totally rigid grammar with a uniform order. Such grammars are central for this paper. They allow the following simple description of their language in terms of substitutions: Lemma 3. If G is totally rigid and acyclic, then up to renaming of the non-terminals

G = α 0 , {α 0 , . . . , α n }, T, P with L(G) = {α 0 [α 0 \t 0 ] • • • [α n \t n ] | α i → t i ∈ P }.
Proof. Acyclicity permits a renaming of non-terminals s.t. α i > P α j implies i > j. The rightto-left inclusion is obvious. For the left-to-right inclusion, let α 0 = s 0 → . . . → s n = s ∈ T (T ) be a derivation in G. By Lemma 1 we can assume that for each i at most one production whose left-hand side is α i is applied, say α i → t i . By acyclicity we can rearrange the derivation so that α i → t i is only applied after α j → t j if i > j. For those α i which do not appear in the derivation we can insert any substitution without changing the final term so we obtain

s = α 0 [α 0 \t 0 ] • • • [α n \t n ].
We finish this section on tree languages with basic observations that will be useful later on.

Lemma 4. If a rigid tree grammar G ′ is obtained from another rigid tree grammar G by deletion of production rules, then L(G ′ ) ⊆ L(G).

Proof. Every G ′ -derivation is a G-derivation.

Lemma 5. If a rigid tree grammar G ′ is obtained from another rigid tree grammar G by identifying two rigid non-terminals, then L(G ′ ) ⊆ L(G).

Proof. Let β and γ be two non-terminals in G and call (βγ) the new non-terminal in G ′ which replaces all occurrences of both β and γ. Let α → • • • → t be a G ′ -derivation then by Lemma 1 we can assume that only one (βγ)-rule is used in it, say (βγ) → s. If s = (βγ) we obtain a G-derivation by dropping all applications of (βγ) → (βγ). If s = (βγ), then (βγ) / ∈ s as (βγ) ∈ s would contradict rigidity. Then either β → s or γ → s must be a production in G so α → • • • → t can be transformed to a derivation in G. Lemma 6. Let G = α, N, R, T, P be a rigid tree grammar,

β ∈ R, β → t 1 , . . . , β → t n ∈ P , γ / ∈ N and G ′ = α, N ∪ {γ}, R ∪ {γ}, T, P ′ where P ′ = (P \ {β → t 1 , . . . , β → t n }) ∪ {β → γ, γ → t 1 , . . . , γ → t n }. Then L(G) = L(G ′ ).
Proof. Let t ∈ L(G) then by Lemma 1 there is a G-derivation α → • • • → t which uses at most one β-production. If it does not use a β-production at all, then t ∈ L(G ′ ), so assume it uses β → s as only β-production. If s ∈ {t 1 , . . . , t n }, obtain a G ′ -derivation by replacing all applications of β → s by β → γ → s. The rigidity of γ in the G ′ -derivation follows from γ / ∈ N and the rigidity of β in the G-derivation. For the other direction, let t ∈ L(G ′ ), then by Lemma 1 there is a G ′ -derivation α → • • • → t which uses at most one γ-production. If it does not use a γ-production, then t ∈ L(G), so assume it uses γ → t i . As γ is only introduced by β → γ we can permute independent steps and collapse β → γ → t i to β → t i thereby obtaining a G-derivation which satisfies the rigidity condition.

Γ → ∆, A A, Π → Λ Γ, Π → ∆, Λ cut
The quantifier rules are subject to the usual conditions: The regularity of a proof is a useful and harmless assumption in the context of cut-elimination. Also the second condition does not present a severe restriction; it is a standard result that strong quantifiers can be removed from formulas and proofs by Skolemisation. Prenexifying and possibly moving the formulas to the left then yields an end-sequent as demanded. The only of the above restrictions that substantially decreases the scope of the present analysis and justifies the terminology "simple" is the third one concerning the use of quantifiers in cuts.

The results in this paper can be extended to a slightly more general class of proofs where the existential prefix in the end-sequent is a block of quantifiers and also cut-formulas are allowed to contain an arbitrary number of quantifiers as long they do not contain both a strong and a weak quantifier. The class of simple proofs has been chosen here for expositional clarity.

Definition 8. Let π be a simple proof of Γ → ∃x A and ψ a subproof of π. The Herbrand-set

H(ψ, π) of ψ w.r.t. π is defined as follows. If ψ is an axiom, then H(ψ, π) = ∅. If ψ is of the form (ψ ′ ) Π → Λ, A[x\t] Π → Λ, ∃x A ∃ r
where the main formula ∃x A is ancestor of the formula ∃x A in the end-sequent, then

H(ψ, π) = H(ψ ′ , π) ∪ {A[x\t]}.
If ψ ends with any other unary inference and ψ ′ is its immediate subproof then H(ψ, π) = H(ψ ′ , π). If ψ ends with a binary rule and ψ 1 , ψ 2 are its immediate subproofs, then H(ψ, π) = H(ψ 1 , π) ∪ H(ψ 2 , π). We write H(π) for H(π, π).

Example 2. Define the axioms

A 1 = P (a) ∨ P (b), A 2 = ∀x (P (x) ⊃ Q(f (x))) and A 3 = ∀x∀y (P (x) ⊃ Q(y) ⊃ R(g(x, y))) and the simple proof π = (π 1 ) A 1 → P (a), P (b) A 1 → ∃xP (x), P (b) ∃ r A 1 → ∃xP (x), ∃xP (x) ∃ r A 1 → ∃xP (x) c r (π 2 ) P (α), A 2 → Q(f (α)) P (α), A 2 → ∃xQ(x) ∃ r (π 3 ) P (α), Q(β), A 3 → R(g(α, β)) P (α), Q(β), A 3 → ∃xR(x) ∃ r P (α), ∃xQ(x), A 3 → ∃xR(x) ∃ l P (α), A 2 , A 3 → ∃xR(x) c l , cut ∃xP (x), A 2 , A 3 → ∃xR(x) ∃ l A 1 , A 2 , A 3 → ∃xR(x) cut
where π 1 , π 2 and π 3 are the obvious cut-free proofs. Then H(π) = {R(g(α, β))}.

Definition 9. Let π be a proof and Q be a quantifier occurrence in π. Define a set of terms t(Q) associated with Q as follows: if Q occurs in the main formula of a weakening, then t(Q) = ∅. If Q is introduced by a quantifier inference from a term t or a variable x, then t(Q) = {t} or t(Q) = {x} respectively. If Q occurs in the main formula of a contraction and Q 1 , Q 2 are the two corresponding quantifiers in the auxiliary formulas of the contraction, then t(Q

) = t(Q 1 )∪t(Q 2 ).
In all other cases Q has exactly one immediate ancestor

Q ′ and t(Q) = t(Q ′ ).
Let π be a simple proof and c be a cut in π that contains a quantifier. Write Q c for the strong occurrence of the quantifier in one cut-formula of c and Q ′ c for the corresponding weak occurrence in the other cut-formula. For C being the set of cuts in π which contain a quantifier, define the base substitutions of π as B(π where Σ(π) is the signature of the proof π.

) := c∈C {[α\t] | α ∈ t(Q c ), t ∈ t(Q ′ c )}. Example 3. The proof π of Example 2 has B(π) = {[α\a], [α\b], [β\f (α)]}.
P = {ϕ → F | F ∈ H(π)} ∪ {α → t | [α\t] ∈ B(π)}. a b α f (α) β R(g(α, β)) ϕ j j V V V V V V V V V V V V V V V V V V V V V : : t t
Let |G| be the number of production rules of the grammar G and |π| be the number of inferences in a proof π. From the above definition, it is easy to show that |G| ≤ |π| 2 . We will later (in Lemma 11) Proof. By induction on the number of cuts in the proof. The grammar of a cut-free proof is trivially acyclic. For the induction step, let ι be the lowest binary inference with subproofs π 1 and π 2 s.t. either 1. ι is a cut or 2. ι is not a cut but both π 1 and π 2 contain a cut. Let P 1 be the productions induced by the cuts in π 1 , P 2 that induced by the cuts in π 2 and P that induced by cuts in π. In case 2, < P = < P 1 ∪ < P 2 which is acyclic by induction hypothesis. In case 1, let P ι be the productions induced by the cut ι, then

construct a G ′ with |G ′ | ≤ |π|.
< 1 P = < 1 P 1 ∪ < 1 P 2 ∪ < 1
Pι . By induction hypothesis, < P 1 and < P 2 are acyclic and as ι contains at most one quantifier, also < Pι is acyclic. Therefore, a cycle in < P must be of the form

α 1 ≤ P 1 β 1 < Pι α 2 ≤ P 2 β 2 < Pι α 1
where α 1 , β 1 are eigenvariables of strong quantifier inferences in π 1 and α 2 , β 2 of inferences in π 2 . However, ι contains only one quantifier and depending on its polarity all substitutions in B(ι) lead from π 1 to π 2 or from π 2 to π 1 but not both, so < P is acyclic.

Some Algebraic Preliminaries

Before proving the main result, it will be useful to make some simple but rather abstract observations. We will work in a structure (U, < 1 , ∼) where < 1 is a binary relation on U and ∼ is an equivalence relation on U . The results of this section will only be applied to the situation U = B(π), < 1 being the one step scope order of Definition 13 and [α\t] ∼ [β\s] iff α = β. The author has found it useful to think about such structures in terms of diagrams such as the one depicted in Figure 1.

We use letters X, Y, . . . for subsets of U , letters X, X 1 , . . . for subsets of the power set of U and the letters C, D, . . . for ∼-classes. We write x < X y if there are x 1 = x, x 2 , . . . , x n = y ∈ X with x i < 1 x i+1 for 1 ≤ i < n. We write x < y for x < U y. For X ⊆ U define X ↑ x = {y ∈ X | x < X y} which for the case x / ∈ X entails X ↑ x = ∅. For X ⊆ U define X * = {Y ⊆ X | for every C ∈ X /∼ there is exactly one x ∈ C ∩ Y } which entails ∅ * = {∅}. For a set X of subsets of U we define X ↑ x := {X ↑ x | x ∈ X ∈ X}. We will often use sets of the form

X * ↑ x = {X 0 ↑ x | x ∈ X 0 ∈ X * }. Example 5. Let U = {[α\a], [α\b], [β\f (α)]} = B(π)
* ↑ β = {{[β\f (α)], [α\a]}, {[β\f (α)], [α\b]}}. Lemma 8 (Monotonicity). If X 1 ⊆ X 2 , then X 1 ↑ x ⊆ X 2 ↑ x.
Proof. If y ∈ X 1 ↑ x then there are x 1 = x, . . . , x n = y ∈ X 1 with x i < 1 x i+1 and the x i also being in

X 2 we have y ∈ X 2 ↑ x. X and Y are called class-disjoint if for every C ∈ U /∼ we have X ∩ C = ∅ or Y ∩ C = ∅. Lemma 9 (Context). If X, Y are class-disjoint and x ∈ X with (X ∪ Y ) ↑ x = X ↑ x then (X ∪ Y ) * ↑ x = X * ↑ x.
Proof. First note that due to class-disjointness we have

(X ∪ Y ) * ↑ x = {(X 0 ∪ Y 0 ) ↑ x | x ∈ X 0 ∪ Y 0 , X 0 ∈ X * , Y 0 ∈ Y * } but (X ∪ Y ) ↑ x = X ↑ x implies (X 0 ∪ Y 0 ) ↑ x = X 0 ↑ x for all X 0 ⊆ X, Y 0 ⊆ Y and therefore = {X 0 ↑ x | x ∈ X 0 ∈ X * } = X * ↑ x. For X, Y ⊆ U we write Y < 1 X if there are x ∈ X, y ∈ Y s.t. y < 1 x and Y ≮ 1 X if this is not the case. For sets X, Y write X ↑ Y for y∈Y X ↑ y. Definition 11. Let X, Y ⊆ U , a class C ∈ Y /∼ is called entrance of Y for X if i) x < 1 z for all x ∈ X and all z ∈ C and ii) for all x ∈ X, y ∈ Y with x < X∪Y y there is a z ∈ C s.t. x < 1 z < Y y. Lemma 10 (Splitting). Let X, Y be class-disjoint with Y ≮ 1 X, let C ∈ Y /∼ be the entrance of Y for X and D ∈ X /∼, let X 0 ∈ X * and Y 0 ∈ Y * , then (X 0 ∪ Y 0 ) ↑ D = X 0 ↑ D ∪ Y 0 ↑ C. Proof. As D ∈ X /∼ and X 0 ∈ X * we have D ∩ X 0 = {x 0 } = D ∩ (X 0 ∪ Y 0 ) for some x 0 , so it suffices to show (X 0 ∪ Y 0 ) ↑ x 0 = X 0 ↑ x 0 ∪ Y 0 ↑ C. For the left-to-right inclusion let z ∈ (X 0 ∪Y 0 ) ↑ x 0 . If z ∈ X 0 then x 0 < X 0 z because Y ≮ 1 X so z ∈ X 0 ↑ x 0 . If z ∈ Y 0 then x < X 0 ∪Y 0 z implies z ∈ Y 0 ↑ C because C is entrance of Y for X.
For the other direction, let x ∈ X 0 ↑ x 0 , then x ∈ (X 0 ∪ Y 0 ) ↑ x 0 by monotonicity. For y ∈ Y 0 ↑ C we have z ∈ C with z < Y 0 y and as C is entrance of Y for X we obtain x 0 < 1 z < Y 0 y.

From Proofs to Tree Languages

The grammar of a proof is invariant under many proof transformations including most local cut-reduction rules. A notable exception are the duplications of proofs induced by the removal of contractions: such a transformation duplicates parts of the grammar. However -and this is the technical key point of this paper -this transformation can be done in a way which does not change the language of the grammar. To achieve this we will exercise a tight control over the removal of contractions by imposing an uppermost reduction strategy as well as a particular normal form for proofs (also for those containing cuts).

This normal form for simple proofs requires the cuts to be prenex. The transformation to prenex cuts will partially be the one used in [START_REF] Baaz | Cut Normal Forms and Proof Complexity[END_REF] on first-order proofs as well as by [START_REF] Morioka | Logical Approaches to the Complexity of Search Problems: Proof Complexity, Quantified Propositional Calculus and Bounded Arithmetic[END_REF]Theorem 5.13] in quantified propositional calculus, see also [START_REF] Cook | Logical Foundations of Proof Complexity[END_REF]Theorem VII.4.7]. In order to control the changes of the language of the grammar induced by this transformation we introduce a new dummy constant d which does not appear in the original proof and we write G nd (π) for G(π) without productions of the form β → d.

In a proof where all formulas are prenex and without quantifier alternations, a weak quantifier inference ι can be shifted downwards until either: it reaches the premise sequent of a cut or the end-sequent where the quantifier is introduced, or: it reaches the premise sequent of a strong quantifier inference whose eigenvariable appears in the term of ι. Such a sequent will be called blocking sequent for ι.

Definition 12. A proof π is said to be in normal form if the following conditions are fulfilled:

1. π is simple.

2. The dummy constant d appears only in a context of the form

Γ → ∆, A Γ → ∆, A ∨ B[x\d] ∨ r 1 Γ → ∆, ∃x (A ∨ B) ∃ r or Γ → ∆, A Γ → ∆, B[x\d] ∨ A ∨ r 2 Γ → ∆, ∃x (B ∨ A) ∃ r
where x / ∈ A and ∃x (A ∨ B) or ∃x (B ∨ A) respectively is ancestor of a cut-formula.

3. For every ∃ r -inference ι: the only inferences between ι and its blocking sequent are other ∃ r -inferences, contractions and ∨ r -inferences deleting d.

4. All cut-formulas are of the form ∃x A for some quantifier-free A and appear in a context of the form

(ψ 1 ) Γ → ∆, ∃x A (ψ 2 ) A[x\α], Π → Λ ∃x A, Π → Λ ∃ l Γ, Π → ∆, Λ cut
where ψ 1 contains at least one ∃ r -inference whose main formula is ancestor of ∃x A in the cut and two different such ∃ r -inferences introduce different terms, Lemma 11 (normal form). If π is a simple proof then there is a proof π ′ in normal form and a totally rigid acyclic grammar

G ′ with |G ′ | ≤ |π| and L(G nd (π ′ )) = L(G ′ ) ⊆ L(G(π)).
Proof. For showing this lemma we will consider proofs using the inference rule

Γ → ∆, A ∃x B, Π → ∆ Γ, Π → ∆, Λ p -cut
where B is quantifier-free and A can be transformed to ∃x B using the usual quantifier shifting rules. This inference rule is sound and the definition of the base substitutions extends naturally to simple proofs containing p-cuts because each p-cut still has one weak and one strong occurrence of a quantifier. Furthermore we use the notation |π| w for the number of weak quantifier inferences in π.

First, define π 1 from π by shifting down weakenings as far as possible removing pairs of connected weakenings and contractions and deleting subproofs of binary inferences as in the replacement of (ψ

1 ) Γ → ∆ Γ → ∆, A w r (ψ 2 ) A, Π → Λ Γ, Π → ∆, Λ cut by (ψ 1 ) Γ → ∆ Γ, Π → ∆, Λ w * .
Then all weakenings in π 1 appear in a block above the end-sequent, |π 1 | w ≤ |π| w and L(G(π 1 )) ⊆ L(G(π)) by Lemma 4.

Each cut that contains a quantifier has a strong side (the side of the occurrence of the strong quantifier) and a weak side (defined analogously). Define π 2 from π 1 by replacing each cut

(ψ 1 ) Γ → ∆, A (ψ 2 ) A, Π → Λ Γ, Π → ∆, Λ cut whose strong side is ψ 1 by (ψ 2 ) A, Π → Λ Π → Λ, ¬A ¬ r (ψ 1 ) Γ → ∆, A ¬A, Γ → ∆ ¬ l Γ, Π → ∆, Λ cut . Then |π 2 | w = |π 1 | w , G(π 2 ) = G(π 1
) and in π 2 the strong side of every cut is the right one.

Define π 3 from π 2 by replacing each cut

(ψ 1 ) Γ → ∆, A (ψ 2 ) A, Π → Λ Γ, Π → ∆, Λ cut by (ψ 1 ) Γ → ∆, A (ψ ′ 2 ) B[x\α], Π → ∆ ∃x B, Π → ∆ ∃ l Γ, Π → ∆, Λ p -cut
where ψ ′ 2 is obtained from ψ 2 by leaving out all strong quantifier inferences that introduce the quantifier in A and identifying their eigenvariables. Then |π 3 | w = |π 2 | w and by Lemma 5:

L(G(π 3 )) ⊆ L(G(π 2 )). Defining G ′ = G(π 3 ) we obtain |G ′ | ≤ |π 3 | w ≤ |π| and L(G ′ ) ⊆ L(G(π)).
It remains to construct π ′ . To that aim, we will first define π 4 from π 3 by prenexifying the weak side of a cut through the introduction of additional cuts. Apply the following transformation top-down to the whole proof: Suppose Qx A is a ancestor of a cut-formula on the weak side of the cut and auxiliary formula of an inference that is about to destroy its prenex property, for example Qx = ∃x and the inference being ¬ l ,

(ψ) Γ → ∆, ∃x A ¬∃x A, Γ → ∆ ¬ l ,
then replace the above inference by

(ψ) Γ → ∆, ∃x A (η) A[x\α] → A[x\α] A[x\α], ¬A[x\α] → ¬ l A[x\α], ∀x ¬A → ∀ l ∃x A, ∀x ¬A → ∃ l ∀x ¬A, Γ → ∆ cut
where α is a new eigenvariable. Similarly, replace inferences of the form

(ψ) Γ → ∆, ∃x A Γ → ∆, ∃x A ∨ B ∨ r 1 by (ψ) Γ → ∆, ∃x A (η) A[x\α] → A[x\α] A[x\α] → A[x\α] ∨ B ∨ r 1 A[x\α] → ∃x (A ∨ B) ∃ r ∃x A → ∃x (A ∨ B) ∃ l Γ → ∆, ∃x (A ∨ B) cut and (ψ 1 ) Γ → ∆, ∃x A (ψ 2 ) Π → Λ, B Γ, Π → ∆, Λ, ∃x A ∧ B ∧ r by (ψ 2 ) Π → Λ, B (ψ 1 ) Γ → ∆, ∃x A (η) A[x\α] → A[x\α] (η) B → B A[x\α], B → A[x\α] ∧ B ∧ r A[x\α], B → ∃x (A ∧ B) ∃ r ∃x A, B → ∃x (A ∧ B) ∃ l B, Γ → ∆, ∃x (A ∧ B) cut Γ, Π → ∆, Λ, ∃x (A ∧ B) cut .
Such a transformation replaces a set of production rules {β → t 1 , . . . β → t n } by {β → α, α → t 1 , . . . α → t n } where α is a new non-terminal, so by Lemma 6 the language is not changed. The symmetric cases for Qx = ∀x are treated analogously.

Furthermore, replace inferences of the form

(ψ) Γ → ∆, B Γ → ∆, ∃x A ∨ B ∨ r 2 by (ψ) Γ → ∆, B (η) B → B B → A[x\d] ∨ B ∨ r 2 B → ∃x (A ∨ B) ∃ r Γ → ∆, ∃x (A ∨ B) cut .
This transformation introduces productions of the form β → d which leave G nd unchanged. Again, the symmetric case for the universal quantifier is treated analogously. So we have obtained a proof π 4 with L(G nd (π 4 )) = L(G ′ ).

Finally, we shift down ∃ r -inferences together with contractions having their main formulas as auxiliary formulas and with the corresponding ∨ r -inferences that delete d until there are no other inferences between the ∃ r -inference and its blocking sequent. If one quantifier is introduced from the same term t two times we replace

(ψ) Γ → ∆, A[x\t], A[x\t] Γ → ∆, A[x\t], ∃x A ∃ r Γ → ∆, ∃x A, ∃x A ∃ r Γ → ∆, ∃x A c r by (ψ) Γ → ∆, A[x\t], A[x\t] Γ → ∆, A[x\t] c r Γ → ∆, ∃x A ∃ r
.

The result of these transformations is a proof π ′ in normal form having

L(G nd (π ′ )) = L(G ′ ).
The proof transformations used for showing the above lemma illustrate an important point: on the level of the grammar one can carry out transformations, in particular simplifications, which are impossible on the level of the proof (i.e. they necessitate tricks like p-cuts and dummy constants). This is due to the fact that the equality of languages is sufficient for validity and local soundness criteria as in a formal proof are no longer needed. The small grammar G ′ can neither be read off from π nor from π ′ ; both of them have larger grammars.

A proof in normal form exhibits a one-to-one correspondence between cuts and eigenvariables. Consequently, for an eigenvariable α we write c α for the cut corresponding to it. The set of eigenvariables of a proof π is denoted as EV(π). For a proof π in normal form and

α ∈ EV(π), define EV L(π, α) = {β ∈ EV(π) | c β is on the left above c α } and EV L (π, α) = {α} ∪ EV L(π, α).
Define EV R (π, α) and EV R(π, α) analogously for the right side of c α . Given a set V of variables and a set S of unary substitutions, define

S V = {σ ∈ S | dom(σ) ⊆ V }. Write B V (π) for (B(π)) V and define B X (π, α) = B EV X (π,α) (π) for X ∈ {L, R, L, R}.
During the elimination of contractions, proof parts are duplicated and the eigenvariables introduced there are copied hence renamed. The final value of an eigenvariable develops gradually through such renamings. It will turn out to be very useful to name an eigenvariable by the current state of development of its final value. To that aim, we label an eigenvariable α of the original proof π by a set of substitutions S ⊆ B(π) which is denoted as α S . By convention we identify α and α ∅ . An indexed variable α k with label S is written as α k,S .

A variable-renaming is a substitution whose range contains only variables. For a set of variables V , a variable-renaming ρ is called V -fresh if rge(ρ) ∩ V = ∅. For a substitution σ, a variablerenaming ρ is called σ-fresh if rge(ρ) ∩ (dom(σ) ∪ rge(σ)) = ∅ and for a set S of substitutions ρ is called S-fresh if it is σ-fresh for all σ ∈ S.

Define S R = {[xρ\tρ] | [x\t]
∈ S, ρ ∈ R} for a set of S-fresh variable renamings R and a set of substitutions S. For a variable-renaming ρ we write B ρ (π) for (B(π)) ρ . For a variable-renaming ρ, a set of unary substitutions S and a set of variables V we write

S ρ V for (S V ) ρ , so B ρ V (π) is ((B(π)) V ) ρ .
) = H(π){ρ A | A ∈ B * (π)} and B(π ′ ) = A∈B * (π) A ρ A .
Proof. Let EV(π) = {α 1 , . . . , α n } be ordered s.t. c α i is uppermost in {c α i , . . . , c αn }. The following equalities hold for all i ∈ {1, . . . , n} and follow from simple properties of the scope order and the uppermost order of the c α i :

B {α 1 ,...,α i } (π) ↑ α i = B L (π, α i ) ↑ α i (1) B {α 1 ,...,α i } (π) ↑ α = B R(π, α i+1 ) ↑ α for α ∈ EV R (π, α i+1 ) (2)
By Lemma 9 one obtains the * -ed version of these equalities. For k ∈ {0, . . . , n} let

R k = {ρ A | A ∈ B * {α 1 ,...,α k } (π)}.
We will show by induction on k that there is a proof π k in normal form s.t.

1. the only active cuts in π k are c α j for some j > k,

2. EV(π k ) = EV(π)R k , 3. H(π k ) = H(π)R k , and
4. B(π k ) = A∈B * {α 1 ,...,α k } (π) (A ∪ B {α k+1 ,...,αn} (π)) ρ A .
The result then follows from letting π ′ = π n .

If k = 0 then π = π 0 trivially satisfies the conditions. For the case k + 1 we obtain π k from induction hypothesis and observe that α k+1 ∈ EV(π k ) and that c α k+1 appears in a context of the form

(ψ 1 ) Γ → ∆, ∃x A (ψ 2 ) A[x\α k+1 ], Π → Λ ∃x A, Π → Λ ∃ l Γ, Π → ∆, Λ cut(c α k+1 ) .
Let {t 1 , . . . , t m } be the terms inserted for ∃x A in ψ 1 , then {t 1 , . . . , t m } = α k+1 B {α k+1 } (π k ). We will first describe this set of terms by suitably chosen upsets in the base substitutions of the original proof π. By induction hypothesis we have

B {α k+1 } (π k ) = A∈B * {α 1 ,...,α k } (π) B ρ A {α k+1 } (π)
which together with [START_REF] Baaz | On the non-confluence of cut-elimination[END_REF] shows that the mapping

τ : B * L (π, α k+1 ) ↑ α k+1 -→ {t 1 , . . . , t m }, A → α k+1 Aρ A
is well-defined. It is also bijective; for surjectivity let i ∈ {1, . . . , m}, then there is [α

k+1 \t i ] ∈ B {α k+1 } (π k ) hence there are A ∈ B * {α 1 ,...,α k } (π) and [α k+1 \s] ∈ B {α k+1 } (π) s.t. t i = sρ A . Let A ′ = {[α k+1 \s]} α∈s A ↑ α and observe that A ′ ∈ B * {α 1 ,...,α k+1 } (π) ↑ α k+1 = B * L (π, α k+1 ) ↑ α k+1 and A ↑ α = A ′ ↑ α for all α ∈ s hence t i = α k+1 A ′ ρ A ′ . For injectivity let {[α k+1 \s 1 ]} ∪ A 1 , {[α k+1 \s 2 ]} ∪ A 2 ∈ B * L (π, α k+1 ) ↑ α k+1 s.t. s 1 ρ A 1 = s 2 ρ A 2 .
As the ρ A i only add labels and the s i are label-free we have

s 1 = s 2 hence A 1 ↑ α = A 2 ↑ α for all α ∈ s i . If σ ∈ A i then there is α ∈ s i with α ≤ o σ so we can conclude A 1 = A 2 . Let B * L (π, α k+1 ) ↑ α k+1 = {C 1 , . . . , C m }
where the indices are obtained from τ and for 1 ≤ i ≤ m define a variable renaming

δ i = [α A \α A∪C i ] α∈EV R (π,α k+1 ),A∈B * R(π,α k+1 )↑α .
Let ψ ′ 1 be the proof of Γ → ∆, ∃x A, . . . , ∃x A obtained from ψ 1 by omitting all contractions on ancestors of ∃x A that contain the existential quantifier and define k+1 by replacing c α k+1 by

(ψ ′ 1 ) Γ → ∆, ∃x A, . . . , ∃x A (ψ 2 δ 1 ) A[x\α k+1,C 1 ], Π → Λ ∃x A, Π → Λ ∃ l Γ, Π → ∆, Λ, ∃x A, . . . , ∃x A cut . . . . Γ, Π, . . . , Π → ∆, Λ, . . . , Λ, ∃x A (ψ 2 δ m ) A[x\α k+1,Cm ], Π → Λ ∃x A, Π → Λ ∃ l Γ, Π, . . . , Π → ∆, Λ, . . . , Λ cut Γ, Π → ∆, Λ c *
where ψ 2 δ i is linked to t i via a cut.

After this transformation each logical inference, each axiom and each cut in π k+1 has a unique ancestor in π k and -by induction -in π. This ancestor relation extends naturally to auxiliary and main formulas of inferences. Observe that this proof transformation has the property that whenever an inference is above another one in one of the π k then the same is true about their ancestors in π. Therefore we obtain

EV(ψ 2 ) = EV R (π, α k+1 )R k
from the induction hypothesis which using (2) entails

EV(ψ 2 ) = {α A | α ∈ EV R (π, α k+1 ), A ∈ B * R(π, α k+1 ) ↑ α}.
For α A ∈ EV(ψ 2 ) and i, j ∈ {1, . . . , m}, the equality α A δ i = α A δ j entails C i = C j hence i = j so the regularity of π k+1 follows from that of π k . It is then easy to check that π k+1 is in normal form.

Let A ∈ B * R(π, α k+1 ), i ∈ {1, . . . , m}, C i ⊆ C ∈ B * L (π, α k+1 ), A ∪ C ⊆ A ′ ∈ B * {α 1 ,...,α k+1 } (π). Let F be a main formula of an inference in π which is ancestor of one in ψ 2 . If α ∈ F but α / ∈ EV R (π, α k+1 ) then α = α l for some l > k + 1 hence αρ A δ i = α. If α ∈ EV R (π, α k+1 ), then αρ A δ i = α A↑α∪C i , so F ρ A δ i = F [α\α A↑α∪C i ] α∈EV R (π,α k+1 ) . Now α k+1 is the entrance of B L (π, α k+1 ) for B R(π, α k+1 ) and B L (π, α k+1 ) ≮ o B R(π, α k+1 ) because c α k+1 is a purely existen- tial cut, so by Lemma 10 F ρ A δ i = F [α\α (A∪C)↑α ] α∈EV R (π,α k+1 ) and from the context lemma we obtain F ρ A δ i = F ρ A ′ . (3)
Let G be a main formula of an inference in π which is not ancestor of one in ψ 2 and let α ∈ G. Then α / ∈ EV R (π, α k+1 ) and α ≤ o B {α 1 ,...,α k+1 } (π) α k+1 is impossible because all cuts below c α k+1 have index higher than k + 1. Therefore

Gρ A = Gρ A δ i = Gρ A ′ (4)
by the context lemma. Summing up, (3) and ( 4) entail HR k+1 = HR k {δ i | 1 ≤ i ≤ m} for any formula H in π which together with the respective induction hypothesis shows 2. and 3.

It remains to show 4. First we will establish

B {α k+1 } (π k+1 ) = A∈B * {α 1 ,...,α k+1 } (π) A ρ A {α k+1 } . (5)
We start with the left-to-right inclusion: let [α k+1,C i \t i ] ∈ B(π k+1 ), then from τ and (1) we obtain a

C i ∈ B * {α 1 ,...,α k+1 } (π) ↑ α k+1 with i = α k+1 C i ρ C i and so [α\s] ∈ C i for some s. Let C i ⊆ A ∈ B * {α 1 ,...,α k+1 } (π), then [α k+1 \s] ρ A = [α k+1 \s] ρ C i = [α k+1,C i \t i ]. For the other direction let [α k+1 \s] ∈ A ∈ B * {α 1 ,...,α k+1 } (π) and let i ∈ {1, . . . , m} s.t. C i = A ↑ α k+1 ∈ B * L (π, α k+1 ) ↑ α k+1 . Then [α k+1 \s] ρ A = [α k+1 \s] ρ C i = [α k+1,C i \t i ] ∈ B(π k+1 ). Let us show B {α} (π k+1 ) = A∈B * {α 1 ,...,α k+1 } (π) A ρ A {α} for α ∈ EV R(π, α k+1 ) (6) next. If [α A∪C i \t ′ ] ∈ B(π k+1 ) then there is [α A \t] ∈ B(π k ) with tδ i = t ′ and [α\s] ∈ A ∈ B * R(π, α k+1 ) ↑ α with αρ A = α A and sρ A = t by induction hypothesis and (2). Let A ∪ C i ⊆ A ′ ∈ B {α 1 ,...,α k+1 } (π), then [α\s] ∈ A ′ and by (3) we have αρ A ′ = αρ A δ i = α A∪C i and sρ A ′ = sρ A δ i = t ′ .
For the other direction let A ∈ B * {α 1 ,...,α k+1 } (π), then there is i ∈ {1, . . . , m} and

A 0 ∈ B R(π, α k+1 ) s.t. C i ∪A 0 ⊆ A and [α\s] ∈ A 0 . By induction hypothesis [αρ A 0 \sρ A 0 ] ∈ B(π k ) so [αρ A 0 δ i \sρ A 0 δ i ] ∈ B(
(π ′ )-derivation ϕ → F ′ 1 → • • • → F ′ l there is a G(π)-derivation ϕ → F 1 → • • • → F l and an A ∈ B * (π) s.t. F i ρ A = F ′ i for 1 ≤ i ≤ l and every production γ → s used in F 1 → • • • → F l satisfies [γ\s] ∈ A.
We proceed by induction on l: for l = 1 this follows immediately. Let

ϕ → F ′ 1 → • • • → F ′ l+1 be given and obtain A and ϕ → F 1 → • • • → F l from induction hypothesis. Let αρ A ′ → tρ A ′ with A ′ ∈ B * (π) be the production rule applied in F ′ l → F ′ l+1 . So αρ A ′ appears in F ′ l = F l ρ A hence A ′ ↑ α = A ↑ α. As [α\t] ∈ A ′ we have [α\t] ∈ A and A ↑ β = A ′ ↑ β for all β ∈ t. Hence αρ A = αρ A ′ and tρ A = tρ A ′ so αρ A → tρ A applied to F ′ l gives F ′ l+1 .
Applying α → t at the same position to F l leads to a formula F l+1 with F l+1 ρ A = F ′ l+1 . By induction hypothesis the only α-production used in

F 1 → • • • → F l is α → t,
and as all non-terminals of t are rigid, the rigidity condition on α is preserved.

For the other direction, suppose we are given a G(π)-derivation. By Lemma 1 it induces a set A ∈ B * (π) and by applying ρ A can be converted to a G(π ′ )-derivation. Rigidity is preserved as ρ A is an injective renaming of non-terminals. Lemma 14. If π is a proof of Γ → ∃x A in normal form without active cuts, then Γ → L(G nd (π)) is provable.

Proof. We will first produce a proof π ′ in normal form without active cuts that does no longer contain d. If d appears in π, then it does so in a context of the form

(ψ 1 ) Π → Λ, A Π → Λ, A ∨ B[x\d] ∨ r 1 Π → Λ, ∃x (A ∨ B) ∃ r (ψ 2 ) A ∨ B[x\α], Σ → Θ ∃x (A ∨ B), Σ → Θ ∃ l Π, Σ → Λ, Θ cut
or in a symmetric variant. Let ψ ′ 2 be the proof of A, Σ → Θ obtained from ψ 2 by replacing A ∨ B[x\α] by A until arriving at inferences of the form

(ξ 1 ) A, Σ 1 → Θ 1 (ξ 2 ) B[x\α], Σ 2 → Θ 2 A ∨ B[x\α], Σ 1 , Σ 2 → Θ 1 , Θ 2 ∨ l
which are replaced by ξ 1 . Let π 1 be the proof obtained from replacing the above cut by

(ψ 1 ) Π → Λ, A (ψ ′ 2 ) A, Σ → Θ Π, Σ → Λ, Θ cut .
Repeating this transformation for all occurrences of d we obtain a proof π ′ which does not contain d anymore and by Lemma 4 satisfies

L(G(π ′ )) ⊆ L(G(π)) hence L(G(π ′ )) ⊆ L(G nd (π)).
Let α → t be any production in G(π ′ ), then [α\t] is the only base substitution of c α . We define a proof π ′′ as follows: we shift c α upwards to the left (observing that inference permutations do not change the grammar) until we reach the ∃ r -inference introducing t. The standard cutreduction of the existential quantifier then yields the proof π ′′ with H(π ′′ ) = H(π ′ )[α\t] and B(π ′′ ) = (B(π ′ ) \ {[α\t]}) [α\t] . A G(π ′′ )-derivation is then translated to a G(π ′ )-derivation by replacing applications of a production β → s[α\t] by β → s followed by a sufficient number of applications of α → t. Let p 1 , p 2 be two positions of α in the G(π ′ )-derivation. As α → t is the only α-production and all non-terminals in t are rigid, the rigidity condition is also fulfilled for α at p 1 , p 2 . For the other direction, observe that whenever α is introduced, say by a production β → s it must be followed by α → t on all positions of α. After permutation of independent steps we can thus collapse β → s and the appropriate applications of α → t to a single application of β → s[α\t] which preserves rigidity. We have obtained L(G(π ′′ )) = L(G(π ′ )).

By iterating this procedure we obtain a proof π * with L(G(π * )) = L(G(π ′ )) ⊆ L(G nd (π)) all of whose cuts are quantifier-free. Therefore B(π * ) = ∅, i.e. there are no B-productions in G(π * ) and using the standard proof of the mid-sequent theorem (i.e. inference permutations) one obtains a proof of Γ → H(π * ) i.e. Γ → L(G(π * )) from which by adding weakenings one obtains a proof of Γ → L(G nd (π)).

We can now prove the main results of this paper.

Theorem 2. If π is a simple proof of Γ → ∃x A then there is a totally rigid acyclic grammar

G ′ with |G ′ | ≤ |π| and L(G ′ ) ⊆ L(G(π)) s.t. Γ → L(G ′ ) is provable.
Proof. From Lemma 11 we obtain a proof π 1 in normal form and a grammar G ′ satisfying

|G ′ | ≤ |π| and L(G ′ ) = L(G nd (π 1 )) ⊆ L(G(π)). Applying Lemma 13 to π 1 we obtain a proof π 2 in normal form without active cuts satisfying L(G(π 2 )) = L(G(π 1 )) hence L(G nd (π 2 )) = L(G nd (π 1 )) = L(G ′ ). Applying Lemma 14 to π 2 then shows that Γ → L(G ′ ) is provable. Corollary 1. If π is a simple proof of Γ → ∃x A then Γ → L(G(π)) is provable.
Proof. Append weakenings to the proof of Γ → L(G ′ ) obtained from Theorem 2.

Example 6. Applying Corollary 1 to the proof π of Example 2 shows that

A 1 , A 2 , A 3 → R(g(a, f (a))), R(g(b, f (b)))
is provable.

The following corollary shows how the logical restriction on the cut-formulas (of having at most one quantifier) induces a combinatorial restriction on the Herbrand-disjunctions obtainable from simple proofs.

Corollary 2. If π is a simple proof of Γ → ∃x A, then there are variables x 1 , . . . , x n and sets of terms U 1 , . . . , U n s.t.

Γ → (u 1 ,...,un)∈U 1 ו••×Un A[x 1 \u 1 ] • • • [x n \u n ] is provable and n i=1 |U i | ≤ |π|.
Proof. By Theorem 2 there is G ′ with |G ′ | ≤ |π| and Γ → L(G ′ ) being provable. By Lemma 3 we can write L(G ′ ) using sets U i as above.

Example 7. Applying Corollary 2 to the proof π of Example 2 yields the representation

A 1 , A 2 , A 3 → (u 1 ,u 2 ,u 3 )∈U 1 ×U 2 ×U 3 R(x)[x\u 1 ][β\u 2 ][α\u 3 ]
where U 1 = {g(α, β)}, U 2 = {f (α)} and U 3 = {a, b}.

From Tree Languages to Proofs

Already the results in [START_REF] Hetzl | On the form of witness terms[END_REF] show that a simple proof induces an acyclic regular(!) tree grammar whose finite language is an Herbrand-disjunction. So what have we gained from the strengthening of this result by adding total rigidity? On the one hand, we have gained an exponent: we have seen in Lemma 3 that in the totally rigid case the size of the language is bound by n n , but:

Lemma 15. There is an acyclic regular tree grammar G with 2n productions and L(G) = n n n .

Proof. Let f be an n-ary function symbol, then the productions

α 0 → f (α 1 , . . . , α 1 ), . . . , α n-1 → f (α n , . . . , α n )
create an tree with n n leaves. Let c 1 , . . . , c n be terminal symbols, then by adding the productions

α n → c 1 , . . . , α n → c n
we obtain the desired grammar G.

However there is another -more fundamental -motivation for this result: in this section we show that the compression power of simple proofs corresponds exactly to that of totally rigid acyclic grammars. Given such a grammar G we will obtain a simple proof π that induces G.

As L(G(π)) is a set of formulas but L(G) is a set of terms (which do not necessarily represent formulas), we cannot expect to obtain G(π) = G. The closest possible connection is to wrap up the term language of G in some new unary predicate symbol R 1 .

Theorem 3. For every totally rigid acyclic tree grammar G = α 1 , R, T, P there is a simple proof π with G(π) = α 0 , R ∪ {α 0 }, T, P ∪ {α 0 → R 1 (α 1 )} .

Proof. By Lemma 3 we can assume that G = α 1 , {α 1 , . . . , α n }, T, P s.t. α i depends only on α j with j > i. The proof π is defined in the language T ∪ {R i | 1 ≤ i ≤ n} where the R i are unary predicate symbols with intended interpretation "being reachable from the non-terminal α i ". For each rule α i → t define the formula

ϕ α i →t = ∀x i+1 • • • ∀x n ( R i+1 (x i+1 ) ⊃ • • • R n (x n ) ⊃ R i (t[α j \x j ] n j=i+1
) ). For each non-terminal α i with rules α i → t 1 , . . . , α i → t m define the formula

ϕ i = m j=1 ϕ α i →t j and the proof ψ i = • • • R i (t j ) → R i (t j ) R i (t j ) → ∃x R i (x) ∃ r ϕ α i →t j , R i+1 (α i+1 ), . . . , R n (α n ) → ∃x R i (x) ∀ * l , ⊃ * l • • • ϕ i , R i+1 (α i+1 ), . . . , R n (α n ) → ∃x R i (x) ∨ * l .

Now define proofs π

i : ϕ 1 , . . . , ϕ i , R i+1 (α i+1 ), . . . , R n (α n ) → ∃x R 1 (x) for i ∈ {0, . . . , n} and π ′ i : ϕ 1 , . . . , ϕ i , ∃x R i+1 (x), R i+2 (α i+2 ), . . . , R n (α n ) → ∃x R 1 (x) for i ∈ {0, . . . , n -1} by π ′ i = (π i ) ϕ 1 , . . . , ϕ i , R i+1 (α i+1 ), . . . , R n (α n ) → ∃x R 1 (x) ϕ 1 , . . . , ϕ i , ∃x R i+1 (x), R i+2 (α i+2 ), . . . , R n (α n ) → ∃x R 1 (x) ∃ l and π 0 = R 1 (α 1 ) → R 1 (α 1 ) R 1 (α 1 ), . . . , R n (α n ) → ∃x R 1 (x) w * l , ∃ r and π i+1 = (ψ i+1 ) ϕ i+1 , R i+2 (α i+2 ), . . . , R n (α n ) → ∃x R i+1 (x) (π ′ i ) ϕ 1 , . . . , ϕ i+1 , R i+2 (α i+2 ), . . . , R n (α n ) → ∃x R 1 (x) cut .
Then it is easy to verify that π = π n : ϕ 1 , . . . , ϕ n → ∃x R 1 (x) has the desired grammar.

It is worthwhile to describe the models of the end-sequent ϕ 1 , . . . , ϕ n → ∃x R 1 (x) of the proof constructed above: in a structure that satisfies ϕ i at least one of the α i -productions must be true. A structure satisfying ϕ 1 , . . . , ϕ n hence makes one production of every non-terminal true and therefore one formula from L(G(π)). The disjunction of the formulas in L(G(π)) is therefore true in every model of ϕ 1 , . . . , ϕ n and vice versa: every disjunction of instances of ∃x R 1 (x) which is true in all models of ϕ 1 , . . . , ϕ n must contain L(G(π)).

Conclusion

We have shown that the compression power of proofs where each cut contains at most one quantifier corresponds exactly to that of totally rigid acyclic tree grammars. This work constitutes a proof-of-concept result for a new connection between proof theory and formal language theory arising from exact characterisations of classes of proofs by classes of grammars.

A side effect of Corollary 1 is to illustrate how little information about a proof is necessary for computing an Herbrand-disjunction: the current instances of the end-formula together with the base substitutions suffice, not even the cut-formulas are necessary.

The following directions are left for future work.

Extensions

The strategy of describing a cut-free proof by a tree language is applicable to any system that possesses an Herbrand-like theorem, i.e. even full higher-order logic as in [START_REF] Miller | A Compact Representation of Proofs[END_REF]. The difficulty consists in finding an appropriate type of grammars. For full first-order logic (including quantifier alternations in the cuts) it would be natural to consider a stack of tree grammars, each layer of which corresponds to one layer of quantifiers in the cuts and to prove an analogous result by iterating Lemma 12. An extension to arithmetic would require -in addition -a mechanism for recursion in the grammars to model induction.

Confluence

One of the original motivations for describing cut-elimination by grammars was to characterise the set of cut-free proofs that can be obtained from a single proof by cut-elimination without any restriction of the reduction strategy [START_REF] Hetzl | On the form of witness terms[END_REF]; let → denote this cut-elimination relation. The author conjectures that the result of [START_REF] Hetzl | On the form of witness terms[END_REF] can be extended to the rigid tree grammars presented in this paper, i.e.

Conjecture 1. If π → π ′ and π ′ is cut-free, then H(π ′ ) ⊆ L(G(π)).

In fact, the behaviour of rigid tree grammars under the cut-reduction steps suggests the following stronger version. Let → -be → without deletion of subproofs (e.g. in a purely multiplicative calculus: without the reduction of weakening).

Conjecture 2. If π → -π ′ , then L(G(π)) = L(G(π ′ )).

This conjecture entails a confluence result by applying it to two arbitrary → --normal forms π ′ 1 and π ′ 2 yielding H(π ′ 1 ) = L(G(π)) = H(π ′ 2 ). Confluence properties of classical logic have been the subject of many papers. This conjecture would be an important contribution to that discussion: it states that the first-order level is confluent (though highly redundant [START_REF] Baaz | On the non-confluence of cut-elimination[END_REF]) and that the different normal forms arise only from different choices taken at the propositional level how to (partially) remove this redundancy.

Algorithmic Cut-Introduction

Computer-generated proofs are typically analytic, i.e. in the case of first-order logic can be written as Herbrand-disjunctions. Due to their shorter length it is natural to try to find proofs with cut algorithmically. One approach is to abbreviate a given cut-free proof by the introduction of cuts, see e.g. [START_REF] Finger | Equal Rights for the Cut: Computable Non-analytic Cuts in Cut-based Proofs[END_REF][START_REF] Woltzenlogel | Atomic Cut Introduction by Resolution: Proof Structuring and Compression[END_REF]. With respect to general-purpose data compression, such a procedure has the algorithmic advantage of also reducing the runtime of operations, for example proof checking, which is important in applications such as proof-carrying code. Cut-introduction (as any compression) exploits redudancy which is present in the Herbrand-disjunction. A fundamental problem of this approach is to understand which type of redudancy can be removed by which cuts. The characterisation results of this paper give a solution to this problem for the case of cuts with one quantifier: the corresponding redundancy is that of the language of a totally rigid acyclic tree grammar.

Proof Length

From a more theoretical point of view, it is possible to view a proof with cuts as a compressed representation of a cut-free proof or an Herbrand-disjunction (if we fix a particular cut-elimination procedure, for instance the computation of the language of its grammar). The results of this paper show that the size of the proof with cut is intimately related to measures from formal language theory such as automatic complexity [START_REF] Shallit | Automatic complexity of strings[END_REF] or automaticity [START_REF] Shallit | Automaticity I: Properties of a Measure of Descriptional Complexity[END_REF]. By the size condition of Corollary 2, a lower bound on the number of rules of totally rigid acyclic tree grammars translates to a lower bound on the length of proofs with cuts. The perspective of exploiting this connection in order to use techniques from formal language theory for proving lower bounds on proofs seems promising (e.g. for problems 22 and 24 in [START_REF] Clote | Open problems[END_REF] on the impact of Skolemisation and equational reasoning on the length of proofs).

Intuitionistic Logic

Another interesting application of these grammars would be the analysis of cut-elimination in intuitionistic logic. Moving from Herbrand's theorem to the existential witness property, the natural expectation would be to find that |L(G(π))| = 1.

Definition 10 .

 10 For a simple proof π define the totally rigid grammar G(π) = ϕ, N, T, P by N = {ϕ} ∪ EV(π), T = Σ(π) ∪ {∧, ∨, ¬}, and

Example 4 .

 4 The proof π of Example 2 has G(π) = ϕ, N, T, P where N = {ϕ, α, β}, T = {a, b, f, g, P, Q, R, ∧, ∨, ¬} and P = {ϕ → R(g(α, β)), β → f (α), α → a, α → b}, see also the diagram in Figure 1. The language of this grammar is L(G(π)) = {R(g(a, f (a))), R(g(b, f (b)))}. Lemma 7. If π is a simple proof, then G(π) is acyclic.

  where π is the proof of Example 2, let [β\f (α)] < 1 [α\a] and [β\f (α)] < 1 [α\b] be all pairs in the < 1 -relation and let [α\a] ∼ [α\b] be the only pair in the equivalence relation ∼. Then U * ↑ α = {{[α\a]}, {[α\b]}} and U

  π k+1 ) and by[START_REF] Clote | Open problems[END_REF] we have αρ A 0 δ i = αρ A and sρ A 0 δ i = sρ A .The equality B {α} (π k+1 ) = A∈B * {α 1 ,...,α k+1 } (π)B ρ A {α} (π) for α ∈ {α 1 , . . . , α k } \ EV R(π, α k+1 )(7)follows from induction hypothesis and the observation that B α (π) o α k+1 for such α. It remains to showB {α} (π k+1 ) = A∈B * {α 1 ,...,α k+1 } (π) B ρ A {α} (π) for α ∈ {α k+2 , . . . , α n } (8) Let [α\t ′ ] ∈ B(π k+1 ), then there is [α\t] ∈ B(π k )where either (case i) t ′ is introduced by an ∃ r -inference in one of the ψ 2 δ i , then t ′ = tδ i for some i ∈ {1, . . . , m} or otherwise (case ii) [α\t] ρ A = [α\t] for all A ∈ B * {α 1 ,...,α k+1 } (π) which directly entails the claim. In case i) we obtain A ∈ B * R(π, α k+1 ) and [α\s] ∈ B(π) with sρ A = t from induction hypothesis and (1).Let A ∪ C i ⊆ A ′ ∈ B * {α 1 ,...,α k+1 } (π) then sρ A ′ = sρ A δ i = t ′ by (3). For the other direction let A ∈ B * {α 1 ,...,α k+1 } (π), [α\s] ∈ B(π) and A 0 ∈ B R(π, α k+1 ), i ∈ {1, . . . , m} s.t. A 0 ∪ C i ⊆ A.If s is introduced by an ∃ r -inference on the right above c α k+1 in π then by[START_REF] Clote | Open problems[END_REF] we have sρ A = sρ A 0 δ i .By induction hypothesis and (2) we have [α\sρA 0 ] ∈ B(π k ) which entails [α\sρ A 0 δ i ] ∈ B(π k+1 ).If s is not introduced on the right above c α k+1 in π, then sρ A = sρ A 0 by[START_REF] Clote | Open problems[END_REF]. By induction hypothesis [α\sρ A 0 ] ∈ B(π k ) hence [α\sρ A 0 ] ∈ B(π k+1 ).

Lemma 13 .

 13 If π is a proof in normal form, then there is a proof π ′ in normal form without active cuts s.t. L(G(π ′ )) = L(G(π)). Proof. Let π ′ be the proof obtained in Lemma 12 having H(π ′ ) = H(π){ρ A | A ∈ B * (π)} and B(π ′ ) = A∈B * (π) A ρ A . Note that every substitution in B(π ′ ) is of the form [αρ A \tρ A ] for [α\t] ∈ A ∈ B * (π).Let us first show that for every G

  Definition 13 (scope order). For a proof π in normal form and [α\t], [β\s] ∈ B(π) we write [α\t] < o 1 [β\s] if the ∃ r -inference of t is above the ∃ l -inference of β. We furthermore write < o for the transitive and ≤ o for the reflexive and transitive closure of< o 1 . Note that [α\t] < o [β\s 1 ] iff [α\t] < o [β\s 2 ] so we often just write [α\t] < o β. Furthermore, [α\t] < o 1 [β\s] is necessary (although not sufficient) for β ∈ t. Hence the scope order includes the order induced by the productions of the grammar as in Section 2 and is equal to it if every term introduced by a weak quantifier inference contains all variables introduced underneath it by strong quantifier inferences. For technical reasons (the applicability of Lemma 10) it is more convenient to work with the scope order in this section. We apply the notation and results of Section 4 to the set B(π) with order < o 1 and equivalence relation [α\t] ∼ [β\s] iff α = β; the upset formation ↑ as well as the choice-operation * have the meaning defined in Section 4. We write B * (π) for (B(π)) * . For a set of unary substitutions A we define the variable renaming ρ A = [α\α A↑α ] α∈A . As we will see later, this renaming plays an important role because it labels α with the partial value given by A. A cut c in a proof π in normal form is called active if its cut-formula ∃x A is introduced from more than one term in the left subproof. The following lemma is the central technical result of this paper.Lemma 12 (Contraction Lemma). If π is a proof in normal form, then there is a proof π ′ in normal form without active cuts s.t. H(π ′

The Grammar of a Proof Definition 6. A sequent is a pair of multisets of formulas. A proof is a tree that starts with sequents of the form A → A for an atomic formula A and is built up using the following rules.Γ → ∆, A Π → Λ, B Γ, Π → ∆, Λ, A ∧ B ∧ r A, Γ → ∆ A ∧ B, Γ → ∆ ∧ l 1 B, Γ → ∆ A ∧ B, Γ → ∆ ∧ l 2 A, Γ → ∆ B, Π → Λ A ∨ B, Γ, Π → ∆, Λ ∨ l Γ → ∆, A Γ → ∆, A ∨ B ∨ r 1 Γ → ∆, B Γ → ∆, A ∨ B ∨ r 2 Γ → ∆, A ¬A, Γ → ∆ ¬ l A, Γ → ∆ Γ → ∆, ¬A ¬ r A[x\t], Γ → ∆ ∀x A, Γ → ∆ ∀ l Γ → ∆, A[x\α] Γ → ∆, ∀x A ∀ r A[x\α], Γ → ∆ ∃x A, Γ → ∆ ∃ l Γ → ∆, A[x\t] Γ → ∆, ∃x A ∃ r Γ → ∆ A, Γ → ∆ w l Γ → ∆ Γ → ∆, A w r A, A, Γ → ∆ A, Γ → ∆ c l Γ → ∆, A, A Γ → ∆, A c r


M W ; Erasmusmc

Pediatrics Lakeman Erasmus Mc

Ellen Denayer

Magdalena Chmara

Hilde Brems

Anneke Maat Kievit

Yolande Van Bever

Ans Mw Van Den Ouweland

Rick Van Minkelen

Arja De Goede-Bolder

Rianne Oostenbrink

Phillis Lakeman

Eline Beert

Takuma Ishizaki

Tomoaki Mori

Kathelijn Keymolen

Jenneke Van Den Ende

Elisabeth Mangold

Sirkku Peltonen

Glen Brice

Julia Rankin

Karin Y Van Spaendonck-Zwarts

Akihiko Yoshimura

Eric Legius
email: eric.legius@uzleuven.be.

HUMAN MUTATION Mutation in Brief #____ (20XX) Online

Keywords: Legius syndrome, SPRED1, NF1, RAS-MAPK pathway, polydactyly

Legius syndrome presents as an autosomal dominant condition characterized by caféau-lait macules with or without freckling and sometimes a Noonan-like appearance and/or learning difficulties. It is caused by germline loss-of-function SPRED1 mutations and is a member of the

INTRODUCTION

Legius syndrome (OMIM # 611431) was recently identified as a Neurofibromatosis type 1 (NF1)-like syndrome caused by heterozygous germline loss-of-function SPRED1 (OMIM *609291) mutations [START_REF] Brems | Germline loss-of-function mutations in SPRED1 cause a neurofibromatosis 1-like phenotype[END_REF]. In the original report five families with an autosomal dominant inherited condition presenting with multiple café-au-lait macules (CALM), axillary freckling, macrocephaly and at times a Noonan-like facial appearance were described. Learning difficulties and/or attention deficit were observed in several children and multiple lipomas were present in several adults. Some typical NF1 (OMIM #162200) features such as Lisch nodules of the iris, neurofibromas and central nervous system tumors were systematically absent.

Pasmant et al. identified five probands with a SPRED1 mutation in 61 index cases. They confirmed a high prevalence of CALM, freckling and learning disability as well as absence of neurofibromas and Lisch nodules (Pasmant et al., 2009b). Noonan-like dysmorphism was not observed and macrocephaly was reported in only one individual. Lipomas were seen in one family. Spurlock et al. identified 6 probands with SPRED1 mutations in 85 unrelated patients referred for NF1 gene (OMIM *613113) testing who were NF1 mutation negative and had no cutaneous neurofibromas [START_REF] Spurlock | SPRED1 mutations (Legius syndrome): another clinically useful genotype for dissecting the neurofibromatosis type 1 phenotype[END_REF]. All affected probands but 1 satisfied NF1 diagnostic criteria. They all had CALM. None had Noonan-like features, macrocephaly, Lisch nodules or cutaneous neurofibromas. No significant developmental or learning problems were observed.

Messiaen et al. performed a genotype-phenotype study in 22 unrelated probands carrying a SPRED1 mutation identified through clinical testing [START_REF] Messiaen | Clinical and mutational spectrum of neurofibromatosis type 1-like syndrome[END_REF]. Fifty percent of SPRED1 positive individuals fulfilled NF1 NIH diagnostic criteria based on the presence of more than 5 CALM with or without freckling or a NF1 family history. Symptomatic optic pathway gliomas, neurofibromas or typical NF1 osseous lesions were absent in the affected individuals and there was no increased prevalence of lipomas. Relative macrocephaly was documented in 27% of individuals and language/speech difficulties in 25% of children. In a second cross-sectional study Messiaen et al. performed SPRED1 mutation analysis in 1318 unrelated patients presenting with a broad range of signs typical for NF1 but no detectable NF1 mutation [START_REF] Messiaen | Clinical and mutational spectrum of neurofibromatosis type 1-like syndrome[END_REF]. They identified 26 pathogenic SPRED1 mutations in 33 probands and 7 probable non-pathogenic missense mutations in 9 probands. A SPRED1 mutation detection rate of 19% was found in families with an autosomal dominant phenotype of CALM with or without freckling and no other NF1 features. Muram-Zborovski et al. sequenced the SPRED1 gene in 151 individuals with a clinical diagnosis of NF1 and identified 2 SPRED1-positive individuals. They both had multiple CALM, intertriginous freckling, learning difficulties and absence of neurofibromas [START_REF] Muram-Zborovski | SPRED1 Mutations in a Neurofibromatosis Clinic[END_REF].

The SPRED1 gene is a relatively small gene (7 coding exons) located on chromosome 15q14. Most germline mutations truncate the protein, but two pathogenic missense mutations and one in-frame deletion have been reported. Similar to neurofibromin, the protein product of NF1, SPRED1 is a negative regulator of RAS-MAPK signalling. Whereas neurofibromin acts as a GTP-ase activating protein that accelerates conversion of active GTPbound RAS to inactive GDP-bound RAS, SPRED1 is believed to act at the level of RAS-RAF interaction [START_REF] Wakioka | Spred is a Sprouty-related suppressor of Ras signalling[END_REF]. Both syndromes thus belong to the group of RAS-MAPK pathway disorders or neurocardio-facial-cutaneous (NCFC) syndromes [START_REF] Bentires-Alj | Stops along the RAS pathway in human genetic disease[END_REF][START_REF] Denayer | Clinical and molecular aspects of RAS related disorders[END_REF]. Different degrees of cognitive impairment and tumor predisposition are associated with these syndromes. In Legius syndrome one occurrence each of non-small cell lung cancer, Wilms tumor, tubular colon adenoma, [START_REF] Brems | Germline loss-of-function mutations in SPRED1 cause a neurofibromatosis 1-like phenotype[END_REF] acute myeloblastic anemia, (Pasmant et al., 2009a;Pasmant et al., 2009b) tenosynovial giant cell tumor, breast cancer and dermoid tumor of the ovary [START_REF] Messiaen | Clinical and mutational spectrum of neurofibromatosis type 1-like syndrome[END_REF] has been reported. No causal relationship with the germline SPRED1 mutation has been proven in any of these cases. Whether Legius syndrome is associated with an increased risk for a specific range of malignancies remains unknown. Messiaen et al. estimated that a study of 250 adult patients would be needed to detect rare complications with a prevalence of only 1% [START_REF] Messiaen | Clinical and mutational spectrum of neurofibromatosis type 1-like syndrome[END_REF]. Therefore it remains important to report on new cases of Legius syndrome.

In this study the clinical data of fourteen new probands with Legius syndrome and their affected relatives are described. One missense mutation was characterized functionally.

MATERIALS AND METHODS

Study population

After publication of the first report, SPRED1 mutation analysis was performed in the Department of Human Genetics, Catholic University of Leuven, Belgium in 35 probands with a NF1-like syndrome. DNA samples included patients followed in the Leuven neurofibromatosis clinic as well as samples sent by clinical geneticists from other centres in Belgium or from abroad. Clinical data of 6 affected probands and their relatives carrying a mutation were collected by an extended phenotypical checklist (families 6, 7, 10, 11, 12, 14). In addition clinical data of eight other SPRED1-mutation positive families were obtained. Mutation analysis for these cases was performed in the Department of Clinical Genetics, Erasmus Medical Centre, Rotterdam, The Netherlands (families 1, 2, 3, 5, 8, 9, 13) and in the Medical Genetics Centre, Munich, Germany (family 4). Most of these cases showed a phenotype compatible with Legius syndrome: presence of CALM and freckling and absence of neurofibromas and several had been tested before for NF1 mutations.

Brain imaging data were available for 10 patients (9 MRI, 1 CT). Height and head circumference at a given age were converted to standard deviations using the growth charts of Flanders 2004 (http://www.vub.ac.be/groeicurven) and [START_REF] Roelants | References for growth and pubertal development from birth to 21 years in Flanders, Belgium[END_REF] An individual was recorded as macrocephalic when head circumference was 2 standard deviations above the mean. An individual was recorded to have relative macrocephaly when head circumference was above 2 standard deviations at the age when height would have been at the mean.

Mutation analysis

Mutation analysis was performed as reported before [START_REF] Brems | Germline loss-of-function mutations in SPRED1 cause a neurofibromatosis 1-like phenotype[END_REF]. Mutation numbering was based on the cDNA sequence with +1 corresponding to the A of the ATG translation initiation codon in the reference sequence (GenBank accession code: NM_152594.2). For protein numbering the initiation codon is codon 1 (NP_689807.1). Names of all variants were checked using the Mutalyzer program (http://www.LOVD.nl/mutalyzer/). Amino acid conservation for a novel missense mutation was evaluated with the Conseq program (http://conseq.tau.ac.il/). Bio-informatical prediction of the possible impact of the missense change on the SPRED1 protein was performed with Polyphen (http://genetics.bwh.harvard.edu/pph/). Mutation analysis in DNA extracted from paraffin-embedded tissue from a vestibular schwannoma was performed with a different set of primers resulting in smaller amplicons.

Functional analyses

Wild-type SPRED1 cDNA was cloned into a pcDNA3.1 (Invitrogen) construct encoding an N-terminal Flagtag. SPRED1 mutant p.Trp31Cys was generated by PCR-directed mutagenesis and verified by sequencing. Wildtype and mutant SPRED1 constructs were subcloned in a pmax vector (Amaxa Biosystems). The GAL4/Elk-1 reporter assay was performed as described before [START_REF] Messiaen | Clinical and mutational spectrum of neurofibromatosis type 1-like syndrome[END_REF]. The Elk-1 transcription factor is a substrate for phosphorylation by the activated MAPK pathway. In the GAL4/Elk-1 reporter assay luciferase activity is measured in HEK293T cells co-transfected with pFA-Elk1, pFR-Luc, β-galactosidase and Flag-tagged SPRED1 constructs after stimulation with epidermal growth factor (EGF).

RESULTS

Mutation analysis

Twelve different truncating SPRED1 mutations were found in 13 unrelated probands: 7 frameshift and 5 nonsense mutations, 11/13 cases were familial. A missense mutation was found in proband 3 and occurred de novo. Mutation analysis of DNA extracted from peripheral blood of both parents of proband 3 showed only wild type SPRED1 sequence. An overview of the different mutations is given in Table 1. Six mutations had not been reported as germline mutations in the literature before (c. 93G>T,p.Trp31Cys;c.304dupA,p.Thr102AsnfsX7;c.360dupA,p.Glu121ArgfsX13;c.576_580dup,p.Gln194ProfsX4;c.940C>T,p.Gln314X;c. p.Arg349GlyfsX4). Trp31 is a highly conserved amino acid residue (Conseq score 7, conserved in Bos Taurus, Mus musculus, Gallus gallus, Xenopus tropicalis, Danio rerio, Drosophila melanogaster). Bio-informatic analysis using Polyphen software predicts the p.Trp31Cys mutation to be probably damaging. It may disrupt the function of the EVH1 domain. In the Elk-1 reporter assay overexpression of wild-type SPRED1 efficiently inhibited the activation of the MAPK pathway after stimulation of the cells with EGF resulting in low luciferase activity. The Trp31Cys SPRED1 mutant was unable to suppress the EGF induced Elk-1 dependent transcription activation confirming that this is an inactivating and therefore pathogenic mutation. (Figure 1) Figure 1: Elk-1 quantitative luciferase assay for Erk activation. Empty vector or vector carrying wild-type (WT; as a control) or mutant SPRED1 (Trp31Cys, W31C; Thr102Arg, T102R; Ile81del, I81del) were transfected into HEK293T cells along with Elk-1 reporter plasmids. Elk-1 activation is measured as an increase in luciferase activity after stimulation with EGF. Three different amounts of plasmids were transfected: 0.05µg, 0.1µg and 0.2 µg. The bars represent the average increase in luciferase activity of 3 replicates and error bars represent the standard deviation. Wild-type SPRED1 vector efficiently suppresses EGF induced Elk-1 activation in comparison to empty vector. Similar to the known pathogenic Thr102Arg and Ile81del mutations, Trp31Cys is unable to downregulate the increase in luciferase activity after EGF stimulation.

Phenotype in patients with germline SPRED1 mutations

Clinical information was obtained for 14 probands and 16 affected relatives. Phenotypic features are summarized in Table 2. All individuals had more than 5 CALM, except for two adults from the same family who had none. Freckling was present in 10/27 individuals, macrocephaly in 1/24, relative macrocephaly in 2/24. In 20/24 individuals the head circumference was on a higher percentile than the height. Lisch nodules were systematically absent in those patients who had been investigated ophthalmologically (17/30). Neurofibromas were not observed, lipomas were present in 2/15 adults. Information regarding psychomotor development was only available for 17 patients. Five children had motor delay, 5 children delayed speech. Learning difficulties were mentioned in 14/25 individuals. Three individuals were diagnosed with ADHD; in a fourth individual hyperactivity and attention deficit were noticed, but there was no formal diagnosis of ADHD; one patient had attention deficit without hyperactivity (ADD). In another child concentration problems were noted. In 7 patients the diagnosis of Noonan syndrome was considered previously and in 20 patients the diagnosis of NF1 was suspected. Sixteen patients fulfil the NF1 NIH diagnostic criteria based on the presence of more than 5 CALM with or without freckling and a positive family history. One patient had a desmoid tumor of the abdominal wall. A vestibular schwannoma had developed after the age of 50 in patient I1 of family 11. She was said to have the same pigmentary findings as her daughter and granddaughter, but had not been examined clinically. SPRED1 mutation analysis was conducted on paraffin-embedded tissue from this vestibular schwannoma. In this tissue the familial SPRED1 germline mutation was confirmed, but no somatic second hit was found in SPRED1. T2 hyperintense spots in the subcortical white matter were observed on brain MRI in 2 patients. (Figure 2) Other findings were epilepsy and Parkinsons disease (n=1), unilateral postaxial hexadactyly (n=2), Chiari malformation with syringomyelia (n=1), scoliosis (n=4) with block vertebra (n=1), sensorineural hearing loss (n=1), asymptomatic arachnoid cyst detected by brain MRI (n=1), congenital hypothyroidism (n=1). One patient had a clinical diagnosis of Marfan syndrome, which was confirmed by a pathogenic mutation in the FBN1 gene (c.3757C>T, p.Gln1253X). Received <date>; accepted revised manuscript <date>.

DISCUSSION

We report on the second largest series of families with Legius syndrome. In this report we describe 30 new individuals from 14 families. Our results confirm previous findings that Legius syndrome is characterized by the presence of CALM with or without freckling and the absence of typical NF1 complications such as Lisch nodules and neurofibromas. In a subset of patients we find Noonan-like facial features (n=12) and/or sternal abnormalities (n=7; one of these patients had an additional diagnosis of Marfan syndrome, which is also associated with sternal abnormalities). No congenital vascular malformations were present in this cohort. One vestibular schwannoma and one benign tumor of the abdominal wall (desmoid tumor) were observed. Both tumor types had not been reported before in association with Legius syndrome and it is unclear whether there is a causal relationship between these tumors and the germline SPRED1 mutation. Learning difficulties were mentioned in 14/25 patients (56%), three patients were diagnosed with ADHD and one with ADD. Combining the data in the literature with that of the current report (142 individuals) learning difficulties were observed in 26 individuals (18.3%) with Legius syndrome, delayed psychomotor development (mostly confined to specific speech delay) in 13 (9.2%), and hyperactivity, attention problems or ADHD in 14 (9.9%). Whether Legius syndrome is associated with a specific neurocognitive profile warrants further investigation. Focal areas of high signal intensity on T2-weighed or FLAIR images of brain MRI, also denoted UBOs (Unidentified Bright Objects), are found in about 70% of children with NF1 [START_REF] Gill | Age-related findings on MRI in neurofibromatosis type 1[END_REF]North, 2000). UBOs occur most often in the basal ganglia, cerebellum, thalamus, brainstem and subcortical white matter. They are not associated with focal neurological deficits, but the pathological correlate remains controversial (North, 2000). The number and intensity of UBOs diminish with age in the basal ganglia, cerebellum, brainstem and thalamus, whereas lesions in the cerebral hemispheres and hippocampus do not change in prevalence over time, suggesting a different pathologic background [START_REF] Gill | Age-related findings on MRI in neurofibromatosis type 1[END_REF]. There is no consensus on the relationship between UBOs and cognitive impairment in NF1. We report two patients (one child and one 39 years old woman) with Legius syndrome and aspecific T2 hyperintense lesions on brain MRI. Thus the presence of such a lesion cannot be used to exclude the diagnosis of Legius syndrome. However at an adult age these lesions are aspecific and not uncommon in the general population. To gain better insight into the prevalence of these and other structural brain lesions in patients with Legius syndrome it would be interesting to systematically perform brain MRI in all patients in whom the diagnosis is made.

Unilateral postaxial polydactyly has been observed both by Messiaen et al. (in one case) and in this report (two cases) to be associated with Legius syndrome. Combining the data in the literature with that of the current report clinical details of 142 individuals with a SPRED1 mutation have been described [START_REF] Brems | Germline loss-of-function mutations in SPRED1 cause a neurofibromatosis 1-like phenotype[END_REF][START_REF] Messiaen | Clinical and mutational spectrum of neurofibromatosis type 1-like syndrome[END_REF][START_REF] Muram-Zborovski | SPRED1 Mutations in a Neurofibromatosis Clinic[END_REF]Pasmant et al., 2009b;[START_REF] Spurlock | SPRED1 mutations (Legius syndrome): another clinically useful genotype for dissecting the neurofibromatosis type 1 phenotype[END_REF]. According to the EUROCAT data the prevalence of any type of polydactyly at birth in the European member states was 8.11 cases per 10000 births in the 2000-2007 period. The highest prevalence in a specific region of the European Union in that time frame was 15 cases per 10000 births (Strasbourg, France). Comparing the prevalence of polydactyly in Legius syndrome (3/142) with the maximal birth prevalence in the European Union (15/10000) results in a significant difference (p= .0014 for 3 or more cases in a group of 142, binomial distribution). It is interesting to note that a similar figure was reported in an Italian study in children with NF1. Ruggieri et al. reported polydactyly in 4 children in a total group of 135 children with NF1 [START_REF] Ruggieri | Congenital bone malformations in patients with neurofibromatosis type 1 (Nf1)[END_REF].

Germline SPRED1 mutations are found in all exons of the gene and although some recurrent mutations have been reported, no clear mutational hotspots are present. The majority of reported SPRED1 mutations are predicted to result in a premature stop codon (nonsense, frameshift, splice-site, out-of-frame insertions and deletions). One in-frame deletion and 11 different missense mutations have been reported. By means of functional analyses 2 missense mutations were classified as pathogenic and 7 as rare benign variants. [START_REF] Messiaen | Clinical and mutational spectrum of neurofibromatosis type 1-like syndrome[END_REF]. Two missense mutations were not characterized (Pasmant et al, 2009b[START_REF] Spurlock | SPRED1 mutations (Legius syndrome): another clinically useful genotype for dissecting the neurofibromatosis type 1 phenotype[END_REF]. We characterized an additional missense mutation and classify this Trp31Cys mutation as pathogenic based on de novo occurrence in Combining the data in this report and previous publications, one can conclude that the highest chances of finding a SPRED1 mutation are in familial cases of CALM with or without freckling. Sporadic cases of CALM are more likely due to mosaicism for NF1 [START_REF] Kehrer-Sawatzki | Mosaicism in sporadic neurofibromatosis type 1: variations on a theme common to other hereditary cancer syndromes?[END_REF]. Although the diagnosis of NF1 is made clinically based on the NIH criteria, the importance of mutation analysis for genetic counselling is increasing with the discovery of allelic and non-allelic NF1 variants. Especially in young children the diagnosis of NF1 can be difficult since only approximately half of children with NF1 and no known family history meet the NIH criteria by age one year, because many features of NF1 increase in frequency with age. The more general availability of NF1 mutation analysis allows for more general use of NF1 mutation testing also in young children. Children with typical multiple CALM who test negative for NF1 are candidates for SPRED1 mutation analysis. In sporadic cases the yield will be low (2.4%) [START_REF] Messiaen | Clinical and mutational spectrum of neurofibromatosis type 1-like syndrome[END_REF]. In children testing negative for mutations in both NF1 and SPRED1 mosaicism for NF1 should be suspected [START_REF] Maertens | Molecular dissection of isolated disease features in mosaic neurofibromatosis type 1[END_REF]. As has been shown in this and previous reports Legius syndrome is associated with a milder phenotype than NF1. Likewise a mild NF1 variant associated with a 3-basepair inframe deletion of exon 17 (c.2970-2972 delAAT) has been described in which neurofibromas are rare and multiple CALM may be the only apparent manifestation [START_REF] Upadhyaya | An absence of cutaneous neurofibromas associated with a 3-bp inframe deletion in exon 17 of the NF1 gene (c.2970-2972 delAAT): evidence of a clinically significant NF1 genotype-phenotype correlation[END_REF]. In contrast, patients with a microdeletion of the NF1 region tend to have a more severe phenotype associated with large numbers and more early appearance of cutaneous neurofibromas, a higher risk for development of malignant peripheral nerve sheath tumors, more severe cognitive impairment and sometimes somatic overgrowth with large hands and feet and dysmorphic facial features [START_REF] Mensink | Connective tissue dysplasia in five new patients with NF1 microdeletions: further expansion of phenotype and review of the literature[END_REF].

In conclusion, we report clinical details of 30 probands from 14 families with pathogenic SPRED1 mutations. Six novel germline mutations were found. The p.Trp31Cys missense mutation is a pathogenic missense mutation. Our results confirm previous reports that Legius syndrome shares clinical features with NF1 but has a milder phenotype, although serious problems can be present such as learning difficulties. Therefore we can recommend less stringent surveillance of these patients than for patients with NF1. We would recommend routine screening for developmental delays and behavioural and learning problems. However physical examination by a clinical geneticist or physician familiar with Legius syndrome every 3 years during childhood seems sufficient. A possible association with polydactyly is suggested by the finding of two cases in this report and one in a previous report.

  Received <date>; accepted revised manuscript <date>.

  amino acid conservation and functional analysis.

Table 1 :

 1 SPRED1 mutations in fourteen families with Legius syndrome

	Family	Exon	Nucleotide change	Amino acid change	Inheritance
	1	3	c.52C>T	p.Arg18X	sporadic b
	2	3	c.70C>T	p.Arg24X	familial
	3	3	c.93G>T	p.Trp31Cys	de novo
	4	3	c.190C>T	p.Arg64X	familial
	5	3	c.190C>T	p.Arg64X	sporadic b
	6	4	c.304dupA a	p.Thr102AsnfsX7	familial
	7	4	c.326_329dup	p.Arg110SerfsX2	familial
	8	4	c.349C>T	p.Arg117X	familial
	9	4	c.360dupA	p.Glu121ArgfsX13	familial
	10	6	c.576_580dup	p.Gln194ProfsX4	familial
	11	8	c.940C>T	p.Gln314X	familial b
	12	8	c.1045_1046del	p.Arg349GlyfsX11	familial
	13	8	c.1048_1060del	p.Gly350MetfsX52	familial
	14	8	c.1149_1152del	p.Gly385IlefsX20	familial
	Mutation numbering was based on the cDNA sequence with +1 corresponding to the A of the ATG translation
	initiation codon in the reference sequence (GenBank accession code: NM_152594.2). For protein numbering the
	initiation codon is codon 1 (NP_689807.1).
	Bold: novel mutations
	a: This mutation has already been reported as a somatic mutation in melanocytes of a patient with Legius
	syndrome
	b: no DNA from family members available to prove sporadic or familial occurrence of the mutation

Table 2 :

 2 Clinical features in 14 families with Legius syndrome

							Human Mutation				Page 8 of 15
	Patient Age	CALM Freckling Height:	Head	Dysmorphic	Psychomotor	Learning	Behavioral	Type of	Other	Other
		(y)/			SD	circum-	features	development	difficulties	problems	education	diagnosis
		gender				ference:						considered
						SD
	Family
	1
	I1	12/F	>5	inguinal	+0.65	+0.76	Hypertelorism Normal	Dyslexia,	No	Special	NF1	Congenital
									mathematics				hypothyroidism
	Family
	2
	I1	51/M	>5	None	-2.16	+1.94	None	U	No	Rigid, sad,	Normal	No	Generalized
										drowsy as			epilepsy since
										consequence			age 39y,
										of			Parkinson
										Parkinsonism			disease since age
													45y, MRI:
													lesions nucleus
													caudatus, relative
													macrocephaly,
													Surinamese-
													Indian origin
	II1	18/M	>5	Axillary	-1.76	+1.33	Low posterior	Normal	Speech	Concentration	Normal	NF1	Relative
							hairline		problems	problems and			macrocephaly,
										hyperactive,			Surinamese-
										no diagnosis			Indian origin
										of ADHD
	Family
	3
	I1	15/M	>5	None	+0.62	+1.55	Hypertelorism,	Motor and	Yes	ADHD	Special	NF1	Eczema first
							downslanting	language					year, asthma,
							palpebral	delay					strabismus
							fissures,
							ptosis, low
							implanted
							posteriorly
							John Wiley & Sons, Inc.

SD: standard deviation; U: unknown; L: left; R: right; MRI: magnetic resonance imaging; ADHD: attention deficit hyperactivity disorder; FSIQ: full-scale intelligence quotient; VIQ: verbal intelligence quotient; PIQ: performance intelligence quotient; IUGR: intrauterine growth retardation *: clinical phenotype present, but no mutation analysis performed in this patient Page 13 of 15 John Wiley & Sons, Inc. HUMAN MUTATION Mutation in Brief #____ (20XX) Online © 2010 WILEY-LISS, INC.

<First Author et al.>

Contract grant sponsor: ED is aspirant of the Fonds voor Wetenschappelijk Onderzoek (FWO)-Vlaanderen. MC was supported by a grant from the Foundation for Polish Science. HB is supported by the Institute for the Promotion of Innovation through Science and Technology in Flanders (IWT-Vlaanderen). This work is supported by research grants from the FWO Vlaanderen (G.0578.06 and G.0551.08 to EL); the Interuniversitary Attraction Poles (IAP) granted by the Federal Office for Scientific, Technical and Cultural Affairs, Belgium (2007-2011; P6/05) (EL) and by a Concerted Action Grant from the KULeuven (EL).This study was supported by Grants-in-Aid from the Ministry of Education, Culture, Sports, Science and Technology of Japan and the Program for Promotion of Fundamental Studies in Health Sciences of the National Institute of Biomedical Innovation (NIBIO). TYKS evo grant to PS.