操作方法の仕様は以下のようになります。
操作方法
上下左右のキーで操作します。「前進モード」と「選択モード」があります。初期値は「前進モード」です。この操作で進んでゴールに到達すれば終了です。
前進モードのとき
下キー
- 選択ノード(下位のノードから選択するノード)のとき
- 下位の選択可能なノードがあるとき
- 下位の最初の選択可能なノードに移動
- 現在の表示はそのまま
- その下に道と選択候補テキストを表示
- 選択モードにする
- 下位の選択可能なノードがないとき
- 何もしない
- 下位の選択可能なノードがあるとき
- 選択ノード(下位のノードから選択するノード)ではないとき
- 次の兄弟ノードがあるとき
- 次の兄弟ノードに移動
- 現在の表示はそのまま
- その下に道とテキストを表示
- 次の兄弟ノードがないとき
- 何もしない
- 次の兄弟ノードがあるとき
上キー
- 前の兄弟ノードがあるとき
- 前の兄弟ノードに移動
- 現在の表示とその上の道の表示を消す
- 前の兄弟ノードがないとき
- 何もしない
左右キー
- 何もしない
選択モードのとき
下キー
- 下位の選択可能なノードがあるとき
- 下位の最初の選択可能なノードに移動
- 現在の表示はそのまま
- その下に道とテキストを表示
- 前進モードに戻す
- 下位の選択可能なノードがないとき
- 何もしない
上キー
- 上位のノードがあるとき
- 上位のノードに移動
- 現在の表示とその上の道の表示を消す
- 前進モードに戻す
- 上位のノードがないとき
- 何もしない
右キー
- 次の選択可能な兄弟ノードがあるとき
- 次の選択可能な兄弟ノードに移動
- 現在の表示を消す
- 選択候補テキストを表示
- 最初の選択可能な兄弟ノードがあるとき
- 最初の選択可能な兄弟ノードに移動
- 現在の表示を消す
- 選択候補テキストを表示
- 次の選択可能な兄弟ノードも最初の選択可能な兄弟ノードもないとき
- 何もしない
左キー
- 前の選択可能な兄弟ノードがあるとき
- 前の選択可能な兄弟ノードに移動
- 現在の表示を消す
- 選択候補テキストを表示
- 最後の選択可能な兄弟ノードがあるとき
- 最後の選択可能な兄弟ノードに移動
- 現在の表示を消す
- 選択候補テキストを表示
- 前の選択可能な兄弟ノードも最後の選択可能な兄弟ノードもないとき
- 何もしない
「証明路」ツリーの例
「証明路」ツリーは以下のようになります(これは動作が確認されたものではありません)。スペース1個のインデントで階層を表しています。
◆問題を選択
整域で素元ならば既約元
◆p は素元
★既約元の定義
◆p = ab とおく
★素元の定義
素元の定義の仮定(p | ab)が成立
◆＜p | a＞a1 または ＜p | b＞a2 が成立
▼a1p | a
◆p | a
★p | a の定義
a = pc と書ける
◆p = ab = (pc)b = p(cb)
★整域の定義
◆両辺を 0 以外で割ることができる
★素元の定義
p は 0 ではない
★素元の定義
◆p は 0 ではない
★整域の定義
両辺を 0 以外で割ることができる
両辺を p で割ることができる
1 = cb
b は単元
＝a1a が単元または b が単元
▼a2p | b
◆p | b
★p | b の定義
b = pd と書ける
◆p = ab = a(pd) = p(ad)
★整域の定義
◆両辺を 0 以外で割ることができる
★素元の定義
p は 0 ではない
★素元の定義
◆p は 0 ではない
★整域の定義
両辺を 0 以外で割ることができる
両辺を p で割ることができる
1 = ad
a は単元
＝a2a が単元または b が単元
▲a3ゴールへ
■ゴール
UFDで既約元ならば素元
◆p は既約元
★素元の定義
◆p | ab とおく
★p | ab の定義
◆pc = ab と書ける
★UFDの定義(分解可能)
a=a_1…a_m、b=b_1…b_n、c=c_1…c_k と既約元の積に分解できる
◆p・c_1…c_k = a_1…a_m・b_1…b_n
★UFDの定義(一意性)
p は a_1,…, a_m, b_1,…, b_n のどれかと同伴
◆p は ＜a_1,…, a_m のどれかと同伴＞b1 または ＜b_1,…, b_n のどれかと同伴＞b2
▼b1p は a_1,…, a_m のどれかと同伴
p は a_1,…, a_m のどれかと同伴
p | a
＝b1p | a または p | b
▼b2p は b_1,…, b_n のどれかと同伴
p は b_1,…, b_n のどれかと同伴
p | b
＝b2p | a または p | b
▲b3ゴールへ
■ゴール
