サンプルを動くようにする： 努力段階

environ

:: From NAT_1
 vocabularies NUMBERS, ORDINAL1, REAL_1, SUBSET_1, CARD_1, ARYTM_3, TARSKI,
      RELAT_1, XXREAL_0, XCMPLX_0, ARYTM_1, XBOOLE_0, FINSET_1, FUNCT_1, NAT_1,
      FUNCOP_1, PBOOLE, PARTFUN1, FUNCT_7, SETFAM_1, ZFMISC_1;

 notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, SUBSET_1, SETFAM_1, ORDINAL1,
      FINSET_1, CARD_1, PBOOLE, NUMBERS, XCMPLX_0, XREAL_0, XXREAL_0, RELAT_1,
      FUNCT_1, PARTFUN1, FUNCOP_1, FUNCT_2, BINOP_1;


 constructors NUMBERS, XCMPLX_0, XXREAL_0, XREAL_0, CARD_1, WELLORD2, FUNCT_2,
      PARTFUN1, FUNCOP_1, FUNCT_4, ENUMSET1, RELSET_1, PBOOLE, ORDINAL1,
      SETFAM_1, ZFMISC_1, BINOP_1;

 registrations SUBSET_1, ORDINAL1, NUMBERS, XXREAL_0, XREAL_0, CARD_1,
      RELSET_1, FUNCT_2, PBOOLE;

 requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;

:: Added
 schemes NAT_1;

begin

INDUCT2: for n, m being Nat holds n + 1 = m  + 1 implies n = m;
INDUCT3: for n being Nat holds n + 0 = n;
INDUCT4: for n, m being Nat holds n + (m + 1) = (n + m) + 1;


:: ::$N The Principle of Mathematical Induction
:: scheme :: NAT_1:sch 2
::   NatInd { P[Nat] } : for k being Nat holds P[k]
:: provided
::  P[0] and
::  for k be Nat st P[k] holds P[k + 1];

reserve i,j,k,l,m,n for Nat;

i+k = j+k implies i=j
proof
  defpred P[Nat] means
    i+$1 = j+$1 implies i=j;
  A1: P[0]
  proof
    assume
    B0: i+0 = j+0;
    B1: i+0 = i by INDUCT3;
    B2: j+0 = j by INDUCT3;
    hence thesis by B0,B1,B2;
  end;
  A2: for k be Nat st P[k] holds P[k + 1]
  proof
    let l such that C1: P[l];
    assume C2: i + (l + 1) = j + (l + 1);
    then C3: (i + l) + 1 = j + (l + 1) by C2,INDUCT4
    .= (j + l) + 1 by INDUCT4;
    hence thesis by C1,INDUCT2;
  end;
  for k holds P[k] from NAT_1:sch 2(A1,A2);
  hence thesis;
end;

結果は：

Running verifier on ex03 ...
Make Environment, Mizar Ver. 8.1.04 (Win32/FPC)
Copyright (c) 1990-2015 Association of Mizar Users

Verifier based on More Strict Mizar Processor, Mizar Ver. 8.1.04 (Win32/FPC)
Copyright (c) 1990-2015 Association of Mizar Users
Processing: c:/Users/hiyama/Work/tmp/mizar-test/text/ex03.miz

Parser   [  61]   0:00
MSM      [  62]   0:00
Analyzer [  62 *1]   0:00
Checker  [  62 *2]   0:00
Time of mizaring: 0:00
c:/Users/hiyama/Work/tmp/mizar-test/text/ex03.miz:52:34: *121: Disagreement of argument types
c:/Users/hiyama/Work/tmp/mizar-test/text/ex03.miz:60:23: *191: Unknown scheme

エラー箇所は、

  A2: for k be Nat st P[k] holds P[k + 1]
::>                              *121
  proof
    let l such that C1: P[l];
    assume C2: i + (l + 1) = j + (l + 1);
    then C3: (i + l) + 1 = j + (l + 1) by C2,INDUCT4
    .= (j + l) + 1 by INDUCT4;
    hence thesis by C1,INDUCT2;
  end;
  for k holds P[k] from NAT_1:sch 2(A1,A2);
::>                   *191
  hence thesis;
end;
::> 121: Disagreement of argument types
::> 191: Unknown scheme