Изменения

Даны множества <tex>S</tex> и <tex>P</tex> и пусть для простоты <tex>P \subset S</tex>, необходимо проверить является ли <tex>P</tex> эквивалентным <tex>S</tex>. Для этого достаточно построить замыкание <tex>P^+_S</tex> и по теореме проверить все фз функциональные зависимости из <tex>S</tex>, которые отсутствуют в <tex>P</tex>. Если доказать, что из <tex>P</tex> выводимы все базовые правила <tex>S</tex>, то их замыкания ФЗ будут совпадать, следовательно, два множества эквивалентны. Например, пусть <tex>A \to B \in S, A \to B \not\in P </tex>, тогда если <tex>B \in P_S^+</tex>, то <tex> A \to B \in P^+</tex>.

<tex>(=>)</tex><br>По определению замыкания атрибутов, т.к так как все атрибуты функционально зависят от <tex>X</tex>.<br/>

<tex>A \subset X_S^* => X \to A</tex>(по правилу расщепления, т.к. так как <tex>X_S^*</tex> изначально содержит в себе <tex>X</tex>) <tex>=> X \to B </tex>, то есть <tex>B</tex> входит в замыкание. <br>

Доказательство от обратного: Пусть <tex>X_S^+ \not\subset X_S^* => \exists A: A \in X_S^+ \text{ and } A \not\in X_S^*.\; A \in X_S^+ => X \to A =></tex> есть вывод <tex> X \to X_1^+, ..., X_n^+ \to A</tex>. В этой цепочке найдём первую свежую ФЗ, то есть она не была в базовых ФЗ <tex>X</tex>. Такая фз функциональная зависимость точно есть в этой цепочке, например, <tex>X_n^+ \to A</tex>, т.к. так как <tex>A \in X_S^+ \text{ and } A \not\in X_S^* => </tex> такое правило не могло быть в <tex>X</tex>. Получается, что атрибут A не был добавлен в <tex>X^*_S</tex> в алгоритме, такое может быть только если атрибут A уже содержался в <tex>X => </tex> противоречие.