2.VII. Критерий локального изменения данных
. К оглавлению . Показать весь текст .
Теперь мы сформулируем и докажем теоремы, которые нам потребуются для доказательства «полиномиальной представимости» машины компьютерных алгоритмов в теории строк. Теория строк излагается в данной (1-й) статье, машина компьютерных алгоритмов строится в следующей (2-й) статье. Доказательство «полиномиальной представимости» будет дано в 3-й статье, а некоторые нюансы (оговоренные в 3-й статье) будут уточнены в 4-й статье.
(т.9.1) len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ⇒ str(a ⋅ b ⋅ u, len(a) ′, len(b)) = b
Доказательство при дедуктивном предположении len(a) ≠ ⊖ ∧ len(b) ≠ ⊖.
Ветка 1. Дедуктивное предположение-2: len(b) ≠ 0
Тогда из-за (т.4.2) (i ≠ 0 ∧ j ≠ 0) ⇒ str(a, i, j) = end(beg(a, i+j-1), i) получим:
1.1. str(a ⋅ b ⋅ u, len(a) ′, len(b)) = end(beg(a ⋅ b ⋅ u, len(a) + len(b)), len(a) ′)
Так как len(a ⋅ b) = len(a) + len(b) из-за (т.7.1), и в силу (т.8.6) len(a) ≠ ⊖ ⇒ a = beg(a ⋅ u, len(a)) получаем:
beg((a ⋅ b) ⋅ u, len(a) + len(b)) = (a ⋅ b)
Поэтому из п.1.1 и предыдущего равенства получим:
1.2. str(a ⋅ b ⋅ u, len(a) ′, len(b)) = end((a ⋅ b), len(a) ′)
Но end((a ⋅ b), len(a) ′) = b, из-за (т.8.7) len(a) ≠ ⊖ ⇒ u = end(a ⋅ u, len(a) ′ ), поэтому
1.3. str(a ⋅ b ⋅ u, len(a) ′, len(b)) = b
Ветка 1 доказана.
Ветка 2. Дедуктивное предположение-2: len(b) = 0
Тогда в силу определения str() и из-за (2.1) beg(a, 0) = ⊖ получим:
2.1. str(a ⋅ b ⋅ u, len(a) ′, len(b)) = str(a ⋅ b ⋅ u, len(a) ′, 0) = ⊖
С другой стороны, из-за (т.8.8) a = ⊖ ⇔ len(a) = 0 получим:
2.2. b = ⊖
Из пунктов 2.1 и 2.2 получаем:
str(a ⋅ b ⋅ u, len(a) ′, len(b)) = b
Ветка 2 для случая len(b) = 0 тоже доказана. Вместе с веткой 1 для случая len(b) ≠ 0, все варианты рассмотрены.
Теорема (т.9.1) доказана.
(т.9.2) len(a) ≠ ⊖ ⇒ end(a ⋅ b ⋅ u, len(a) ′) = b ⋅ u
Доказательство при дедуктивном предположении len(a) ≠ ⊖.
Из (т.8.7) len(a) ≠ ⊖ ⇒ u = end(a ⋅ u, len(a) ′ ) получим, используя ассоциативность конкатенации:
end(a ⋅ (b ⋅ u), len(a) ′) = b ⋅ u
Теорема (т.9.2) доказана.
(т.9.3) IsIns(len(a), i, len(b)) = 1 ⇒ len(Ins(a, i, b)) = len(a)
Доказательство при дедуктивном предположении IsIns(len(a), i, len(b)) = 1.
Из определения (9.7) и дедуктивного предположения получаем:
i ≠ 0 ∧ len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ∧ (len(b)=0 ∨ len(a) ≥ i + len(b) - 1)
Теперь просто вычислим, чему равна функция Ins(a, i, b) при истинности предыдущего утверждения:
Ins(a, i, b) = beg(a, max(i, 1) - 1) ⋅ b ⋅ end(a, if_0(min(len(len(b)), i), 0, len(b) + i)), по определению (9.6)
В силу дедуктивного предположения (max(i, 1) - 1) = i-1 и в силу ещё и того, что len(b) ≠ ⊖ (а, значит, len(len(b)) ≠ 0 из-за (с.8.8)) верно min(len(len(b)), i) > 0. Из последнего неравенства и определения if_0 получаем if_0(min(len(len(b)), i), 0, len(b) + i) = len(b) + i. Поэтому:
Ins(a, i, b) = beg(a, i - 1) ⋅ b ⋅ end(a, len(b) + i)
Если len(b) = 0, то b = ⊖ из-за (т.8.8) и тогда его можно исключить из конкатенации в силу её ассоциативности и (т.8.3) a = a ⋅ ⊖ = ⊖ ⋅ a. Поэтому тогда:
Ins(a, i, b) = beg(a, i - 1) ⋅ ⊖ ⋅ end(a, 0 + i) = beg(a, i - 1) ⋅ end(a, i)
Но по (1) имеем:
a = beg(a, i - 1) ⋅ end(a, i)
То есть, при len(b) = 0 верно:
Ins(a, i, b) = a
len(Ins(a, i, b) )) = len(a)
Теперь рассмотрим len(b) ≠ 0, тогда из дедуктивного предположения верно:
len(a) ≥ i + len(b) - 1
Чтобы посчитать len(Ins(a, i, b)), будем считать длины каждого члена конкатенации в равенстве:
Ins(a, i, b) = beg(a, i - 1) ⋅ b ⋅ end(a, len(b) + i)
А что их сумма будет равна длине их конкатенации обеспечено теоремой (т.7.1) которая (напоминание):
len(a_1) ≠ ⊖ ∧ … ∧ len(a_n) ≠ ⊖ ⇒ len(a_1 ⋅ … ⋅ a_n) = len(a_1) + … + len(a_n)
Поэтому:
len(Ins(a, i, b)) = len(beg(a, i - 1)) + len(b) + len(end(a, len(b) + i))
Из-за теоремы (т.6.7) которая (напоминание):
len(a) ≠ ⊖ ∧ i ≤ len(a) ⇒ len(beg(a, i)) = i ∧ (len(end(a, i)) = len(a) - i +1 ∨ i = 0)
Получаем (так как (i-1) ≤ len(a)):
len(beg(a, i - 1)) = i - 1
Слагаемое len(b) не требует вычисления, осталось найти len(end(a, len(b) + i)
Случай 1.
Для вычисления данного слагаемого нам может пригодится либо упомянутая теорем (6.7) в части:
len(end(a, i)) = len(a) - i +1, но только если i ≤ len(a) в теореме и len(b) + i ≤ len(a) в нашем конкретном случае. Тогда:
len(end(a, len(b) + i) = len(a) - (len(b) + i) +1 = len(a) - len(b) - i +1
len(Ins(a, i, b)) = (i - 1) + len(b) + (len(a) - len(b) - i +1) = len(a)
Для Случая 1 теорема доказана.
Случай 2.
Либо для вычисления len(end(a, len(b) + i) нам пригодится теорема (6.9) которая (напоминание):
len(a) ≠ ⊖ ∧ len(a) < i ⇒ len(beg(a, i)) = len(a) ∧ (len(end(a, i)) = 0)
Нас интересует следующая часть теоремы (6.9):
len(end(a, i)) = 0, но только если len(a) < i в теореме и len(a) < len(b) + i в нашем конкретном случае. Тогда вместе с условием len(a) ≥ i + len(b) - 1 из дедуктивного предположения имеем:
len(a) ≥ i + len(b) - 1 ∧ len(a) < len(b) + i
Перепишем для большей наглядности так:
len(b) + i - 1 ≤ len(a) < len(b) + i
В арифметике из этого выводится:
len(a) = len(b) + i - 1
len(b) = len(a) - i + 1
Теперь можем посчитать всю сумму длин:
len(Ins(a, i, b)) = (i - 1) + len(b) + 0 = i - 1 + len(a) - i + 1 = len(a)
Для Случая 2 теорема тоже доказана.
Теорема доказана.
(т.9.4) Критерий локальной вставки:
(len(a) ≠ ⊖ ∧ len(b) ≠ ⊖) ⇒
( IsIns(len(a), i, len(b)) = 1 ⇔ ∀ u Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u )
Для доказательства этой эквивалентности нужно доказать, что в условиях 1-го дедуктивного предположения:
len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ истинны 2 импликации:
IsIns(len(a), i, len(b)) = 1 ⇒ ∀ u Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u) - первая импликация;
∀ u Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u) ⇒ IsIns(len(a), i, len(b)) = 1 - вторая импликация.
Для доказательства 1-й импликации делаем 2-е дедуктивное предположение:
IsIns(len(a), i, len(b)) = 1
Из определения (9.7) и 2-го дедуктивного предположения получаем:
i ≠ 0 ∧ len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ∧ (len(b)=0 ∨ len(a) ≥ i + len(b) - 1)
Теперь просто вычислим, чему равна функция Ins(a ⋅ u, i, b) из заключения 1-й импликации при истинности предыдущего утверждения:
Ins(a ⋅ u, i, b) = beg(a ⋅ u, max(i, 1) - 1) ⋅ b ⋅ end(a ⋅ u, if_0(min(len(len(b)), i), 0, len(b) + i)), по определению (9.6)
В силу 2-го дедуктивного предположения max(i, 1) - 1 = i-1 и в силу ещё и того, что len(b) ≠ ⊖ (из 1-го дедуктивного предположения) верно min(len(len(b)), i) > 0 (так как len(b) ≠ ⊖ ⇔ len(len(b)) ≠ 0 из-за (с.8.8)) Из последнего неравенства и определения if_0 получаем if_0(min(len(len(b)), i), 0, len(b) + i) = len(b) + i. Поэтому:
Ins(a ⋅ u, i, b) = beg(a ⋅ u, i - 1) ⋅ b ⋅ end(a ⋅ u, len(b) + i), но:
beg(a ⋅ u, i - 1) = str(a ⋅ u, 1, i - 1), из-за (т.4.6),
Поэтому:
Ins(a ⋅ u, i, b) = str(a ⋅ u, 1, i - 1) ⋅ b ⋅ end(a ⋅ u, len(b) + i)
Ветка 1 для 1-й импликации. Случай len(b)=0.
Если len(b)=0, то b = ⊖ из-за (т.8.8) и тогда его можно исключить из конкатенации в силу её ассоциативности и (т.8.3) a = a ⋅ ⊖ = ⊖ ⋅ a. Поэтому тогда:
Ins(a ⋅ u, i, b) = str(a ⋅ u, 1, i - 1) ⋅ end(a ⋅ u, 0 + i)
Так str(a ⋅ u, 1, i - 1) = beg(a ⋅ u, i - 1) из-за (т.4.6) str(a, 1, j) = beg(a, j), то
Ins(a ⋅ u, i, b) = beg(a ⋅ u, i - 1) ⋅ end(a ⋅ u, i)
В силу (1) поэтому при len(b)=0 получаем:
Ins(a ⋅ u, i, b) = a ⋅ u
Так как
Ins(a, i, b) = Ins(a ⋅ ⊖, i, b) = a ⋅ ⊖ = a
То
Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u
Для ветки 1 импликация 1 доказана.
Ветка 2 для 1-й импликации. Случай len(b) > 0. Из этого и из 2-го дедуктивного предположения получается len(a) ≥ i + len(b) - 1.
У нас доказано при 1-м и 2-м предположениях дедукции
Ins(a ⋅ u, i, b) = str(a ⋅ u, 1, i - 1) ⋅ b ⋅ end(a ⋅ u, len(b) + i)
Но i - 1 ≤ len(a), так как выше мы видели, что len(b) + i - 1 ≤ len(a). Поэтому:
str(a ⋅ u, 1, i - 1) = str(a, 1, i - 1), что выводится из (т.8.6) len(a) ≠ ⊖ ⇒ a = beg(a ⋅ u, len(a)), после того, как разбить a в соответствии с (1) a = beg(a, i - 1) ⋅ end(a, i) и воспользоваться теоремой (т.6.7) чтобы доказать len(beg(a, i - 1)) = i - 1, подобно тому, как мы делали чуть выше.
Таким образом:
Ins(a ⋅ u, i, b) = str(a, 1, i - 1) ⋅ b ⋅ end(a ⋅ u, len(b) + i)
У нас остался только один член конкатенации, зависящий от u. Поэтому теперь надо доказать, что:
end(a ⋅ u, len(b) + i) = end(a, len(b) + i) ⋅ u
Запишем на основании аксиомы (1) переменную a в виде:
a = beg(a, len(b) + i - 1) ⋅ end(a, len(b) + i)
Тогда
end(a ⋅ u, len(b) + i) = end(beg(a, len(b) + i - 1) ⋅ end(a, len(b) + i) ⋅ u, len(b) + i)
В силу 2-го дедуктивного и предположения Ветки 2 верно len(a) ≥ i + len(b) - 1, поэтому
len(b) + i - 1 ≤ len(a)
Поэтому в силу (т.6.7) которая (напоминание):
len(a) ≠ ⊖ ∧ i ≤ len(a) ⇒ len(beg(a, i)) = i ∧ (len(end(a, i)) = len(a) - i +1 ∨ i = 0)
Имеем:
len(beg(a, len(b) + i - 1)) = len(b) + i - 1
А поэтому из теоремы (т.9.2) которая (напоминание):
len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ⇒ end(a ⋅ b ⋅ u, len(a) ′) = b ⋅ u
Получим
end(beg(a, len(b) + i - 1) ⋅ end(a, len(b) + i) ⋅ u, len(b) + i) = end(a, len(b) + i) ⋅ u
Таким образом, мы получили:
end(a ⋅ u, len(b) + i) = end(a, len(b) + i) ⋅ u
И теперь мы можем переписать предложение
Ins(a ⋅ u, i, b) = str(a, 1, i - 1) ⋅ b ⋅ end(a ⋅ u, len(b) + i)
Таким образом:
Ins(a ⋅ u, i, b) = str(a, 1, i - 1) ⋅ b ⋅ end(a, len(b) + i) ⋅ u
Если рассмотреть случай u = ⊖, то получим:
Ins(a, i, b) = Ins(a ⋅ ⊖, i, b) = str(a, 1, i - 1) ⋅ b ⋅ end(a, len(b) + i)
Из последних 2 формул получаем:
Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u
Ветка 2 для импликации 1 доказана.
Чтобы перейти к квантору общности, надо для результата этих 2х веток (сделав из каждой импликацию по теореме дедукции, соединив обе эти импликации в одну и отбросив дизъюнкцию частных посылок по MP) воспользоваться правилом вывода:
(α) Если верно U ⇒ B(a), то верно U ⇒ ∀ x B(x)
После чего импликация 1 доказана.
Теперь надо доказать в рамках len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ 1-го дедуктивного предположения 2-ю импликацию:
∀ u Ins(a ⋅ u, i, b) = Ins(a, i, b) ⋅ u ⇒ IsIns(len(a), i, len(b)) = 1
Перепишем её в эквивалентном виде при помощи контрапозиции, превращая квантор всеобщности в квантор существования при помощи теоремы VI.7 из раздела 4. Приложение:
IsIns(len(a), i, len(b)) ≠ 1 ⇒ ∃ u Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u)
Очевидно, что
IsIns(len(a), i, len(b)) ≠ 1 ⇔ IsIns(len(a), i, len(b)) = 0
Поэтому перепишем 2ю импликацию так:
IsIns(len(a), i, len(b)) = 0 ⇒ ∃ u Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u)
Для доказательства 2-й импликации делаем 2-е дедуктивное предположение:
IsIns(len(a), i, len(b)) = 0
Из определения (9.7) и 2-го дедуктивного предположения получаем «рабочий вариант» 2-го дедуктивного предположения:
i = 0 ∨ len(a) = ⊖ ∨ len(b) = ⊖ ∨ (len(b) ≠ 0 ∧ len(a) < i + len(b) - 1)
Теперь нам нужно доказать, что из каждого члена дизъюнкции приведённого рабочего варианта 2-го дизъюнктивного предположения следует нужное нам заключение
∃ u Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u)
А после этого мы сможем объединить все импликации с разными посылками и одинаковым заключением в импликацию, где посылка будет дизъюнкцией при помощи
III.3 (A ⇒ C) ⇒ ((B ⇒ C) ⇒ (A ∨ B ⇒ C)), из раздела 4. Приложение.
Поэтому доказываем последовательно для каждой такой посылки нужное нам заключение
Ветка 1. i = 0
Положим
u = Chr(0), тогда из определения (9.6)
Ins(a ⋅ u, i, b) = beg(a ⋅ u, max(i, 1) - 1) ⋅ b ⋅ end(a ⋅ u, if_0(min(len(len(b)), i), 0, len(b) + i))
Подстановкой соответствующего i=0 получим для двух членов конкатенации:
beg(a ⋅ u, max(i, 1) - 1) = beg(a ⋅ u, max(0, 1) - 1) = beg(a ⋅ u, 0) = ⊖
end(a ⋅ u, if_0(min(len(len(b)), i), 0, len(b) + i)) = end(a ⋅ u, if_0(0, 0, len(b) + i)) = ⊖
Поэтому:
Ins(a ⋅ u, i, b) = ⊖ ⋅ b ⋅ ⊖ = b
Что касается Ins(a, i, b) ⋅ u, то по аналогичному выводу получим (подставляя u = Chr(0)):
Ins(a, i, b) ⋅ u = b ⋅ u = b ⋅ Chr(0)
Очевидно, что длины строк, получающиеся из 2-х последних формул не равны:
len(Ins(a ⋅ u, i, b)) ≠ len(Ins(a, i, b) ⋅ u)
А не равны они из-за теоремы (т.7.1) которая (напоминание):
len(a_1) ≠ ⊖ ∧ … ∧ len(a_n) ≠ ⊖ ⇒ len(a_1 ⋅ … ⋅ a_n) = len(a_1) + … + len(a_n)
Поэтому
len(b) < len(b ⋅ Chr(0)) = len(b) + len(Chr(0)) = len(b) + 1
Кстати, про Chr(0) мы можем заведомо утверждать, что Chr(0) ≠ ⊖, а поэтому и длина его равна 1 из-за теоремы (т.7.2) которая (напоминание):
i ≤ l_ChrLim ⇒ len(Chr(i)) = 1:
Ведь для случая i = 0 заведомо выполнено i ≤ l_ChrLim, каким бы натуральным числом l_ChrLim ни был.
А в силу того, что длины строк не равны - не равны и сами строки из-за теоремы (т.8.5) которая (напоминание):
len(a)≠⊖ ⇒ [ a = b ⇔ ∀ i ((len(a) = len(b) ∧ 0 < i ∧ i ≤ len(a)) ⇒ str(a, i, 1) = str(b, i, 1)) ]
Поэтому для u = Chr(0) верно:
Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u
То есть, верно - после подстановки - следующее неравенство:
Ins(a ⋅ b ⋅ Chr(0), i, b) ≠ Ins(a, i, b) ⋅ b ⋅ Chr(0)
В силу аксиомы логики предикатов из раздела 4. Приложение:
(b) A(a) ⇒ ∃ x A(x)
Верно:
Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u ⇒ ∃ u Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u)
И мы можем подставить на место свободных переменных конкретное значение u = Chr(0):
Ins(a ⋅ Chr(0), i, b) ≠ Ins(a, i, b) ⋅ Chr(0) ⇒ ∃ u Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u)
Посылка данной импликации доказана чуть выше, поэтому её можно отбросить по правилу вывода MP. И мы получаем:
∃ u Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u)
Что и требовалось доказать для Ветки 1.
Ветка 2. len(a) = ⊖ ∨ len(b) = ⊖
В этой ветке 2-е дедуктивное предположение является точным логическим отрицанием 1-го с его len(a) ≠ ⊖ ∧ len(b) ≠ ⊖. А из противоречия доказано всё. Поэтому для Ветки 2 заключение импликации 2 тоже доказано.
Ветка 3. (len(b) ≠ 0 ∧ len(a) < i + len(b) - 1)
А точнее, мы рассмотрим Ветку 3 в таком «рабочем виде»:
i ≠ 0 ∧ len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ∧ (len(b) ≠ 0 ∧ len(a) < i + len(b) - 1)
Поясню такую «метаморфозу».
У нас 2-е дедуктивное предположение:
i = 0 ∨ len(a) = ⊖ ∨ len(b) = ⊖ ∨ (len(b) ≠ 0 ∧ len(a) < i + len(b) - 1)
Если записать его в виде:
A ∨ B
Где член дизъюнкции A - уже рассмотрен в «Ветка 1» и «Ветка 2», а сейчас мы рассматриваем в качестве посылки член дизъюнкции B. И «вдруг» подменяем его на:
(¬ A ∧ B)
Это возможно в том случае, если 2-е дедуктивное предположение в виде A ∨ B эквивалентно следующему:
A ∨ (¬ A ∧ B)
А оно действительно эквивалентно в силу теоремы VI.10 (A ∨ B) ⇔ (A ∨ (¬ A ∧ B)) из раздела 4. Приложение.
Поэтому наша «подмена» дедуктивного предположения-2 Ветки 3:
len(b) ≠ 0 ∧ len(a) < i + len(b) - 1
на «Рабочую посылку 3»:
i ≠ 0 ∧ len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ∧ (len(b) ≠ 0 ∧ len(a) < i + len(b) - 1)
является корректной.
Из рабочей посылки 3 нам нужно вывести заключение 2-й импликации:
∃ u Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u)
Для этого положим:
u = ss(i + len(b) - 1 - len(a))
В качестве аргумента в ss() тут - натуральное число, не равное нулю, в силу
len(a) < i + len(b) - 1, из рабочей посылки 3.
Теперь просто вычислим размер Ins(a ⋅ u, i, b) для которого верно:
Ins(a ⋅ u, i, b) = Ins(a ⋅ ss(i + len(b) - 1 - len(a)), i, b)
Так как:
len(a ⋅ ss(i + len(b) - 1 - len(a))) = len(a) + len(ss(i + len(b) - 1 - len(a)))
То учтём, что по определению ss(i) верно: len(ss(i)) = i, поэтому:
len(a ⋅ ss(i + len(b) - 1 - len(a))) = len(a) + i + len(b) - 1 - len(a) = i + len(b) - 1
А это значит, что наша реализация
a ⋅ u = a ⋅ ss(i + len(b) - 1 - len(a))
удовлетворяет условию:
len(a ⋅ u) ≤ i + len(b) - 1
Кроме того, верно:
len(a ⋅ u) ≠ ⊖
И выполнено:
IsIns(a ⋅ u, i, b) = 1
А поэтому воспользуемся теоремой (т.9.3), которая (напоминание):
IsIns(len(a), i, len(b)) = 1 ⇒ len(Ins(a, i, b) )) = len(a)
Из неё мы непосредственно получаем:
len(Ins(a ⋅ u, i, b)) = len(a ⋅ u) = i + len(b) - 1, при u = ss(i + len(b) - 1 - len(a)).
А теперь посчитаем len(Ins(a, i, b) ⋅ u):
len(Ins(a, i, b) ⋅ u) = len(Ins(a, i, b)) + len(u)
Из определения (9.6) для Ins(a, i, b):
Ins(a, i, b) = beg(a, max(i, 1) - 1) ⋅ b ⋅ end(a, if_0(min(len(len(b)), i), 0, len(b) + i))
Для beg(a, max(i, 1) - 1) верно:
len(beg(a, max(i, 1) - 1)) = len(beg(a, i - 1)) = min(len(a), i - 1)
Действительно, max(i, 1) = i, так как в Рабочей посылке 3 выполнено i ≠ 0, а последняя строка в цепочке равенств - из следствия (с.6.9), которая (напоминание):
len(a) ≠ ⊖ ⇒ len(beg(a, i)) = min(i, len(a)) ∧ (len(end(a, i)) = max(len(a), i +1) - i +1 ∨ i = 0)
Для end(a, if_0(min(len(len(b)), i), 0, len(b) + i)) верно:
len(end(a, if_0(min(len(len(b)), i), 0, len(b) + i))) = len(end(a, len(b) + i))
Действительно, min(len(len(b)), i) ≠ 0, так как в Рабочей посылке 3 выполнено i ≠ 0, len(b) ≠ 0, len(b) ≠ ⊖. Из len(b) ≠ ⊖ следует len(len(b)) ≠ 0 в силу (с.8.8) len(a) = ⊖ ⇔ len(len(a)) = 0. А поэтому if_0(min(len(len(b)), i), 0, len(b) + i) равно len(b) + i.
Таким образом:
len(Ins(a, i, b)) = min(len(a), i - 1) + len(b) + len(end(a, len(b) + i))
Так как в Рабочей посылке 3 верно len(a) < i + len(b) - 1, то тем более len(a) < i + len(b).
Поэтому в силу теоремы (т.6.9), которая (напоминание):
len(a) ≠ ⊖ ∧ len(a) < i ⇒ len(beg(a, i)) = len(a) ∧ (len(end(a, i)) = 0)
Получаем:
len(end(a, len(b) + i)) = 0
Значит:
len(Ins(a, i, b)) = min(len(a), i - 1) + len(b) + 0 = min(len(a), i - 1) + len(b)
Вспоминая, что мы рассматриваем u = ss(i + len(b) - 1 - len(a)) где len(u) = i + len(b) - 1 - len(a) получим:
len(Ins(a, i, b) ⋅ u) = min(len(a), i - 1) + len(b) + len(u) = min(len(a), i - 1) + len(b) + i + len(b) - 1 - len(a)
len(Ins(a, i, b) ⋅ u) = min(len(a), i - 1) + i - 1 - len(a) + 2 × len(b)
И сравним это с полученным выше:
len(Ins(a ⋅ u, i, b)) = i + len(b) - 1
Тогда:
len(Ins(a, i, b) ⋅ u) - len(Ins(a ⋅ u, i, b)) = [ min(len(a), i - 1) + i - 1 - len(a) + 2 × len(b) ] - [ i + len(b) - 1 ]
len(Ins(a ⋅ u, i, b)) - len(Ins(a, i, b) ⋅ u) = min(len(a), i - 1) + len(b) - len(a)
Так как в Рабочей посылке 3 верно len(a) < i + len(b) - 1, то результат последнего выражения больше 0, так как если min(len(a), i - 1) = i - 1, то len(a) вычитается от i + len(b) - 1, которая больше len(a). А если min(len(a), i - 1) = len(a), то результат выражения равен len(b), а len(b) ≠ 0 по Рабочей посылке 3.
Таким образом:
len(Ins(a ⋅ u, i, b)) ≠ len(Ins(a, i, b) ⋅ u)
Значит, по теореме (т.8.5), которая (напоминание)::
len(a)≠⊖ ⇒ [ a = b ⇔ ∀ i ((len(a) = len(b) ∧ 0 < i ∧ i ≤ len(a)) ⇒ str(a, i, 1) = str(b, i, 1)) ]
Получаем:
Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u, при u = ss(i + len(b) - 1 - len(a)).
От этого конкретного значения u переходим к нужному нам заключению:
∃ u Ins(a ⋅ u, i, b) ≠ Ins(a, i, b) ⋅ u)
Для перехода от предпоследнего предложения к последнему предложению используем тот же способ, который использовался при рассмотрении Ветки 1.
Все варианты посылок рассмотрены, поэтому импликация 2 тоже доказана.
Теорема доказана.