Editing Tree automaton (section)

=== Pumping lemma ===

Every sufficiently large<ref>Formally: ''[[Term (logic)#Operations with terms|height]]''(''t'') > ''k'', with ''k'' > 0 depending only on ''L'', not on ''t''</ref> ground term ''t'' in a recognizable tree language ''L'' can be vertically tripartited<ref>Formally: there is a context ''C''[.], a nontrivial context {{math|''C&prime;''[.]}}, and a ground term ''u'' such that {{math|1=''t'' = ''C''[''C&prime;''[''u'']]}}. A "context" ''C''[.] is a tree with one hole (or, correspondingly, a term with one occurrence of one variable). A context is called "trivial" if the tree consists only of the hole node (or, correspondingly, if the term is just the variable). The notation ''C''[''t''] means the result of inserting the tree ''t'' into the hole of ''C''[.] (or, correspondingly, [[Ground instance|instantiating]] the variable to ''t''). {{harvnb|Comon et al.|2008|p=17}}, gives a formal definition.</ref> such that arbitrary repetition ("pumping") of the middle part keeps the resulting term in ''L''.<ref>Formally: {{math|''C''[''C&prime;''<sup>''n''</sup>[''u'']] ∈ ''L''}} for all ''n'' ≥ 0. The notation ''C''<sup>''n''</sup>[.] means the result of stacking ''n'' copies of ''C''[.] one in another, cf. {{harvnb|Comon et al.|2008|p=17}}.</ref>{{sfn|Comon et al.|2008|loc=sect. 1.2, p. 29}}

For the language of all finite lists of boolean values from the above example, all terms beyond the height limit ''k''=2 can be pumped, since they need to contain an occurrence of {{color|#800000|''cons''}}. For example,

:{|
|-
| {{color|#800000|''cons''}}({{color|#800000|''false''}},
| {{color|#800000|''cons''}}({{color|#800000|''true''}},{{color|#800000|''nil''}})
| )
| ,
|-
| {{color|#800000|''cons''}}({{color|#800000|''false''}},{{color|#800000|''cons''}}({{color|#800000|''false''}},
| {{color|#800000|''cons''}}({{color|#800000|''true''}},{{color|#800000|''nil''}})
| ))
| ,
|-
| {{color|#800000|''cons''}}({{color|#800000|''false''}},{{color|#800000|''cons''}}({{color|#800000|''false''}},{{color|#800000|''cons''}}({{color|#800000|''false''}},
| {{color|#800000|''cons''}}({{color|#800000|''true''}},{{color|#800000|''nil''}})
| )))
| , ...
|}

all belong to that language.