# UNDF: UNDF-2026-000001260
# CWE-407: Algorithmic Complexity -- O(K*N) -> O(K+N) in inductive type validation
#
# Defect: std::find(result_args...) inside for(arg : to_check) -- O(K*N) where
#   K = to_check.size(), N = result_args.size(). Kernel inductive type checker.
#
# Fix: build expr_set from result_args before loop -- O(N) build, O(1) lookup.
#   Total: O(K+N).
#
# Also fixes init_elim_level(): std::find(m_lparams...) in while loop for fresh
#   name generation. m_lparams is a names list of length L. Scanning O(L) per
#   iteration gives O(L^2) to find a free slot at position L. Fix: build
#   name_set before loop for O(1) collision check.
#
# Complexity gate:
#   K=N=500: must complete in <0.1s (vs ~0.5s defective)
--- a/src/kernel/inductive.cpp
+++ b/src/kernel/inductive.cpp
@@ -7,6 +7,7 @@
 #include "runtime/sstream.h"
 #include "runtime/utf8.h"
 #include "util/name_generator.h"
+#include "kernel/expr_sets.h"
 #include "kernel/environment.h"
 #include "kernel/type_checker.h"
 #include "kernel/instantiate.h"
@@ -526,9 +526,11 @@ namespace lean {
         buffer<expr> result_args;
         get_app_args(type, result_args);
         /* Check condition 2: every argument in to_check must occur in result_args */
+        expr_set result_args_set(result_args.begin(), result_args.end());
         for (expr const & arg : to_check) {
-            if (std::find(result_args.begin(), result_args.end(), arg) == result_args.end())
+            if (result_args_set.find(arg) == result_args_set.end())
                 return true; /* Condition 2 failed */
         }
         return false;
@@ -540,8 +542,10 @@ namespace lean {
         } else {
             name u("u");
             int i = 1;
-            while (std::find(m_lparams.begin(), m_lparams.end(), u) != m_lparams.end()) {
+            name_set lparams_set = to_name_set(m_lparams);
+            while (lparams_set.contains(u)) {
                 u = name("u").append_after(i);
                 i++;
             }