kb84tkhrのブログ

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

定理証明手習い (43) set?/add-atomsの証明(続)

下記にオレンジ色で示したif式のQuestion部は、どちらも同じ(set? (add-atoms (cdr a) bs))という意味です。

知ってた

しかし、if-nest-Aif-nest-Eで単純な形にはできません。

先に言ってくれ!

続きを読む

定理証明手習い (42) set?/add-atomsの証明

テキストに沿って証明を進めます
ここ、自分で考えたらやっぱりけっこう大変なんだろうなあ

続きを読む

ScrapboxとWorkflowyとの使い分け

Scrapboxが楽しいんですがWorkflowyも捨てがたい
どうしたものですかね

続きを読む

定理証明手習い (41)

Defun帰納法はかなり適用範囲が広そうなやり方です

Defun帰納法は、自分たちで書くどんな関数でも使えるのでしょうか?
帰納的な主張を構成する方法にしろ、全域性の主張を構成する方法にしろ、どんな関数に対しても構成はできます。

ifの位置にもよるけど持ち上げればOK、とのこと

続きを読む

定理証明手習い (40) 種

リスト型帰納法やスター型帰納法はDefun帰納法に含まれるそうです

リスト型帰納法list-inductionから作ります

続きを読む

定理証明手習い (39) Defun式帰納法

Defun式帰納法、とか言ってまた難しく書いてあります
ていうか前よりわからないので今回も定義にしたがって追ってみます

続きを読む

定理証明手習い (38) 帰納法を作る

ということでadd-atoms用の帰納法が作れるのならどんなものでしょうか
list-inductionのときは主張を読んでみたら普通に帰納法だねって感じだったので
まず自分で普通に考えてみます

続きを読む