「ゲーム・プログラミング(5) - 非専門的シンギュラリティー研究所」で証明を迷路のようにしたものを生成AIで作ってもらいましたが、迷路にはなっていないのですが改造すれば使えそうなものができたので、これを改造して使うことにしました。迷路とは言えないので「証明路」と呼ぶことにします。将来的にはテキストを入れ替えることによっていろいろな証明に対応できるようにしますが、今は
- 整域において素元は既約元である
- UFDにおいて既約元は素元である
ということの証明をたどることができるものになっています。
「証明路」は以下のようにツリーの形式に変更しました。このため、主要な部分は全面的に書き直しました。
「証明路」ツリーのテキストの形式
テキストの先頭に以下のような文字があるときは、ノードの種類を表します。先頭に何もないときは下位のノードは上から順に進むことを表します。
変数名、数値は1文字の文字列です。
選択
形式: ◆テキスト
下位のノードの一つを選択することを表します。
定義の引用
形式: ★テキスト
定義を引用することを表します。
ゴール
形式: ■テキスト
ゴールであることを表します。
変数の値の設定
形式: ＝vnテキスト
v: 変数名
n: 数値
v と n のビットごとの論理積を v に設定します。v に何も設定されていないときの値は 0 です。
選択可能条件(論理積)
形式: ▲vnテキスト
v: 変数名
n: 数値
v と n のビットごとの論理積が 0 ではないときこの選択肢は選択可能であることを表します。
選択可能条件(論理積の否定)
形式: ▼vnテキスト
v: 変数名
n: 数値
v と n のビットごとの論理積が 0 のときこの選択肢は選択可能であることを表します。
テキスト内部のハイライト
これはテキストの先頭ではなく任意の部分に書くことができます。
形式: ＜ハイライトテキスト＞vn
v: 変数名
n: 数値
テキストにこの文字列を埋め込むと
- v と n のビットごとの論理積が 0 ではないときハイライトされて表示されます。
- v と n のビットごとの論理積が 0 のときはそのまま表示されます。
