19.13. Теорема

Пусть даны согласованные системы ВС

SVS⚪ = <T⚪, SH⚪, COM⚪, SEL⚪, VS⚪> и

SVS◎ = <T◎, SH◎, COM◎, SEL◎, VS◎>

такие, что:

• их основы [SVS⚪] и [SVS◎] находятся в отношении О-проекции
• для деревьев T⚪ и T◎ определён один и тот же фрейм FRAME на выделенных вершинах nd0, nd1 .. ndN.
• на этом фрейме как на основе в системе SVS⚪ построен И-фрейм

  <FRAME, s1⚪ .. sM⚪> = FRAME⋒⚪

• состояния, s1⚪ .. sM⚪ являются проекциями состояний s1◎ .. sM◎, которые принадлежат ВС, сопряжённым с теми же листьями фрейма FRAME, но уже в системе SVS◎.

Тогда в системе SVS◎ на этом фрейме как на основе также может быть построен И-фрейм

<FRAME, s1◎ .. sM◎> = FRAME⋒◎

находящийся в отношении И-проекции-прообраза между FRAME⋒⚪ и FRAME⋒◎

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

Сравним работу алгоритма 19.4 при построении с его помощью И-фреймов FRAME⋒⚪ и FRAME⋒◎. Его применимость к FRAME⋒⚪ задана условием теоремы, а для FRAME⋒◎ надо предварительно доказать существование очередной И-ячейки c⋒◎.

Пусть для очередного шага определена И-ячейка

c⋒⚪ = <nd0, nd1 .. ndN, s0⚪, s1⚪ .. sN⚪, k >

системы SVS⚪, а также прообразы s1⚪ .. sN⚪ - состояния s1◎ .. sN◎.

Тогда согласно результатам теоремы 19.2, не только, существует такая И-ячейкиа

c⋒◎ = <nd0, nd1 .. ndN, s0◎, s1◎ .. sN◎, k >,

но она при этом является также и прообразом c⋒⚪.

Значит, существует и "сумма" таких И-ячеек – И-фрейм FRAME⋒◎, являющийся И-прообразом FRAME⋒⚪. █

Назад Вперёд