symbolic discharge: universals over infinite domains decided by intervals

1 files changed, 12 insertions, 4 deletions

diff --git a/docs/vm.org b/docs/vm.org
index 446cee2..a51b85a 100644
--- a/docs/vm.org
+++ b/docs/vm.org
@@ -96,10 +96,18 @@ open goals cannot happen.
 =Exists= lowers to a conjunction at loading, since query variables
 are existential already; its =variable:= is renamed apart so the
 scope cannot be forged. =ForAll= runs when its quantifier is
-decidable: every solution of the quantifier must satisfy the body. A
-universal over an infinite domain is a non total plan, rejected, as
-decision 10 requires. Variables that live only under a universal are
-not answer variables.
+decidable: every solution of the quantifier must satisfy the body.
+Variables that live only under a universal are not answer variables.
+
+A universal over an infinite domain is never enumerated. It gets one
+chance at symbolic discharge: when quantifier and body both read as
+kind and interval constraints over the quantified variable, the
+engine decides entailment algebraically. Every natural is at least
+zero: proven. Not every integer is: refuted, and the refutation is
+backed by a concrete counterexample. Every integer is a rational:
+proven, which is decision 12's subtype inclusion decided
+symbolically. A universal outside that fragment is a non total plan,
+rejected, as decision 10 requires.
 
 * Membership criteria as domains