Редактирование: МФСП, 08 лекция (от 22 октября)
Материал из eSyr's wiki.
Внимание: Вы не представились системе. Ваш IP-адрес будет записан в историю изменений этой страницы.
Правка может быть отменена. Пожалуйста, просмотрите сравнение версий, чтобы убедиться, что это именно те изменения, которые вас интересуют, и нажмите «Записать страницу», чтобы изменения вступили в силу.
| Текущая версия | Ваш текст | ||
| Строка 41: | Строка 41: | ||
Выбираем точку, выбираем индуктивное утверждение q_i, затем выбираем фундированное множество, совпадающее с множеством натуральных чисел, определяющих точки и записываем условие корректности этой точки сечения, оно выглядит достаточно очевидно, поскольку в индуктивном утверждении есть y_2 ≥ 0, поэтому принадлежность множества значений функции очевидно. После этого .... прохождение по циклу из точки сечения i в точку сечения i выглядит очевидно: | Выбираем точку, выбираем индуктивное утверждение q_i, затем выбираем фундированное множество, совпадающее с множеством натуральных чисел, определяющих точки и записываем условие корректности этой точки сечения, оно выглядит достаточно очевидно, поскольку в индуктивном утверждении есть y_2 ≥ 0, поэтому принадлежность множества значений функции очевидно. После этого .... прохождение по циклу из точки сечения i в точку сечения i выглядит очевидно: | ||
| - | i-i: ∀ -x- ∀ -y- (x_1 = y_1 x_2 + y_2) ∧ (y_2 ≥ 0) &and | + | i-i: ∀ -x- ∀ -y- (x_1 = y_1 x_2 + y_2) ∧ (y_2 ≥ 0) &and (x_2 > 0) ∧ (y_2 ≥ x_2) ⇒ y_2 > y_2 - x_2 |
Несложно видеть, что данное условие завершимости является корректным, поскольку (x_2 > 0) ∧ (y_2 ≥ x_2), и из этого следует y_2 > y_2 - x_2. | Несложно видеть, что данное условие завершимости является корректным, поскольку (x_2 > 0) ∧ (y_2 ≥ x_2), и из этого следует y_2 > y_2 - x_2. | ||
