i, j, k, l, m, n は 自然 数 とする。 このとき i + k = j + k ならば i = j 証明: まず 述語を定義する: P[自然 数] とは i + $1 = j + $1 ならば i=j であること。 (A1): P[0] ※帰納法のベース 証明: 次を仮定する: (B0): i + 0 = j + 0 。 このとき (B1)…

http://fm.mizar.org/contents.html より： Title: Tarski Grothendieck Set Theory Author: Andrzej Trybulec Year: 1990 Identifier: TARSKI PDF URL: http://fm.mizar.org/1990-1/pdf1-1/tarski.pdf Summary: This is the first part of the axiomatics o…

名前がないからどうにもならないが、名無し／メタ情報なしでも、 特定シンボル（述語名、関数名、モード名、属性名）を含む定理 特定のプロファイルの特定のシンボルを含む定理 特定のアーティクルで定義された特定のシンボルを含む定理 存在命題、全称命題…

http://www.chimaira.org/archive/MizarLightForHOLLight_miz.ps.pdf より、 :: The drinker's principle reserve x for object; ex x st P x implies for y holds P y proof per cases; suppose A0: ex x st not P x; consider a such that A1: not P a by …

the system Declare by D. Syme ？？ 不明 the Mizar mode for HOL by J.Harrison http://www.cl.cam.ac.uk/~jrh13/papers/mizar.html the Isar language for Isabelle by M. Wenzel http://isabelle.in.tum.de/Isar/ Mizar-light for HOLlight by F. Wiedij…

地獄の作業例。 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 thesi…