Fix text around least upper bound.

docs/language/dartLangSpec.tex

 \documentclass{article}
 \usepackage{epsfig}
 \usepackage{color}
 \usepackage{dart}
 \usepackage{bnf}
 \usepackage{hyperref}
 \usepackage{lmodern}
 \usepackage[T1]{fontenc}
 \newcommand{\code}[1]{{\sf #1}}
 \title{Dart Programming Language  Specification  \\
@@ skipping 7773 matching lines @@
 \begin{itemize}
 \item  $[A_1, \ldots, A_n/U_1, \ldots, U_n]T$ if $d$ depends on type parameters $U_1, \ldots, U_n$, and $A_i$ is the value of $U_i, 1 \le i \le n$.
 \item $T$ otherwise.
 \end{itemize}
 
 \subsubsection{Least Upper Bounds}
 \LMLabel{leastUpperBounds}
 
 \LMHash{}
 % does this diverge in some cases?
-Given two interfaces $I$ and $J$, let $S_I$ be the set of superinterfaces of $I$,  let $S_J$ be the set of superinterfaces of $J$ and let $S =  (I \cup S_I) \cap (J \cup S_J)$.  Furthermore, we define $S_n = \{T | T \in S  \wedge depth(T) =n\}$ for any finite $n$ %, and $k=max(depth(T_1), \ldots, depth(T_m)), T_i \in S, i \in 1..m$,
-where $depth(T)$ is the number of steps in the longest inheritance path from $T$ to \code{Object}. Let $q$ be the largest number such that $S_q$ has cardinality one. The least upper bound of $I$ and $J$ is the sole element of  $S_q$.
+Given two interfaces $I$ and $J$,
+let $S_I$ be the set of superinterfaces of $I$,
+let $S_J$ be the set of superinterfaces of $J$
+and let $S = (\{I\} \cup S_I) \cap (\{J\} \cup S_J)$.
+Furthermore,
+we define $S_n = \{T | T \in S \wedge depth(T) = n\}$ for any finite $n$
+where $depth(T)$ is the number of steps in the longest inheritance path
+from $T$ to \code{Object}.
+%TODO(lrn): Specify that "inheritance path" is a path in the superinterface graph.
+Let $q$ be the largest number such that $S_q$ has cardinality one,
+which must exist because $S_0$ is $\{\code{Object}\}$.
+The least upper bound of $I$ and $J$ is the sole element of $S_q$.
 
 \LMHash{}
 The least upper bound of \DYNAMIC{} and any type $T$ is \DYNAMIC{}.
 The least upper bound of \VOID{} and any type $T \ne \DYNAMIC{}$ is \VOID{}.
 The least upper bound of $\bot$ and any type $T$ is $T$.
 Let $U$ be a type variable with upper bound $B$. The least upper bound of $U$ and a type $T \ne \bot$ is the least upper bound of $B$ and $T$.
 
 \LMHash{}
-The least upper bound relation is symmetric and reflexive.
+The least upper bound operation is commutative and idempotent,
+but it is not associative.
 
 % Function types
 
 \LMHash{}
 The least upper bound of a function type and an interface type $T$ is the least upper bound of \cd{Function} and $T$.
 Let $F$ and $G$ be function types. If $F$ and $G$ differ in their number of required parameters, then the least upper bound of $F$ and $G$ is \cd{Function}.  Otherwise:
 \begin{itemize}
 \item If
 
 $F= (T_1 \ldots T_r, [T_{r+1}, \ldots, T_n]) \longrightarrow T_0$,
@@ skipping 318 matching lines @@
 
 The invariant that each normative paragraph is associated with a line
 containing the text \LMHash{} should be maintained.  Extra occurrences
 of \LMHash{} can be added if needed, e.g., in order to make
 individual \item{}s in itemized lists addressable.  Each \LM.. command
 must occur on a separate line.  \LMHash{} must occur immediately
 before the associated paragraph, and \LMLabel must occur immediately
 after the associated \section{}, \subsection{} etc.
 
 ----------------------------------------------------------------------