dmitgu

Category:

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 тоже доказана.

Теорема доказана.

Error

default userpic

Your reply will be screened

Your IP address will be recorded 

When you submit the form an invisible reCAPTCHA check will be performed.
You must follow the Privacy Policy and Google Terms of use.