environ
vocabularies HIDDEN, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, CAT_1, FINSET_1, NAT_1, AFINSQ_1, AMISTD_1, AMISTD_2, ARYTM_1, VALUED_1, PARTFUN1, ZFMISC_1, AMI_1, ARYTM_3, EXTPRO_1, PBOOLE, COMPOS_1, RELOC, TURING_1, XXREAL_0, SCMFSA_7, INT_1, SCMPDS_4, ORDINAL4, SCMFSA6A, FINSEQ_1;
notations HIDDEN, TARSKI, XBOOLE_0, ZFMISC_1, XTUPLE_0, MCART_1, SUBSET_1, SETFAM_1, ORDINAL1, PBOOLE, FUNCT_7, CARD_1, CARD_3, XXREAL_0, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FINSET_1, NUMBERS, INT_1, NAT_1, NAT_D, FUNCOP_1, FUNCT_4, FINSEQ_1, FUNCT_2, DOMAIN_1, VALUED_0, VALUED_1, AFINSQ_1, STRUCT_0, COMPOS_0;
definitions TARSKI, XBOOLE_0, AFINSQ_1;
theorems ZFMISC_1, FUNCT_2, TARSKI, FUNCT_4, FUNCOP_1, FINSET_1, FUNCT_1, GRFUNC_1, RELAT_1, RELSET_1, XBOOLE_0, XBOOLE_1, ORDINAL1, MCART_1, PARTFUN1, CARD_1, AFINSQ_1, XREAL_1, VALUED_1, CARD_2, PRE_CIRC, XREAL_0, NAT_1, XXREAL_0, NAT_D, INT_1, WELLORD2, ENUMSET1, AFINSQ_2, COMPOS_0;
schemes FRAENKEL, CLASSES1, FUNCT_7, DOMAIN_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2, FUNCOP_1, FUNCT_4, FINSET_1, XREAL_0, RELSET_1, PBOOLE, AFINSQ_1, VALUED_1, XCMPLX_0, NAT_1, MEMBERED, CARD_1, XXREAL_0, ORDINAL5, COMPOS_0, XTUPLE_0;
constructors HIDDEN, SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, RELSET_1, FUNCT_7, PRE_POLY, PBOOLE, AFINSQ_1, NAT_D, WELLORD2, STRUCT_0, COMPOS_0, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities FUNCOP_1, AFINSQ_1, VALUED_1, COMPOS_0, XTUPLE_0;
expansions TARSKI, XBOOLE_0;
Lm2:
for S being COM-Struct holds (card (Stop S)) -' 1 = 0
Lm3:
for S being COM-Struct holds LastLoc (Stop S) = 0
Lm4:
for k being Nat holds - 1 < k
;
Lm5:
for k being Nat
for a, b, c being Element of NAT st 1 <= a & 2 <= b & not k < a - 1 & not ( a <= k & k <= (a + b) - 3 ) & not k = (a + b) - 2 & not (a + b) - 2 < k holds
k = a - 1
Lm6:
for S being COM-Struct
for F, G being Program of S
for f being Nat st f < (card F) - 1 holds
F . f = (F ';' G) . f
:: halt SCM-Instr, zamiast halt SCM, zreszta wyrzucenie jej
:: spowodowaloby problemy z typowaniem.