Допущение индукции обязано строиться ПО МЕСТУ ВЫЗОВА, иначе рекурсия с другим вторым аргументом не сводится

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

Почему поправка законна, а не поблажка. Доказывается «для всех элементы, для всех сколько», а не «для всех элементы при данном сколько»: прочие параметры стоят в посылке свободными именами, ядро сводит посылку, ничего о них не зная, и потому закрытая посылка закрыта сразу для всех их значений. Значит и допущение о части — тоже «для всех прочих», и взять его при любых прочих аргументах законно. Обычное обобщение по параметру, каким структурная индукция пользуется везде.

Поиска при этом ноль: подстановку называет САМ ВЫЗОВ, стоящий в заключении. Сколько в заключении вызовов себя, столько и допущений — ни одним больше. Тот же приём, каким работают «по свойству» и правило постусловия вызванного.

Четыре условия, и снятие любого — дыра. Спуск (на месте переменной индукции у вызова обязана стоять ровно та часть, что связал образец случая); не под связывателем (пусть, разбор, свёртка, отобразить/отфильтровать); число аргументов совпало; подстановка не захватила имени.

Чем подтверждено. Ветка vypusk/dvadcat, коммит 72fe55e8. Вместе с двумя соседними правками (переписка известными равенствами дошла до правила порядка; замкнутая арифметика считается при нормализации) закрыла файлы 07 «Вставить по» и 09 «Взять первые» замера двадцати.

Связано: what-blocks-the-kernel-now-is-induction-without-a-theorem, a-rejected-theorem-blocks-the-direct-path