16.26. Теорема

Если даны основы для согласованной системы ВС [SVS⚪] и [SVS◎], находящихся в отношении О-проекции, то применение к ним алгоритма 16.3 порождает ряд основ, в котором:

1. соседние члены сами находятся в отношении О-проекции
2. последний член совпадает с [SVS⚪]

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

Второй пункт следует из того, что:

• деревья, на которых построены по алгоритму 9.8 каркасы рассматриваемых основ, образуют ряд, последний член которого совпадает с деревом каркаса последней основы (см. теорему 9.8)
• каркасы, построенные на таких деревьях по алгоритму 11.5, образуют ряд, последний член которого совпадает с деревом каркаса последней основы (см. теорему 11.3)
• множества базовых и частичных ВС последнего члена ряда [SVS⊡] совпадают с соответствующими множествами основы [SVS⚪], что можно доказать от обратного:
  1. предположим, что в [SVS⊡] с листом nd сопряжена базовая ВС vs⊡, отличная от ВС vs⚪, сопряженной с тем же nd в [SVS⚪];
  2. в зависимости от того, какая вершина соответствует листу nd в [SVS◎] – тот же лист или узел, – соответствующая vs◎ из [SVS◎] является либо базовой либо частичной; в зависимости от этого превращение исходной vs◎ производится либо на шаге А, либо на шаге Г, однако, в обоих случаях – именно в vs⚪, что доказывает совпадение vs⚪ и vs⊡
  3. предположим, что в [SVS⊡] с узлом nd сопряжена частичная ВС vs⊡, отличная от ВС vs⚪, сопряженной с тем же nd в [SVS⚪];

     узлу nd в [SVS◎] соответствует тот же узел, а соответствующая vs◎ из [SVS◎] является частичной, превращение которой происходит на шаге В (все прочие удалены на шаге Д), и что важно – именно в vs⚪, что доказывает совпадение vs⚪ и vs⊡

Для доказательства первого пункта следует заметить, что в зависимости от типа элементарного шага, которым связаны соседние основы:

• типом Д – в лемме 16.2Д
• типом А – в лемме 16.2А.2
• типом Б – в лемме 16.2Б.2
• типом В – в лемме 16.2В.2
• типом Г – в лемме 16.2Г

доказывается, что в паре основ [SVSi] и [SVSi+1], у которых

• каркасы SKELi и SKELi+1 связаны элементарным шагом одного из указанных типов, либо тождественны
• [SVSi] является основой для согласованной системы ВС

основа [SVSi+1] также является согласованной, то есть, связана с [SVSi] соответствующим элементарным шагом.

Иначе говоря, для заданной пары основ (согласованных) систем ВС [SVS⚪] и [SVS◎], находящихся в отношении О-проекции, построен требуемый ряд связывающих их основ, где каждая пара соседних основ [SVSi] и [SVSi+1]:

• связана одним из элементарных шагов типа А, Б, В, Г или Д
• находится в отношении О-проекции

что и требовалось доказать. █

Назад Вперёд