Теорема 19.8
Содержание (FireFox,Safari)

19.8. Теорема

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

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

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

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

Тогда множества {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, что и требовалось доказать.

Назад Вперёд
ru/en