From e56efc19f71898d798c44b5955fe74451ee0fc6f Mon Sep 17 00:00:00 2001
From: Marcos Magueta <maguetamarcos@gmail.com>
Date: Sun, 12 Jul 2026 10:07:23 -0300
Subject: lexicographic order proven well founded, checker extracted and
 verifying admission

---
 lib/world.ml | 21 +++++++++++++++++++++
 1 file changed, 21 insertions(+)

(limited to 'lib/world.ml')

diff --git a/lib/world.ml b/lib/world.ml
index 8ade9da..a053c2c 100644
--- a/lib/world.ml
+++ b/lib/world.ml
@@ -586,6 +586,27 @@ module Standalone = struct
               in
               match lex_measure calls candidates with
               | None -> Error (Non_total_component members)
+              | Some measure
+                when
+                  (* The search is an untrusted heuristic; the
+                     measure it found is validated call by call with
+                     the lexicographic checker extracted from Rocq,
+                     whose soundness and well-foundedness are
+                     proven. *)
+                  not
+                    (List.for_all
+                       (fun c ->
+                         let project bindings =
+                           List.map
+                             (fun label ->
+                               Pattern.to_checker (Label.Map.find label bindings))
+                             measure
+                         in
+                         Decrease_extracted.lex_ltb Label.equal
+                           Pattern.checker_leaf_equal (project c.args)
+                           (project c.head))
+                       calls) ->
+                  Error (Non_total_component members)
               | Some measure ->
                   Ok
                     (List.fold_left
-- 
cgit v1.2.3