x 1.00
Семинар 8. Язык структурированных доказательств Isar (продолжение)
- 00:15?thesis. Представление теоремы на языке Isar (повторение)
- 03:12Ключевое слово let. Цитирование facts по имени и по значению. Разбитие доказательства на мелкие шаги. Синтаксис для локальных лемм (повторение)
- 08:27Пример
- 13:34Теорема про квадрат разности (пример)
- 21:07Утверждение о существовании двух списков таких, что любой список можно представить в виде их конкатенации, причем их длины совпадают или различаются на 1 (пример)
- 40:49Метод cases
- 46:33Структурная индукция
- 01:04:46Вычислительная индукция (пример)