М
С того, что у тебя m может быть не n+n1
Это тогда что?
Size: a a a
2020 November 08
М
Ну да
Если ну да
М
Ну да, если m >= n, то sub n m = 0
И к чему это
S
И к чему это
Это лемма, которую нужно доказать
М
Щаз отправим площадь криволинейной трапеции счтать по линейке с нулевым шагом
М
Пока не досчитаешь не приходи
S
Щаз отправим площадь криволинейной трапеции счтать по линейке с нулевым шагом
Ну давай хоть с шагом планковской длинны
BT
Решил с Isabelle/HOL поиграться.
theory SubТри утверждения я доказал, ещё 2 не могу, что для любого m >= n результат 0, и для любого m < n результат n - m
imports Main
begin
fun sub :: "nat ⇒ nat ⇒ nat"
where
"sub 0 m = 0" |
"sub n 0 = n" |
"sub (Suc n) (Suc m) = sub n m"
lemma[simp]: "sub 0 m ≡ 0"
by simp
lemma[simp]: "sub n 0 = n"
apply (induction n)
apply auto
done
lemma[simp]: "sub m m = 0"
apply (induction m)
apply auto
done
lemma[simp]: "sub n (Suc 0) = n - Suc 0"
apply (induction n)
apply auto
done
end
Объясни что ты хочешь доказать на русском
М
*шутейка для математиков*
S
Объясни что ты хочешь доказать на русском
Я хочу доказать, что если я передам функции два аргумента, где второй, больше, либо равен первому, то получу 0 в результате
И, что если я передам ей два агрумента, где второй меньше, чем первый, то получу их разность
И, что если я передам ей два агрумента, где второй меньше, чем первый, то получу их разность
BT
Я хочу доказать, что если я передам функции два аргумента, где второй, больше, либо равен первому, то получу 0 в результате
И, что если я передам ей два агрумента, где второй меньше, чем первый, то получу их разность
И, что если я передам ей два агрумента, где второй меньше, чем первый, то получу их разность
Результат чего? Вычитания, умножения?
S
Результат чего? Вычитания, умножения?
Вычитания
S
Функция вычитает
BT
Из чего что
S
Натуральные числа
S
Из первого второе
М
Из 3 вычти 5
g
Ну вы тут умные сидите
BT
Это же не всегда работает