必死チェッカーもどきプログラム > 2015年01月13日

14 位/186 ID中	時間	0	1	2	3	4	5	6	7	8	9	10	11	12	13	14	15	16	17	18	19	20	21	22	23	Total
14 位/186 ID中	書き込み数	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	0	1	2	3

使用した名前一覧	書き込んだスレッド一覧
１	集合論に基づいた言語を作りたい

集合論に基づいた言語を作りたい 807 ：１[sage]：2015/01/13(火) 22:46:33.61 ID:ld5ZWEPI: Lemma l : forall (n:nat), even (1+n)-> odd n.
intros.
apply (even_plus_odd_inv_r 1).
apply H.
apply odd_S.
apply even_O.
Qed.
こう？

nを偶数と奇数に場合分けする方法がわからんとです。

集合論に基づいた言語を作りたい 808 ：１[sage]：2015/01/13(火) 23:04:11.48 ID:ld5ZWEPI: even(1+n)にeven(1+n) -> odd nをapplyして odd nにならんのか？
よくわからん。

集合論に基づいた言語を作りたい 810 ：１[sage]：2015/01/13(火) 23:38:41.86 ID:ld5ZWEPI: 証明済みのLemmaの活用の仕方がわからんです。
applyじゃないの？

※このページは、『２ちゃんねる』の書き込みを基に自動生成したものです。オリジナルはリンク先の２ちゃんねるの書き込みです。
※このサイトでオリジナルの書き込みについては対応できません。
※何か問題のある場合はメールをしてください。対応します。