Ветка если разворачивается в обе стороны и на второй ярус, а разбор списка — ни в какую

Ходовое знание было такое: даром берётся развёртка ПЕРВОЙ ветки если — условие обещания дословно повторяет условие тела в положительную сторону, — а второй ярус если не берётся. Замер на нынешнем двоичном (bootstrap/flang, ветка b/dokazat-9) показывает, что граница проходит не там: берутся ВСЕ ветви если, сколько бы ярусов ни было, если записать цель дизъюнкцией по условиям, стоящим на пути к ветви.

Тело если A то X иначе если B то Y иначе Z закрывается тремя обещаниями:

обеспечивает «первая» (не A) или (результат равен X)
обеспечивает «средняя» A или ((не B) или (результат равен Y))
обеспечивает «последняя» A или (B или (результат равен Z))

Ядро называет два разных правила и оба считает доказательством: «разбор случаев по внутреннему условию цели» — когда цель начинается с (не A); «разбор цели по условию» — когда с A. Условие обещания обязано повторять условие тела дословно; пусть п равно E перед если не мешает, если подставить E вместо п.

Тем же приёмом берётся ветвь разбора по варианту без полей: (не (шаг равен вариант «Первый»)) или (результат равен "первый") — доказано. Вариант с полями так не взять: имена полей в обещании не связаны.

Где стена. разбор по СПИСКУ (случай пусто / случай голова и хвост) не разворачивается ничем. Проверены обе записи условия — (не (беды равен пустой список)) и (не ((длина беды) равен 0)); обе дали дословно «объявлено, не доказано: ни теоремы, ни примеров».

Что ещё берётся даром (замерено там же, сверх известного списка):

• отфильтровать сп где … → (длина результат) не больше (длина сп), правило «порядок по построению»;
• свёртка, копящая число прибавлением, → результат не меньше 0, правило «неотрицательность по построению» (обещание пустое, годится только в паре);
• признак с телом (P) и притом (Q) → (не результат) или (P) и (не результат) или (Q); с телом (P) или (Q) → (не P) или результат и (не Q) или результат;
• постоянная строка длиной в экран: результат содержит "подстрока" закрывается «вычислением замкнутой цели». А вот постоянный СПИСОК из пятнадцати записей уже не считается: (длина результат) равен 15 осталось «объявлено, не доказано».

Ловушка при этом. Тело не (текст содержит "СЛОВО") не берётся ни в одну сторону — ни (текст содержит "СЛОВО") или (не результат), ни обратное. А пара обещаний, которую всё-таки удаётся доказать про такую функцию, целиком переживает подмену тела на постоянное нет: обе половины — одна и та же импликация, записанная прямо и через противоположное. Доказано — и пусто.

Чем подтверждено. scripts/lsp-check.flang (18 обещаний, доказано 18) и fspec/forgery.flang (18 обещаний, доказано 18); четыре снятых обещания — ровно те, что упёрлись в разбор списка и в постоянный список записей.

Связано: three-of-five-named-postcondition-walls-are-already-gone