19.5. Теорема

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

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

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

такие, что такие, что

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

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

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

  c⋓ = <nd0, nd1, .. , ndN, {s01⚪}, .. , {s0N⚪}, {s1⚪}, .. , {sN⚪}, k1, .. , kN>

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

  {s1◎} ⊆ [VS1◎], .. , {sN◎} ⊆ [VSN◎]

  являются всевозможными прообразами указанных {s1⚪} .. {sN⚪}

  {s1⚪} ⊴ {s1◎}, .. , {sN⚪} ⊴ {sN◎}

Тогда множества {s01◎}, .. , {s0N◎} состояний VS0◎, порождённых от указанных {s1◎} .. {sN◎}, не пересекаются, поскольку получены умножением на разные ключи одного селектора, и к тому же, эти множества являются прообразами соответствующих множеств состояний {s01⚪}, .. , {s0N⚪}

{s0i⚪} ⊴ {s0i◎}, (i=1..N)

то есть для каждого

s0i⚪ ∈ {s0i⚪} ⊆ [VSi◎], (i=1..N)

существует

s0i◎ ∈ {s0i◎}, (i=1..N)

являющееся его прообразом

s0i⚪ ⊴ s0i◎, (i=1..N)

Тем самым, существует ЛИБО-ячейка

c⋓◎ = <nd0, nd1 .. ndN, {s01◎}, .. , {s0N◎}, {s1◎} .. {sN◎}, k1 .. kN>

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

c⋓⚪ ⊴ c⋓◎

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

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

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

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

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

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

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

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

█

Назад Вперёд