Квантор по соседним парам стоил ДВУХ файлов вместо двадцати девяти — потому что разбор собрал его из уже существующих узлов

Прецедент говорил: одна новая встроенная форма трогает 29 файлов (лексер, разбор, типы, вычислитель, восемь целей печати и их рантаймы). Проверено на этом дереве: у одноместной встроенной формы хвост имя стоит в 16 файлах flang/self, и в каждой из восьми целей печати это ЧЕТЫРЕ правки — таблица имён, арность, исходник функции рантайма и её место в списке кусков рантайма.

Квантор по соседним парам (СПИСОК не убывает) обошёлся двумя файлами: flang/self/parser.flang и flang/self/proof-kernel.flang. Ни типы, ни вычислитель, ни восемь печатей о новой записи не знают ничего.

Как. Разбор не заводит нового вида узла, а СОБИРАЕТ форму из тех, что есть:

(длина (свёртка Л начиная с пустой список как прежнее и текущее →
   если (длина прежнее) равен 0
     то [текущее]
     иначе (если ((длина прежнее) равен 1) и притом ((элемент 1 в прежнее) не больше текущее)
              то [текущее]
              иначе [текущее, текущее]))) не больше 1

Накопитель — список, и его ДЛИНА кодирует три состояния: 0 — ещё ничего не видели, 1 — пока не убывало (и вот последний элемент), 2 — пара уже нарушена. Из состояния 2 выхода нет: условие «длина накопителя равна 1» ложно навсегда. Поэтому «длина накопителя не больше 1» в конце и означает ровно «ни одна пара соседей не пошла вниз». Список при этом упоминается ОДИН раз — сравнение с длина Л потребовало бы двух и удвоило бы работу.

Что это дало, числом. Настоящая «Вставить по порядку» из flang/stdlib/lists.flang — сердце сортировки вставками — получила ДОКАЗАННОЕ постусловие о порядке: «если приписать значение к элементы не убывает, то и результат не убывает», вердикт «доказано индукцией по «список»: база 1 случай, шаг при допущении на частях». По файлу: доказано ядром было 5 из 34 утверждений, стало 6 из 35, индукцией 2 → 3.

Что все восемь целей печати её берут — проверено печатью, а не рассуждением. flang emit … --target на программе с новой записью отвечает кодом 0 во всех восьми целях, а напечатанный C собран и опрошен: [1,2,3] → true, [3,1] → false, пустой → true, [не число, 1] → false. Ни одна печать не правилась ни на строку.

Попутно опровергнута запись базы знаний. В chto-nelzya-napisat-v-obespechivaet сказано: «Перебрать список внутри обеспечивает нечем. Ни свёртки, ни „для каждого“ там нет». Свёртка там ЕСТЬ — проверено прогоном: модуль с шестью примерами и постусловием-свёрткой проходит flang check и flang test без единого замечания. Верно другое: свёртку туда никто не напишет руками (68 токенов на одно утверждение), и ядро её не читает. Дыра была не в выразимости языка, а в ЗАПИСИ и в правилах ядра.

Занятость проверена прогоном, а не глазами. не и убывает — ключевые с первого дня, значит новых слов в языке ноль; занимается МЕСТО — цепочка этих двух ключевых токенов после выражения, которую разбор прежде отвергал (FLANG_PARSE: неожиданное 'убывает'). Прежний word-occupancy.mjs на такой вопрос ответить не мог: он считает только ГОЛЫЕ имена, а ключевое слово голым именем не бывает никогда, и счёт молчал бы нулём независимо от правды. Прогон научен считать ещё и ЦЕПОЧКИ КЛЮЧЕВЫХ: по 477 файлам дерева — 0.

Связано: occupy-a-form-the-parser-already-rejects, a-language-form-must-reach-code-generation, sort-result-is-non-decreasing-is-false-on-not-a-number