サンプルを動くようにする： 明らかな命題

environがホントに難しいが、environ部を（もし）書けたら、明らかな命題を確認する。

• 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;

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;

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;

(succ n)が定義できれば、INDUCT:* の代替になる。あとは、INDUCT:sch 1 自然数に関する数学的帰納法を、NAT_1:sch 2 で代替すれば良さそう。