18.7. Теорема

Пусть даны:

• согласованная система ВС SVS = <T, SH, COM, SEL, VS>
• фрейм FRAME её дерева T на выделенных вершинах {nd1 .. ndM} = ND
• базовые и/или частичные ВС vs1 .. vsM сопряжены с вершинами nd1 .. ndM
• к vs1 .. vsM принадлежат состояния s1 .. sM

Тогда утверждение об И-сопряжённости указанных s1 .. sM равносильно утверждению о существовании И-фрейма <FRAME, s1 .. sM> = FRAME⋒.

Доказательство

Вначале дадим развёрнутые определения, конкретизирующие условия теоремы

1. согласно определению 15.2 И-сопряжённость указанных s1 .. sM означает существование в корневой ВС vs⋔0 всей SVS некоторого состояния s⋔0, порожденного сразу от всех s1 .. sM.
2. согласно лемме 18.1 и определению 18.4 И-фрейма , с его корнем nd0 сопряжена ВС vs0, содержащая состояние s0, порожденное от s1 .. sM

Теперь требуется проверить два следующих утверждения:

1. из наличия И-фрейма следует И-сопряжённость указанных состояний, что верно, поскольку в согласованная системе из существования s0 следует существование порожденных от него состояний в каждой вышестоящей, в том числе и корневой ВС vs⋔0, а значит порожденных и от всех s1 .. sM; то есть s1 .. sM являются И-сопряжёнными, что и требовалось доказать
2. из И-сопряжённости состояний следует существование И-фрейма, что верно, поскольку:
   1. существование в корневой ВС vs⋔0 некого состояния s⋔0, порожденного от всех s1 .. sM, означает, что и в ВС, сопряжённых с корнем nd0 фрейма, также существует его предок s0, также порожденный от s1 .. sM, так как у s⋔0 нет другого способа быть порожденным от s1 .. sM
   2. далее по индукции используя результат теоремы 18.2 можно доказать, что для каждой ячейки указанного фрейма можно построить сопряжённую с ней И-ячейку так, что у соподчинённых ячеек будет существовать общее состояние, что будет означать существование И-фрейма, что и требовалось доказать

█

Замечание 18.2

По сути, это другое определение косвенного (порождённого) отношения И. █

Назад Вперёд