g
Size: a a a
2020 November 08
АН
S
Но функция по определению считает, что если мы пытаемся из нуля вычесть что-то, то получаем 0, и я это доказал в первой же лемме
fun mul :: "nat ⇒ nat ⇒ nat"
where
"mul n 0 = 0" |
"mul n (Suc(m)) = n + mul n m"
lemma[simp]: "mul 0 m = 0"
apply (induction m)
apply auto
done
BT
А suc это что?
АН
Но функция по определению считает, что если мы пытаемся из нуля вычесть что-то, то получаем 0, и я это доказал в первой же лемме
fun mul :: "nat ⇒ nat ⇒ nat"
where
"mul n 0 = 0" |
"mul n (Suc(m)) = n + mul n m"
lemma[simp]: "mul 0 m = 0"
apply (induction m)
apply auto
done
че за яп то вообще
SR
Разве не твою подругу деанонили?
Магги?
BT
Магги?
+
S
че за яп то вообще
HOL
SR
@mggmgg привет ты как?
g
А suc это что?
Это сосать
М
Но функция по определению считает, что если мы пытаемся из нуля вычесть что-то, то получаем 0, и я это доказал в первой же лемме
fun mul :: "nat ⇒ nat ⇒ nat"
where
"mul n 0 = 0" |
"mul n (Suc(m)) = n + mul n m"
lemma[simp]: "mul 0 m = 0"
apply (induction m)
apply auto
done
Хуй знает че тут на этом твоем мордорском но явно не доказательство того что 2-3=0
S
Вернее Isabelle/HOL, прувер
g
А, ой
АН
HOL
hoHOL
BT
Это сосать
SR
hoHOL
Ахпхпх
Р
hoHOL
S
Хуй знает че тут на этом твоем мордорском но явно не доказательство того что 2-3=0
Ну я тебе привёл доказательство, что 0 - n = 0
BT
Ну я тебе привёл доказательство, что 0 - n = 0
А ебать
BT
Это ж верно