Skip to content
Snippets Groups Projects

Add la_mult_pos and la_mult_neg rules

Merged Lachnitt requested to merge Add-la_mult-rules into master
2 unresolved threads
1 file
+ 3
3
Compare changes
  • Side-by-side
  • Inline
+ 3
3
@@ -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}
.
Loading