- プログラミング雑談スレ ♯♯ [転載禁止]©2ch.net
23 ：片山博文MZ ◆T6xkBnTXz7B0 [sage]：2015/01/13(火) 18:53:35.00 ID:gURRjQHf - 私はお下品
|
- 集合論に基づいた言語を作りたい
806 ：片山博文MZ ◆T6xkBnTXz7B0 [sage]：2015/01/13(火) 21:52:38.35 ID:gURRjQHf - ヒント。
Require Import Even.
Lemma eSr: forall n:nat, even (1 + n) -> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.
|
- 集合論に基づいた言語を作りたい
809 ：片山博文MZ ◆T6xkBnTXz7B0 [sage]：2015/01/13(火) 23:09:34.67 ID:gURRjQHf - Lemma oS: forall n:nat, even n -> odd (S n).
intros.
apply odd_S.
apply H.
Qed.
|
- 集合論に基づいた言語を作りたい
811 ：片山博文MZ ◆T6xkBnTXz7B0 [sage]：2015/01/13(火) 23:39:26.18 ID:gURRjQHf - replace (even (S n)) with (odd n).
apply even_or_odd.
もう少しだな。
|