Make the description of the comp_simplify rule clearer

By changing the variable names we clarify that those are rules that can match.

Furthermore, we also change all occurrences of the very awkward "as long as possible" to "until a fixed point is reached".

spec/rule_list.tex

@@ -110,7 +110,7 @@ to quickly find the definition of rules.
   Rule & Description \\
   \hline
 \ruleref{la_generic} & Tautologous disjunction of linear inequalities. \\
-\ruleref{KIA_generic} & Tautologous disjunction of linear integer inequalities. \\
+\ruleref{lia_generic} & Tautologous disjunction of linear integer inequalities. \\
 \ruleref{la_disequality} & $t_1 ≈ t_2 \lor \neg (t_1 \leq t_2) \lor \neg (t_2 \leq t_1)$ \\
 \ruleref{la_totality} & $t_1 \leq t_2 \lor t_2 \leq t_1$ \\
 \ruleref{la_tautology} & A trivial linear tautology. \\