2.VIII. Критерий локального извлечении данных
. К оглавлению . Показать весь текст .
Критерий локального извлечения данных:
(т.9.5) len(a) ≠ ⊖ ⇒ ( IsStr(len(a), i, j) = 1 ⇔ ∀ u str(a ⋅ u, i, j) = str(a, i, j) )
Для доказательства этой эквивалентности нужно доказать, что в условиях 1-го дедуктивного предположения:
len(a) ≠ ⊖ истинны 2 импликации:
IsStr(len(a), i, j) = 1 ⇒ ∀ u str(a ⋅ u, i, j) = str(a, i, j) - первая импликация;
∀ u str(a ⋅ u, i, j) = str(a, i, j) ⇒ IsStr(len(a), i, j) = 1 - вторая импликация.
Для доказательства 1-й импликации делаем 2-е дедуктивное предположение:
IsStr(len(a), i, j) = 1
Из определения (9.8) и 2-го дедуктивного предположения получаем:
len(a) ≠ ⊖ ∧ (i = 0 ∨ j = 0 ∨ len(a) ≥ i + j - 1)
Ветка 1. i = 0
Тогда из определения str() и из-за (2.2) end(a, 0) = ⊖ и (2.4) beg(⊖, q) = ⊖ получим:
str(a ⋅ u, i, j) = str(a ⋅ u, 0, j) = beg(end(a ⋅ u, 0), j) = ⊖
Аналогично:
str(a, i, j) = ⊖
Поэтому
str(a ⋅ u, i, j) = str(a, i, j)
Первая импликация для Ветки 1 доказана из последнего равенства в виде:
IsStr(len(a), i, j) = 1 ⇒ ∀ u str(a ⋅ u, i, j) = str(a, i, j) )
А переход к квантору общности делается по аксиоме из Раздела 4. Приложение:
(α) Если верно U ⇒ B(a), то верно U ⇒ ∀ x B(x)
Ветка 2. j = 0
Тогда из определения str() и из-за (2.1) beg(a, 0) = ⊖ получим:
str(a ⋅ u, i, j) = str(a ⋅ u, i, 0) = beg(end(a ⋅ u, i), 0) = ⊖
Аналогично:
str(a, i, j) = ⊖
Поэтому
str(a ⋅ u, i, j) = str(a, i, j)
Завершение доказательства Ветки 2 с квантором общности - как для Ветки 1.
Ветка 3. (i ≠ 0 ∧ j ≠ 0 ∧ len(a) ≥ i + j - 1)
Почему рассмотренные Ветки 1 и 2 (i = 0 ∨ j = 0) превратились в своё отрицание, и добавились как член конъюнкции к оставшемуся для рассмотрения варианту - см. теорему VI.10 (A ∨ B) ⇔ (A ∨ (¬ A ∧ B)) в разделе 4. Приложение.
Теперь, чтобы вычислить, чему равна функция str(a ⋅ u, i, j), представим переменную a следующим образом в соответствии с аксиомой (1) и с учётом i ≠ 0 получим:
a = beg(a, i-1) ⋅ end(a, i)
end(a, i) = beg(end(a, i), j) ⋅ end(end(a, i), j ′)
На основании (т.4.6) str(a, 1, j) = beg(a, j) получаем:
beg(a, i - 1) = str(a, 1, i - 1)
На основании определения (4.1) для str() получаем:
beg(end(a, i), j) = str(a, i, j)
На основании (т.3.2) (i ≠ 0 ∧ j ≠ 0) ⇒ end(a, i + j - 1) = end(end(a, i), j) получаем:
end(end(a, i), j ′) = end(a, i + j)
Теперь можно переписать a следующим образом:
a = str(a, 1, i - 1) ⋅ str(a, i, j) ⋅ end(a, i + j)
На основании следствия (с.6.7) которое (напоминание):
len(a) ≠ ⊖ ∧ i ≠ 0 ∧ i + j - 1 ≤ len(a) ⇒ len(str(a, i, j)) = j
Получаем с учётом того, что len(a) ≥ i + j - 1:
len(str(a, 1, i - 1)) = i - 1
len(str(a, i, j)) = j
На основании трёх последних предложений (не считая (с.6.7)), ассоциативности конкатенации и теоремы (т.9.1) которая (напоминание):
len(a) ≠ ⊖ ∧ len(b) ≠ ⊖ ⇒ str(a ⋅ b ⋅ u, len(a) ′, len(b)) = b
Получаем:
str(a ⋅ u, i, j) = str(str(a, 1, i - 1) ⋅ str(a, i, j) ⋅ end(a, i + j) ⋅ u, i, j) = str(a, i, j)
Завершение доказательства Ветки 3 - как для Ветки 1.
Первая импликация доказана.
Теперь надо доказать вторую импликацию:
∀ u str(a ⋅ u, i, j) = str(a, i, j) ⇒ IsStr(len(a), i, j) = 1
Перепишем её в эквивалентном виде при помощи контрапозиции, превращая квантор общности в квантор существования при помощи теоремы VI.7 из раздела 4. Приложение:
IsStr(len(a), i, j) ≠ 1 ⇒ ∃ u str(a ⋅ u, i, j) ≠ str(a, i, j)
Очевидно, что
IsStr(len(a), i, j) ≠ 1 ⇔ IsStr(len(a), i, j) = 0
Поэтому перепишем 2ю импликацию так:
IsStr(len(a), i, j) = 0 ⇒ ∃ u str(a ⋅ u, i, j) ≠ str(a, i, j)
Для доказательства 2-й импликации делаем 2-е дедуктивное предположение:
IsStr(len(a), i, j) = 0
Из определения (9.8) и 2-го дедуктивного предположения получаем «рабочий вариант» 2-го дизъюнктивного предположения:
len(a) = ⊖ ∨ (i ≠ 0 ∧ j ≠ 0 ∧ len(a) < i + j - 1)
Член дизъюнкции len(a) = ⊖ в данном предложении является отрицанием 1-го дедуктивного предположения, поэтому удаляем его из дизъюнкции. И тогда первое и второе дедуктивные предположения дают общее дедуктивное предположение:
len(a) ≠ ⊖ ∧ i ≠ 0 ∧ j ≠ 0 ∧ len(a) < i + j - 1
Из общего дедуктивного предположения нам нужно вывести заключение 2-й импликации:
∃ u str(a ⋅ u, i, j) ≠ str(a, i, j)
Для этого положим:
u = ss(i + j - 1 - len(a))
Тогда, учитывая, что по определению ss(i) верно: len(ss(i)) = i, получим:
len(a ⋅ u) = len(a) + len(u) = len(a) + len(ss(i + j - 1 - len(a)))
len(a ⋅ u) = len(a) + i + j - 1 - len(a) = i + j - 1
На основании следствия (с.6.7) которое (напоминание):
len(a) ≠ ⊖ ∧ i ≠ 0 ∧ i + j - 1 ≤ len(a) ⇒ len(str(a, i, j)) = j
Получаем с учётом того, что len(a ⋅ u) ≥ i + j - 1:
len(str(a ⋅ u, i, j)) = j
С другой стороны, из-за (т.4.2) (i ≠ 0 ∧ j ≠ 0) ⇒ str(a, i, j) = end(beg(a, i + j - 1), i) получим:
str(a, i, j) = end(beg(a, i + j - 1), i)
На основании (т.8.2) len(a) ≠ ⊖ ⇒ a = str(a, 1, len(a)) и (т.4.6) str(a, 1, j) = beg(a, j) получаем:
str(a, i, j) = end(beg(beg(a, len(a)), i + j - 1), i)
На основании (т.3.1) beg(a, min(i, j)) = beg(beg(a, i), j) и len(a) < i + j - 1 из общего дедуктивного предположения получаем:
str(a, i, j) = end(beg(a, len(a)), i)
Используя снова (т.4.6) str(a, 1, j) = beg(a, j) и (т.8.2) len(a) ≠ ⊖ ⇒ a = str(a, 1, len(a)) получаем:
str(a, i, j) = end(a, i)
Тогда на основании 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)
Получаем:
len(str(a, i, j)) = len(end(a, i)) = max(len(a), i -1) - i +1
и надо его сравнить с полученным ранее
len(str(a ⋅ u, i, j)) = j
При том, что len(a) < i + j - 1 из общего дедуктивного предположения.
Перепишем последнее неравенство так:
len(a) - (i-1) < j
Левая часть len(a) - (i-1) может быть и отрицательной, но тогда
max(len(a), i -1) - i +1 = 0 < j
А если len(a) - (i-1) не отрицательна, то
max(len(a), i -1) - i +1 = len(a) - (i-1) < j
То есть, в любом случае:
max(len(a), i -1) - i +1 < j
len(str(a, i, j)) < len(str(a ⋅ u, i, j))
len(str(a, i, j)) ≠ len(str(a ⋅ u, i, j))
Тогда на основании теоремы (т.8.5), которая (напоминание):
len(a)≠⊖ ⇒ [ a = b ⇔ ∀ i ((len(a) = len(b) ∧ 0 < i ∧ i ≤ len(a)) ⇒ str(a, i, 1) = str(b, i, 1)) ]
Получаем:
str(a, i, j) ≠ str(a ⋅ u, i, j)
Поэтому для u = ss(i + j - 1 - len(a)) верно:
str(a, i, j) ≠ str(a ⋅ u, i, j)
То есть, верно - после подстановки - следующее неравенство:
str(a, i, j) ≠ str(a ⋅ u = ss(i + j - 1 - len(a)), i, j)
В силу аксиомы логики предикатов из раздела 4. Приложение:
(b) A(a) ⇒ ∃ x A(x)
Верно:
str(a, i, j) ≠ str(a ⋅ u, i, j) ⇒ ∃ u str(a, i, j) ≠ str(a ⋅ u, i, j)
И мы можем подставить на место свободных переменных конкретное значение u = ss(i + j - 1 - len(a)):
str(a, i, j) ≠ str(a ⋅ ss(i + j - 1 - len(a)), i, j) ⇒ ∃ u str(a, i, j) ≠ str(a ⋅ u, i, j)
Посылка данной импликации доказана чуть выше, поэтому её можно отбросить по правилу вывода MP. И мы получаем:
∃ u str(a, i, j) ≠ str(a ⋅ u, i, j)
Что и требовалось доказать из общего дедуктивного предположения, поэтому импликация 2 тоже доказана.
Теорема доказана.