19.15. Теорема

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

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

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

такие, что:

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

  <FRAME, S1⚪ .. SN⚪> = FRAME⋓⚪

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

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

<FRAME, S1◎ .. SN◎> = FRAME⋓◎

являющийся ЛИБО-прообразом FRAME⋓⚪.

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

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

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

c⋓⚪ = <nd0, nd1 .. ndN, S0⚪, S1⚪ .. SN⚪, k >

системы SVS⚪, а также прообразы S1⚪ .. SN⚪ - множеств состояний S1◎ .. SN◎. Тогда согласно результатам теоремы 19.2 и теоремы 19.3 , не только, существует такая ЛИБО- / И-ЛИБО-ячейка

c⋓◎ = <nd0, nd1 .. ndN, S0◎, S1◎ .. SN◎, k >,

но она при этом является ЛИБО- / И-ЛИБО-прообразом c⋓⚪.

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

Назад Вперёд