kb84tkhrのブログ

何を書こうか考え中です あ、あと組織とは関係ないってやつです 個人的なやつ

2018-04-16から1日間の記事一覧

定理証明手習い (89) J-Bob/prove

(rewrite/prove defs def seed steps) 関数定義なら全域性の主張、 定理なら帰納法の主張を証明します 違うのは種から主張をつくるところだけかな rewrite/prove+1 (defs pf e) そこまでの証明が終わっていれば次の証明を行う rewrite/prove+ (defs pfs) 複…