16.16. Теорема

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

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

и согласованная с ней система

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

а также составляющие основу

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

такие, что выполнены следующие условия:

• корректный каркас

  SKEL◎ = <T◎, SH◎, COM◎, SEL◎>

  связан с корректным SKEL⚪ элементарным шагом типа В (в T⚪ между вершинами nd⫯ и nd⫰ отсутствует nd*)

• если некая вершина является листом в T⚪, а значит и в T◎, то совпадают сопряжённые с ней базовые ВС

  vs⧋⚪ = vs⧋◎

• каждая частичная ВС из VS⫧⚪, сопряженная с произвольной вершиной nd дерева T⚪, входит в VS⫧◎ (будучи сопряжена с той же вершиной nd дерева T◎)

В этом случае также существует согласованная с [SVS⚪] система ВС

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

то есть, (основы) систем SVS⚪ и SVS◎ связаны элементарным шагом типа В, а значит, первая является О-проекцией второй.

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

Согласованность SVS⚪ означает проверку условий B,C1,C2 определения 13.2, поскольку корректность каркаса SKEL⚪ (условие А) предзадано.

Вначале разберёмся с различием между ВС двух систем, которое определяется алгоритмом 14.1.

Очевидно, совпадают ВС обеих систем, сопряжённые с вершинами, у которых среди подчинённых нет nd* (условно, основой T∆, определяемой вершиной nd*).

Иными словами, различия касаются только тех вершин, которые расположены над nd* (условно, дополнением, определяемым вершиной nd*), а именно – каждое их состояние в [VS°] не домножается на некий ключ вершины nd*, отчего они не перестают существовать.

Различие между ключами было выяснено в теореме 11.2В:

• для дерева T∇ (условно, дополнением, определяемым вершиной nd*) ключи совпадают
• для дерева T∆ (условно, основой, определяемой вершиной nd*) ключи не содержат сомножителя, связанного с узлом nd*

Теперь можно доказать существование произведение состояний каждой ВС в системе SVS⚪ на множество унаследованных ключей соответствующей вершины.

Получается, что и для дерева T∆ и для дерева T∇, осуществляется произведение состояний той же самой ВС на ключи, не имеющие сомножителя в виде ключа узла nd*; такое произведение очевидно существует при условии существования исходного «полного» произведения.

Значит, SVS⚪ согласованна. █

Назад Вперёд