Об умножение

[deni_ok]

Эти ваши интернеты бурлят:
ru-marazm.livejournal.com/3591670.html
lj.rossia.org/users/tiphareth/1685303.html
Агда, кстати, на стороне внучки, 9 раз по 2 литра будет 9 * 2:
_*_ : ℕ → ℕ → ℕ zero * n = zero suc m * n = n + (m * n) Впрочем внучке стоило бы снять все вопросы, предоставив доказательство
*-commutative : ∀ m n → m * n ≡ n * m Взяв

Comments

[nivanych]

Ну вот! Практическое использование, самое, что ни на есть!

[thedeemon]

умножения? :)

[nivanych]

Агды!
А как ещё докажешь учителю правоту?

[nealar]

Ты же сам рассказывал про нунчаки с цепочкой от собаки!

[deni_ok]

Эта система доказательств полна и непротиворечива. Слишком мощно для наших целей!

[nivanych]

Нунчаки, это overkill!

[nealar]

Полна и противоречива, скорей.

[deni_ok]

Противоречьями полна
Нас не устроила она.

[nivanych]

Йа не готов сидеть.
А так ничо, да - полна и непротиворечива ;-)

[thedeemon]

Сомневаюсь, что учитель примет доказательство на Агде. Скорее всего, потребует на Coq.

[nivanych]

Ох уж эти традиции французской школы!

[thedeemon]

Oui, monsieur. Скажет, таковы требования Gauronault.

[deni_ok]

Ну это если франкофон, то да.