情報検索法 - (保存用) 檜山正幸のキマイラ飼育記メモ編

http://fm.mizar.org/contents.html からMML IDで探す。

例 Volume 1, 1990 http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf
例 Volume 2, 1991 http://fm.mizar.org/1991-2/pdf2-3/oppcat_1.pdf

テンプレは、http://fm.mizar.org/{年}-{巻}/pdf{巻}-{号}/{小文字ID} 。

ライブラリ収録版はおそらく http://mizar.org/JFM/pdf/{小文字ID}.pdf IDは小文字！！

例題は、スライド http://mizar.org/cicm_tutorial/mizar.pdf (July 29, 2016) の45ページにあったのコード

reserve i,j,k,l,m,n for natural number;
i+k = j+k implies i=j;
proof

2行目のセミコロンは構文間違い。

INDUCTはない。ls ind*.abs で分かる。*.miz で grep -i inductionが引っかからなかったが、*.absならあった。

grep -nH  -i induction *.abs
grep: warning: GREP_OPTIONS is deprecated; please use an alias or script
abcmiz_1.abs:1305:begin :: Structural induction
afinsq_1.abs:380::: Scheme of induction for extended finite sequences
cgames_1.abs:222:begin :: Schemes of induction
finseq_1.abs:388::: scheme of induction for finite sequences ::
hilbert2.abs:1::: Defining by structural induction in the positive propositional language
hilbert2.abs:209:begin :: Defining by structural induction
lattice7.abs:33:begin :: Induction in a finite lattice
nat_1.abs:66:::$N The Principle of Mathematical Induction
ordinal1.abs:1::: The Ordinal Numbers. Transfinite Induction and Defining by
ordinal1.abs:2::: Transfinite Induction
ordinal1.abs:182::: 6. Transfinite induction and principle of minimum of ordinals
ordinal1.abs:190:::$N Transfinite induction
ordinal1.abs:304::: 10. Schemes of definability by transfinite induction
rewrite1.abs:350:  coNoetherianInduction{R() -> Relation, P[object]}:
sgraph1.abs:212::: here is the induction principle on SIMPLEGRAPHS(X).
stacks_1.abs:268:begin :: Schemes of Induction
wellfnd1.abs:139::: Well-founded induction
wellfnd1.abs:149::: WF iff WFInduction
wellfnd1.abs:157:  WFInduction {R() -> non empty RelStr, P[set]}: for x being Element of R()
zf_lang.abs:678:::               The Structural Induction Schemes
zf_lang1.abs:287:  ZFInduction { P[ZF-formula] } : for H holds P[H]
zf_model.abs:1::: Models and Satisfiability. Defining by Structural Induction and

それからは今日の努力 2016-12-14 - 檜山正幸のキマイラ飼育記メモ編