Rewrite

recce.ltx

@@ -3080,6 +3080,58 @@ to \var{tp-set} will be the same as the number of attempts to add
 to \var{tp-set2}
 \end{proof}
 
+\begin{definition}
+Let \var{lb-set} be a set of Leo bounds.
+We say that \var{lb-set} has bounded overlap if there is
+a constant \var{c} such that,
+for all \var{lb}, $\var{lb} \in \var{lb-set}$,
+inputs \Vstr{w},
+and locations \Vloc{i},
+\begin{equation}
+\size{\var{lb}(\var{w},\var{i})} \le \var{c}
+\end{equation}
+\end{definition}
+
+Less formally, a set of Leo bounds has bounded overlap if
+there is some fixed limit \var{c}, such that
+for every specific location and input,
+no more than \var{c} of the Leo bounds have tree predicates there.
+
+\begin{definition}
+Let \var{lb-set} be
+a set of Leo bounds.
+Let
+\begin{equation}
+\var{all-inputs} =
+\bigcup_{\var{lb} \in \var{lb-set}}
+{\left\lbrace x \; \middle| \; lb:\var{x} \mapsto \var{y}
+\right\rbrace}
+\end{equation}
+and
+\begin{equation}
+\var{all-predicate-sets} =
+\bigcup_{\var{lb} \in \var{lb-set}}
+{\left\lbrace y \; \middle| \; lb:\var{x} \mapsto \var{y}.
+\right\rbrace}
+\end{equation}
+Then $\var{lb-union} : \var{all-inputs} \mapsto \var{all-predicate-sets}$
+is defined as
+\begin{equation}
+\var{lb-union}(\var{w}) =
+\bigcup_{\var{lb} \in \var{lb-set}}{\var{lb}(\var{w})}.
+\end{equation}
+
+\end{definition}
+
+\begin{theorem}
+The union of a set of Leo bounds which
+are free of right recursion and have bounded overlap
+is also a Leo bound.
+\end{theorem}
+
+\begin{proof}
+\end{proof}
+
 \begin{definition}
 \label{d:grammar-union}
 Let \var{g1} and \var{g2} be two grammars.