From 04ead7c2f1710dbb24c260df2ca561aecec4dc31 Mon Sep 17 00:00:00 2001
From: =?UTF-8?q?Hans-J=C3=B6rg?= <hansjoergschurr@users.noreply.github.com>
Date: Wed, 20 Sep 2023 19:10:48 -0500
Subject: [PATCH] Fix typos and description of rules (#9920)

The biggest change is to the FACTORING rule, since the current
description implies that not necessary all duplicates are removed
and that the order can change.
---
 src/proof/proof_rule.h | 12 ++++++------
 1 file changed, 6 insertions(+), 6 deletions(-)

diff --git a/src/proof/proof_rule.h b/src/proof/proof_rule.h
index 99a90308e1d..7627ae70205 100644
--- a/src/proof/proof_rule.h
+++ b/src/proof/proof_rule.h
@@ -532,9 +532,9 @@ enum class PfRule : uint32_t
    * .. math::
    *   \inferrule{C_1 \mid -}{C_2}
    *
-   * where the set representations of :math:`C_1` and :math:`C_2` are the same
-   * and the number of literals in :math:`C_2` is smaller than that of
-   * :math:`C_1`. \endverbatim
+   * where :math:`C_2` is the clause :math:`C_1`, but every occurence of a literal
+   * after its first occurence is omitted.
+   * \endverbatim
    */
   FACTORING,
   /**
@@ -566,7 +566,7 @@ enum class PfRule : uint32_t
    *   :math:`pol`, as defined in
    *   :cpp:enumerator:`RESOLUTION <cvc5::internal::PfRule::RESOLUTION>`
    * - let :math:`C_1'` be equal, in its set representation, to :math:`C_1`,
-   * - for each :math:`i > 1`, let :math:`C_i'` be equal, it its set
+   * - for each :math:`i > 1`, let :math:`C_i'` be equal, in its set
    *   representation, to :math:`C_{i-1} \diamond{L_{i-1},\mathit{pol}_{i-1}}
    *   C_i'`
    *
@@ -1028,7 +1028,7 @@ enum class PfRule : uint32_t
    *
    * .. math::
    *   \inferrule{- \mid (\ite{C}{F_1}{F_2})}{(\ite{C}{F_1}{F_2}) \lor \neg C
-   *   \lor \not F_1}
+   *   \lor \neg F_1}
    *
    * \endverbatim
    */
@@ -1062,7 +1062,7 @@ enum class PfRule : uint32_t
    *
    * .. math::
    *
-   *   \inferrule{-\mid t}{t = t)}
+   *   \inferrule{-\mid t}{t = t}
    * \endverbatim
    */
   REFL,