mutual recursion admitted under lexicographic measures

1 files changed, 8 insertions, 6 deletions

diff --git a/docs/virtual-machine-specification.org b/docs/virtual-machine-specification.org
index f70f459..c44b666 100644
--- a/docs/virtual-machine-specification.org
+++ b/docs/virtual-machine-specification.org
@@ -74,10 +74,12 @@ fact.
 The engine terminates on every admitted program. The argument, each
 piece machine checkable and one piece machine checked today:
 
-1. every rule that unfolds recursively has a witness whose argument
-   is ground and strictly contained in the head's at each unfolding;
-2. strict containment decreases a natural measure, and the induced
-   order is well founded: proven in =theories/Decrease.v=;
+1. every rule that unfolds recursively carries its component's
+   lexicographic measure, all positions ground at unfolding, and
+   every call cycle through the component strictly decreases it;
+2. strict containment decreases a natural measure, the induced
+   order is well founded (proven in =theories/Decrease.v=), and the
+   lexicographic product of well founded orders is well founded;
 3. tables are finite, builtins decide or defer without search, and
    bounded generators enumerate finite ranges;
 4. disjunction and rule choice branch finitely.
@@ -136,8 +138,8 @@ without changing admitted semantics:
   infinite domains, and arithmetic decrease measures for recursion
   that structural containment cannot see;
 - Rocq certificates as admission evidence, and extraction of the
-  checker itself;
-- mutual recursion under lexicographic measures;
+  lexicographic search itself (the containment core is already
+  extracted);
 - lowering of finite first order subplans to RNT's =Plan.t= algebra
   with Sakura's cardinality tags, per decision 9;
 - tabling for shared subderivations, an optimization the pure