Fix text around least upper bound.

docs/language/dartLangSpec.tex

Index: docs/language/dartLangSpec.tex
diff --git a/docs/language/dartLangSpec.tex b/docs/language/dartLangSpec.tex
index 62dba6983699c047c42906215f334947d686c81b..3d43547c24ba8f1babdbfaf02fa3754a1d8256d2 100644
--- a/docs/language/dartLangSpec.tex
+++ b/docs/language/dartLangSpec.tex
@@ -7791,8 +7791,18 @@ Let $T$ be the declared type of a declaration $d$, as it appears in the program
 
 \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{}.
@@ -7801,7 +7811,8 @@ 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