19.2. Теорема

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

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

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

такие, что

• их основы [SVS⚪] и [SVS◎] находятся в отношении О-проекции
• nd0 из T⚪ и T◎ является И-узлом с коммутатором com из COM⚪ и COM◎
• для деревьев T⚪ и T◎ определена одна и та же ячейка

  c = <nd0, nd1, .. , ndN>

• vs0⚪ сопряжена с nd0, в T⚪, а vs0◎ – в T◎
• vs1⚪ .. vsN⚪ – системообразующие ВС, сопряженные с nd1 .. ndN в SVS⚪, а vs1◎ .. vsN◎ – в SVS◎
• s1⚪ ∈ [vs1⚪], .. , sN⚪ ∈ [vsN⚪]
• {s0⚪} - множество состояний vs0⚪, порождённых от s1⚪ .. sN⚪
• ключ коммутатора k ∈ com
• на ячейке c как на основе построена в системе SVS⚪ И-ячейка

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

• в соответствующих системообразующих ВС vs1◎ .. vsN◎ из SVS◎ имеются некоторые

  s1◎ ∈ vs1◎, .. , sN◎ ∈ vsN◎

  являющиеся произвольными прообразами указанных s1⚪ .. sN⚪

• s1⚪ ⊴ s1◎, .. , sN⚪ ⊴ sN◎

Тогда в vs0◎, сопряженной с узлом nd0, существует состояние s0◎, являющееся не только порождением от s1◎, .. , sN◎, но в силу этого также и прообразом для s0⚪.

Тем самым существует также И-ячейка

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

являющаяся прообразом (И-ячейки) c⋔⚪:

c⋔⚪ ⊴ c⋔◎

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

Согласно теореме 16.3 и замечанию 19.1 отношение О-проекции означает, что переход от [SVS⚪] к [SVS◎] можно разбить на ряд ЭШ, на каждом из которых меняются ВС только одного пути от ndi до nd0, а ВС остальных путей остаются неизменными.

Следовательно, достаточно доказать, что на любом ЭШ при переходе указанного в условии состояния si⚪ из vsi⚪к его прообразу si◎ из vsi◎, в vs0◎ найдётся состояние si◎, являющееся прообразом s0⚪.

Для этого достаточно заметить однотипность построения s0⚪ и s0◎, не зависящую от типа ЭШ, что было зафиксировано в алгоритме 14 построения системообразующих ВС vs0⚪и vs0◎, сопряжённых с nd0: каждое из этих состояний есть произведение

(si⚪ либо si◎) ✖ ∏kj ✖ ∏sjj, где

• ∏kj - произведение всевозможных ключей коммутаторов на пути от ndi до nd0, участвующих в формировании (s0⚪ либо s0◎)
• ∏sjj - произведение всевозможных состояний на пути от ndi до nd0, участвующих в формировании (s0⚪ либо s0◎)

А поскольку si◎ есть прообраз si⚪, то и s0◎ есть прообраз s0⚪, что и требовалось доказать. █

Назад Вперёд