検索事例
地獄の作業例。
reserve i,j,k,l,m,n for natural number;
i+k = j+k implies i=j;
proof
defpred P[natural number] means
i+$1 = j+$1 implies i=j;
A1: P[0]
proof
assume
B0: i+0 = j+0;
B1: i+0 = i by INDUCT:3;
B2: j+0 = j by INDUCT:3;
hence thesis by B0,B1,B2;
end;
A2: for k st P[k] holds P[succ k]
proof
let l such that C1: P[l];
assume C2: i+succ l=j+succ l;
then C3: succ(i+l) = j+succ l by C2,INDUCT:4
.= succ(j+l) by INDUCT:4;
hence thesis by C1,INDUCT:2;
end;
for k holds P[k] from INDUCT:sch 1(A1,A2);
hence thesis;
end;
http://webmizar.cs.shinshu-u.ac.jp/mmlfe/current/ でメチャクチャ助かる。
- natural -> ordinal1
- number -> ordinal1
- + -> たくさん 153個。ordinal1を文字列検索 nat_1 と目星。
- 0 -> numbers, ordinal1, qc_lang1、ordinal1だろう。
- defpredは予約語らしい。予約語一覧を見る。
- $1 はワカランが、たぶん言語の構文。
- INDUCTはアーティクル名だが存在せず。$MIZFILES/abst/ で確認。
- succ -> aofa_a00, comput_1, ordinal1, ordinal4, trees_2, trees_9、おそらくordinal1。
INDUCTがなくなっているので、次の定理が不明
- INDUCT:3
- INDUCT:4
- INDUCT:2
次のスキーマが不明
- INDUCT:sch 1
内容を予想するに、
- INDUCT:3 ∀n:Na. n + 0 = n
- INDUCT:4 ∀n, m:Nat. n + suc(m) = suc(n + m)
- INDUCT:2
不明分かった、INDUCT:2 ∀n, m:Nat. succ n = succ m ⇒ n = m - INDUCT:sch 1 自然数に関する数学的帰納法
要するに、ペアノ自然数の定義、加法の帰納的定義、数学的帰納法。
定理検索機能がないので、行き詰まり。mml/に総grepかけた結果は、
grep -nH -i induction *.miz
abcmiz_1.miz:4655:begin :: Structural induction
afinsq_1.miz:1090::: Scheme of induction for extended finite sequences
cgames_1.miz:704:begin :: Schemes of induction
finseq_1.miz:1491::: scheme of induction for finite sequences ::
hilbert2.miz:1::: Defining by structural induction in the positive propositional language
hilbert2.miz:832:begin :: Defining by structural induction
lattice7.miz:40:begin :: Induction in a finite lattice
nat_1.miz:92:::$N The Principle of Mathematical Induction
ordinal1.miz:1::: The Ordinal Numbers. Transfinite Induction and Defining by
ordinal1.miz:2::: Transfinite Induction
ordinal1.miz:511::: 6. Transfinite induction and principle of minimum of ordinals
ordinal1.miz:550:::$N Transfinite induction
ordinal1.miz:1043::: 10. Schemes of definability by transfinite induction
rewrite1.miz:1146: coNoetherianInduction{R() -> Relation, P[object]}:
rewrite1.miz:1883:A30: for a being object st a in field R holds P[a] from coNoetherianInduction
sgraph1.miz:522::: here is the induction principle on SIMPLEGRAPHS(X).
stacks_1.miz:683:begin :: Schemes of Induction
wellfnd1.miz:464::: Well-founded induction
wellfnd1.miz:493::: WF iff WFInduction
wellfnd1.miz:553: WFInduction {R() -> non empty RelStr, P[set]}: for x being Element of R()
zf_lang.miz:2245::: The Structural Induction Schemes
zf_lang1.miz:725: ZFInduction { P[ZF-formula] } : for H holds P[H]
zf_lang1.miz:999: for H holds Etha[H] from ZFInduction(A10,A25,A1,A19);
zf_lang1.miz:1025: P[p] from ZFInduction(A3,A4,A1,A2);
zf_lang1.miz:2119: for H holds P[H] from ZFInduction(A6,A1,A2,A3);
zf_lang1.miz:2148: for H holds P[H] from ZFInduction(A3,A4,A1,A2);
zf_lang1.miz:2740: for H holds P[H] from ZFInduction(A5,A1,A2,A3);
zf_model.miz:1::: Models and Satisfiability. Defining by Structural Induction and
ordinal1.absを見て、次が数学的帰納法（超限帰納法）だろうと目星。
::$N Transfinite induction
scheme :: ORDINAL1:sch 2
TransfiniteInd { P[Ordinal] } : for A holds P[A]
provided
for A st for C st C in A holds P[C] holds P[A];
