dmitgu

Category:

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

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

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.