Отвергнутая теорема заслоняет прямой путь: пока она стоит, ядро считает её, а не сводит цель с телом

Если при утверждении написана теорема, ядро идёт по ней. Не сошлась — вердикта нет, и путь «сведение цели с телом функции», которым то же утверждение закрывается БЕЗ теоремы, не пробуется вовсе.

Отсюда механическое правило, дешевле любой правки ядра: прежде чем чинить ядро, снимите теорему и спросите ядро заново.

Чем подтверждено, числом. Замер двадцати функций (docs/benchmark2), ветка vypusk/dvadcat. Из пяти файлов, закрытых за работу, ЧЕТЫРЕ закрылись снятием теоремы — правки ядра для них не понадобилось совсем:

• 06 «Приписать в начало» и 18 «Приписать строку в начало» — теорема стояла с индукция по элементы, а тело у обеих СВЁРТКА, и посылки у свёртки называются иначе («начало свёртки», «шаг свёртки»), так что база с живыми именами примером не закрывалась. Без теоремы цель берёт правило «свёртка, растущая ровно на один»;
• 11 «Уникальные» — то же, цель берёт «свёртка, растущая не быстрее списка»;
• 03 «Вписать» — теорема шла индукция по звенья, а тело добавить … к (свёртка …), то есть ни разбор, ни свёртка на верхнем уровне.

Чем ограничено. Речь про случай, когда теорема ОТВЕРГНУТА. Принятая теорема ничего не заслоняет, а даёт вердикт сама.

Связано: auto-induction-on-match-closes-nine, left-fold-gives-no-list-induction