Алгебраическая интерпретация полноты аксиом вывода

На полном множестве F-зависимостей $\{X\to Y\mid X,Y\subseteq R\}$ над схемой $R$ введена операция $(X\to Y)\blacktriangleright(Z\to V)=X\cup(Z\setminus Y)\to(Y\cup V)$, и доказано, что все F-зависимости, выводимые из заданного множества $F$, представляются в виде алгебраических выражений $\Phi_1\blacktriangleright\Phi_2\blacktriangleright\ldots \blacktriangleright\Phi_k\blacktriangleright W\cdot\mathbf{F2}\cdot\mathbf{B3}$, в которых $\Phi_i\in F$, $W\subseteq R$ и $\Phi_k\blacktriangleright W=\Phi_k\blacktriangleright (W\to W)$, a $\mathbf{F2}$ (пополнение) и $\mathbf{B3}$ (проективность) — аксиомы вывода ТРБД (теории реляционных баз данных), трактуемые как унарные операции.