Базисы допустимых правил вывода табличных модальных логик глубины $2$

Доказывается
Теорема. Любая табличная модальная логика $\lambda$ глубины $2$ над $S4$ имеет конечный базис для допустимых правил вывода.
Кроме того, устанавливаются
Лемма 5. Конечная алгебра $\mathcal L\in\mathcal{F}_\omega(\lambda)^Q$ тогда и только тогда, когда существуют числа $n_1,\dots,n_k$такие, что $\mathcal L\preceq(F_{n_1}\sqcup\dots\sqcup F_{n_k})^{+}$.
Пусть $F$ – $\lambda$-фрейм глубины $2$, $b$ – сгусток второго слоя $F$.
Лемма 6. Для любых $n_1,\dots,n_k$ не существует $p$-морфизмов из $(F_{n_1}\sqcup\dots\sqcup F_{n_k})^+$ на $F$ тогда и только тогда, когда существует локальная компонента $K(b)$ из $F$ такая, что для любого $n$ не существует $p$-морфизмов из любой локальной компоненты $F_n$ на $K(b)$.