kb84tkhrのブログ

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

2018-03-06から1日間の記事一覧

定理証明手習い (56) positive/wt

(+ (wt (car x)) (wt (car x)))は正の数ですか? (wt (car x))が正なら、正ですね。 そういう当たり前のことがね 次のような主張positive/wtを作れば、そのフォーカスをうまい前提に書き換えられますね。 (dethm positive/wt (x) (equal (< '0 (wt x)) 't)) …