サンプルを動くようにする： ほぼ解決

::> 121: Disagreement of argument types
::> 191: Unknown scheme

これの原因は、environ部の不備だった。

schemes NAT_1; だけではスキームのインポートが出来ない。 constructors NAT_1; が必須、これがないとUnknown schemeが出る。registrations NAT_1; も必須、これがないとDisagreementエラーが出る。

environ
:: Self
 vocabularies EX03;

:: 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
:: スキームだけインポートしても、NAT_1:sch が認識されない。
:: notations NAT_1;
 constructors NAT_1; :: 必須、これがないと"Unknown scheme"エラー。
 registrations NAT_1; :: 必須、これがないと"Disagreement of argument types"エラー。
:: theorems NAT_1;
 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;
  ::hereupon
    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;