17.1. Теорема

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

[SVS◎] = <T◎, COM◎, SEL◎, VS⧋◎, VS⫧◎>

и связанная с ней ЭШ типа Г её О-проекция

[SVS⚪] = <T⚪, COM⚪, SEL⚪, VS⧋⚪, VS⫧⚪>

то есть такие, что отличие между ними заключается в добавлении промежуточного узла, а значит и сопряжённой с ней некоторой системообразующей ВС:

• T⚪ и T◎ принадлежат некий узел nd⫯ и подчинённая ему вершина nd⫰, причем:
  • в T⚪ вершина nd⫰ является непосредственно подчинённой для узла nd⫯
  • в T◎ между nd⫰ и nd⫯ имеется единственный дополнительный узел nd⩘
• vs⫯⚪ из VS⚪ и vs⫯◎ из VS◎ – ВС, сопряженные с nd⫯
• vs⫰⚪ из VS⚪ и vs⫰◎ из VS◎ – ВС, сопряженные с nd⫰
• vs⩘◎ из VS◎ – ВС, сопряженная с nd⩘
• s⫰⚪ - произвольное состояние vs⫰⚪, для которого выбраны также произвольные:
  • состояние s⫯⚪ из vs⫯⚪, порождённое от s⫰⚪
  • состояние s⫰◎ из vs⫰◎, являющееся прообразом для s⫰⚪

Тогда в vs⫯◎ существует, как минимум, одно состояние s⫯◎:

• порождённое от s⫰◎
• являющееся прообразом s⫯⚪

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

Поскольку система SVS◎ является согласованной, vs⫯◎ является прообразом для vs⫯⚪, то есть в vs⫯◎ существует некое s⫯◎, порождённое от s⫰◎.

Осталось доказать, что среди подобных s⫯◎ найдётся такое, которое является также и прообразом s⫯⚪.

В зависимости от типа узлов nd⫯ и nd⩘:

1. nd⫯ и nd⩘ имеют тип ЛИБО; тогда согласно алгоритму синтеза ВС:
   1. s⫯⚪ является произведением s⫰⚪ и некоторого ключа k⫯ ∈ sel⚪ из SEL⚪, сопряженного с дугой (nd⫯ , nd⫰):

      s⫯⚪ = s⫰⚪ × k⫯

   2. s⫰◎ = s⫰⚪ × s⫰◎
   3. s⫯◎ является произведением:
      1. s⫰⚪
      2. ключа k⩘ ∈ sel⩘ из SEL◎, сопряженного с дугой (nd⫰ , nd⩘)
      3. уже рассмотренного ключа k⫯ ∈ sel◎ из SEL◎, сопряженного с дугой (nd⩘ , nd⫯)

         s⫯◎ = s⫰◎ × k⩘ × k⫯ =

         = (s⫰⚪ × s⫰◎) × sel⚪ × k⫯ =

         = (s⫰⚪ × k⫯) × s⫰◎ × sel⚪ =

         = s⫯⚪ × s⫰◎ × sel⚪

         тем самым, являясь прообразом s⫯⚪, что и требовалось доказать

2. nd⫯ имеет тип И, а nd⩘ – тип ЛИБО; тогда согласно алгоритму синтеза ВС:
   1. s⫯⚪ является произведением:
      1. некоторого ключа k⫯ ∈ com⫯ из COM⚪, сопряженного с узлом nd⫯
      2. состояния s⫰⚪
      3. некоторых состояний s⫯1⚪ .. s⫯M⫯⚪ из прочих ВС, сопряженных с остальными вершинами, непосредственно подчинёнными узлу nd⫯, и также имеющими произведение с ключом k⫯

         s⫯⚪ = k⫯ × s⫰⚪ × s⫯1⚪ × .. × s⫯M⫯⚪

   2. s⫰◎ = s⫰⚪ × s⫰◎
   3. s⫯◎ является произведением:
      1. состояния s⫰◎
      2. того же самого ключа k⫯
      3. тех же самых состояний s⫯1⚪ .. s⫯M⫯⚪
      4. некоторого ключа sel⚪ ∈ sel⚪ из SEL◎, сопряженного с дугой (nd⩘ , nd⫰), выходящей из узла nd⫯

         s⫯◎ = s⫰◎ × k⫯ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪ =

         = (s⫰⚪ × k⫯) × s⫰◎ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪ =

         = s⫯⚪ × s⫰◎ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪

         тем самым, являясь прообразом s⫯⚪, что и требовалось доказать

