diff --git a/spec/rule_list.tex b/spec/rule_list.tex index f66db1e84b94afc1defbf7fb34ddf9916949671a..6780d983e132df4164e28c51f42e9ce0dd169f2c 100644 --- a/spec/rule_list.tex +++ b/spec/rule_list.tex @@ -562,7 +562,7 @@ with $\bowtie \in \{<,>, \le,\ge, ≈\}$.\\ \begin{AletheX} $i$. & \ctxsep & - $(t_1 > 0 \wedge \neg (t_2 ≈ t_3)) \to \neg (t_1 * t_2 ≈ t_1 * t_3)$ + $(t_1 > 0 \land \neg (t_2 ≈ t_3)) \rightarrow \neg (t_1 * t_2 ≈ t_1 * t_3)$ & (\currule) \\ \end{AletheX} @@ -574,7 +574,7 @@ Either of the form: \begin{AletheX} $i$. & \ctxsep & - $(t_1 < 0 \wedge t_2 \bowtie t_3) \to t_1 * t_2 \bowtie_{inv} t_1 * t_3$ + $(t_1 < 0 \land t_2 \bowtie t_3) \rightarrow t_1 * t_2 \bowtie_{inv} t_1 * t_3$ & (\currule) \\ \end{AletheX} @@ -598,7 +598,7 @@ Either of the form: \begin{AletheX} $i$. & \ctxsep & - $(t_1 < 0 \wedge \neg (t_2 ≈ t_3)) \to \neg (t_1 * t_2 ≈ t_1 * t_3)$ + $(t_1 < 0 \land \neg (t_2 ≈ t_3)) \rightarrow \neg (t_1 * t_2 ≈ t_1 * t_3)$ & (\currule) \\ \end{AletheX} .