17.2. Теорема

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

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

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

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

то есть такие, что отличие между ними заключается в добавлении промежуточного узла nd⩘, а значит и сопряжённой с ней некоторой системообразующей ВС 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⫰⚪, например, в зависимости от типа узла nd⫯:

    тип И	s⫯⚪ = s⫰⚪ × s1⫰ × … × sn⫰ для некоторых сомножителей s1⫰ ... sn⫰
    тип ЛИБО	s⫯⚪ = s⫰⚪ × k⫯ для некоторого ключа k⫯
    тип И-ЛИБО	s⫯⚪ = s⫰⚪ × k⫯ × s1⫰ × … × sn⫰ для некоторого ключа k⫯ и некоторых сомножителей s1⫰ … sn⫰

  • состояние s⫰◎ из vs⫰◎, являющееся прообразом для s1⫰⚪, то есть представимо в виде произведения:
    s⫰◎ =
    s⫰⚪
    ×
    s0

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

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

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

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

Назад Вперёд