403
правки
Изменения
→Время работы
|id = Лемма1
|statement =
Количество классов, созданных во время выполнения алгоритма, не превышает <tex>2 |Q| - 1</tex>.
|proof =
Представим дерево, которое соответствует операциям разделения классов на подклассы. Корнем этого дерева является все множество состояний <tex>Q</tex>. Листьями являются классы эквивалентности, оставшиеся после работы алгоритма. Так как дерево бинарное {{---}} каждый класс может породить лишь два новых, а количество листьев не может быть больше <tex>|Q|</tex>, то количество узлов этого дерева не может быть больше <tex>2 |Q| - 1</tex>, что доказывает утверждение леммы.
}}
{{Лемма
|about = 2
|id = Лемма2
|statement =
Количество итераций цикла <tex>while</tex> не превышает <tex> 2 |\Sigma| |Q| </tex>.
|proof =
Для доказательства этого утверждения достаточно показать, что количество пар <tex>(C,a)</tex> добавленных в очередь <tex>S</tex> не превосходит <tex> 2 |\Sigma| |Q| </tex>, так как на каждой итерации мы извлекаем одну пару из очереди.
По [[#Лемма1 | лемме(1)]] количество классов не превосходит <tex>2 |Q| - 1</tex>. Пусть <tex>C</tex> элемент текущего разбиения. Тогда количество пар <tex>(C,a), \ a \in \Sigma</tex> не может быть больше <tex>|\Sigma|</tex>. Отсюда следует, что всего различных пар, которые можно добавить в очередь, не превосходит <tex> 2 |\Sigma| |Q| </tex>.
}}
