A quantifier's facts are read inside its body

BREAKING-CHANGES.md

@@ -1523,6 +1523,23 @@ in 2.5.0.
 | `forall a in ZZ : a^7 mod 7 = a mod 7` | `UnhandledParseException` | `True` |
 | `forall a, b in ZZ : (a + b)^5 mod 5 = (a^5 + b^5) mod 5` | `UnhandledParseException` | `True` |
 
+### A quantifier's facts are read inside its body
+
+`forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)` was left as
+written. The claim holds because `p` is prime and `0 < k < p`, and only the quantifiers around it
+say so. A quantifier now hands those facts down while it decides its body: the set its name ranges
+over, and, while the claim is simplified, the conjuncts of the hypothesis. The rule for
+`p divides binomial(p, k)` reads them. Nothing decided with them leaves the quantifier:
+`p divides binomial(p, k)` on its own is still left as written. This is Sullivan and Mackey's
+Prob 8.9.24 for every prime ([#1409](https://github.com/asc-community/AngouriMath/issues/1409)).
+Quantifiers were a parse error in 2.5.0.
+
+| Input | Was (2.5.0) | Now |
+|---|---|---|
+| `forall p in PP : forall k in ZZ : (0 < k and k < p) implies p divides binomial(p, k)` | `UnhandledParseException` | `True` |
+| `forall k in ZZ : forall p in PP : (0 < k and k < p) implies p divides binomial(p, k)` | `UnhandledParseException` | `True` |
+| `forall p in PP : forall k in ZZ+ : k < p implies p divides binomial(p, k)` | `UnhandledParseException` | `True` |
+
 ### `binomial(n, k)` is a function
 
 **Addition, not silent.** The binomial coefficient is a node, `Entity.Binomialf`, spelled

Sources/.editorconfig

@@ -318,6 +318,9 @@ file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed
 [AngouriMath/Functions/Boolean/ProofRecording.cs]
 file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n
 
+[AngouriMath/Functions/Boolean/QuantifierFacts.cs]
+file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n
+
 [Tests/UnitTests/Core/ProofRecordingTest.cs]
 file_header_template=\nCopyright (c) 2019-2026 Angouri.\nAngouriMath is licensed under MIT.\nDetails: https://github.com/asc-community/AngouriMath/blob/master/LICENSE.md.\nWebsite: https://am.angouri.org.\n
 

Sources/AngouriMath/Functions/Boolean/ProofRecording.cs

@@ -142,6 +142,49 @@ internal static int Mark()
                 return recording.steps.Count;
         }
 
+        /// <summary>
+        /// Writes the steps recorded since <paramref name="mark"/> with <paramref name="from"/>
+        /// read as <paramref name="to"/>: a quantifier decides under a name of its own while
+        /// facts are in scope (<see cref="Functions.Boolean.QuantifierFacts"/>), and its steps
+        /// are written under the name it was given.
+        /// </summary>
+        internal static void Rename(int mark, Entity.Variable from, Entity.Variable to)
+        {
+            var recording = current.Value;
+            if (recording is null || recording.closed)
+                return;
+            lock (recording.gate)
+                for (var i = mark; i < recording.steps.Count; i++)
+                {
+                    var step = recording.steps[i];
+                    recording.steps[i] = step with
+                    {
+                        Statement = Functions.Boolean.QuantifierFacts.Renamed(step.Statement, from, to),
+                        Rule = step.Rule.Replace(from.Name, to.Name),
+                        Verdict = Functions.Boolean.QuantifierFacts.Renamed(step.Verdict, from, to),
+                    };
+                }
+        }
+
+        /// <summary>
+        /// Writes the step the decision in progress recorded last, since <paramref name="mark"/>,
+        /// as a step about <paramref name="statement"/> by <paramref name="rule"/>, keeping its
+        /// verdict and depth. A quantifier that decided its body with facts in scope records the
+        /// statement as it was written, rather than the body those facts made of it.
+        /// </summary>
+        internal static void Restate(int mark, Entity statement, string rule, string lemma)
+        {
+            var recording = current.Value;
+            if (recording is null || recording.closed)
+                return;
+            lock (recording.gate)
+            {
+                var last = recording.steps.Count - 1;
+                if (last >= mark && recording.steps[last].Depth == depth)
+                    recording.steps[last] = recording.steps[last] with { Statement = statement, Rule = rule, Lemma = lemma };
+            }
+        }
+
         internal static void Rollback(int mark)
         {
             var recording = current.Value;