3. nd⫯ имеет тип ЛИБО, а nd⩘ – тип И; тогда согласно алгоритму синтеза ВС:
   1. s⫯⚪ является произведением s⫰⚪ и некоторого ключа k⫯ ∈ sel⚪ из SEL⚪, сопряженного с дугой (nd⫯ , nd⫰), выходящей из узла nd⫯:

      s⫯⚪ = s⫰⚪ × k⫯

   2. s⫰◎ = s⫰⚪ × s⫰◎
   3. s⫯◎ является произведением:
      1. состояния s⫰◎
      2. того же самого ключа k⫯
      3. тех же самых состояний s⫯1⚪ .. s⫯M⫯⚪
      4. некоторого ключа sel⚪ ∈ com⩘ из COM◎, сопряженного с узлом nd⩘
      5. некоторых состояний s⩘1⚪ .. s⩘M⩘⚪ из прочих ВС, сопряженных с остальными вершинами, непосредственно подчинёнными узлу nd⩘, и также имеющими произведение с ключами COM⩘ и k⫯

         s⫯◎ = s⫰◎ × k⫯ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪ × s⩘1⚪ × .. × s⩘M⩘⚪ =

         = (s⫰⚪ × k⫯) × s⫰◎ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪ × s⩘1⚪ × .. × s⩘M⩘⚪ =

         = s⫯⚪ × s⫰◎ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪ × s⩘1⚪ × .. × s⩘M⩘⚪

      6. s⫰⚪
      7. ключа sel⩘ из SEL◎, сопряженного с дугой (nd⫰ , nd⩘)
      8. уже рассмотренного ключа sel⫯ из SEL◎, сопряженного с дугой (nd⩘ , nd⫯)

         s⫯◎ = s⫰◎ × SEL⩘ × sel⫯ =

         = (s⫰⚪ × s⫰◎) × sel⩘ × sel⫯ =

         = (s⫰⚪ × sel⫯) × s⫰◎ × sel⩘ =

         = s⫯⚪ × s⫰◎ × sel⩘

         тем самым, являясь прообразом s⫯⚪, что и требовалось доказать

4. nd⫯ и nd⩘ имеют тип И; тогда согласно алгоритму синтеза ВС:
   1. s⫯⚪ является произведением:
      1. некоторого ключа k⫯ ∈ com⫯ из COM⚪, сопряженного с узлом nd⫯
      2. состояния s⫰⚪
      3. некоторых состояний s⫯1⚪ .. s⫯M⫯⚪ из прочих ВС, сопряженных с остальными вершинами, непосредственно подчинёнными узлу nd⫯, и также имеющими произведение с ключом k⫯

         s⫯⚪ = k⫯ × s⫰⚪ × s⫯1⚪ × .. × s⫯M⫯⚪

   2. s⫰◎ = s⫰⚪ × s⫰◎
   3. s⫯◎ является произведением:
      1. состояния s⫰◎
      2. того же самого ключа k⫯
      3. тех же самых состояний s⫯1⚪ .. s⫯M⫯⚪
      4. некоторого ключа sel⚪ ∈ com⩘ из COM◎, сопряженного с узлом nd⩘
      5. некоторых состояний s⩘1⚪ .. s⩘M⩘⚪ из прочих ВС, сопряженных с остальными вершинами, непосредственно подчинёнными узлу nd⩘, и также имеющими произведение с ключами sel⚪ и k⫯

         s⫯◎ = s⫰◎ × k⫯ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪ × s⩘1⚪ × .. × s⩘M⩘⚪ =

         = (s⫰⚪ × k⫯) × s⫰◎ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪ × s⩘1⚪ × .. × s⩘M⩘⚪ =

         = s⫯⚪ × s⫰◎ × sel⚪ × s⫯1⚪ × .. × s⫯M⫯⚪ × s⩘1⚪ × .. × s⩘M⩘⚪

         тем самым, являясь прообразом s⫯⚪, что и требовалось доказать

. █

Назад Вперёд