environ
vocabularies HIDDEN, SCMFSA_2, AMI_1, SCMFSA6A, ORDINAL4, AMI_3, SCMFSA8A, CARD_1, AMISTD_2, NAT_1, ARYTM_3, SUBSET_1, SCMFSA8B, AMISTD_1, SCMFSA_9, FUNCT_4, FUNCOP_1, RELAT_1, XBOOLE_0, TARSKI, FUNCT_1, NUMBERS, XXREAL_0, VALUED_1, RELOC, PARTFUN1, ARYTM_1, SCMFSA_7, COMPOS_1, SCMPDS_5, TURING_1, CARD_3, MEMSTR_0, STRUCT_0, GOBRD13, SCMPDS_4, AFINSQ_1;
notations HIDDEN, TARSKI, XBOOLE_0, RELAT_1, FUNCT_1, SUBSET_1, PARTFUN1, FUNCOP_1, FUNCT_4, FUNCT_7, ORDINAL1, CARD_1, CARD_3, AFINSQ_1, NUMBERS, XXREAL_0, XCMPLX_0, NAT_1, NAT_D, XXREAL_2, VALUED_1, STRUCT_0, MEMSTR_0, COMPOS_0, AMISTD_1, EXTPRO_1, COMPOS_1, COMPOS_2, SCMFSA_1, SCMFSA_2, SCMFSA6A, SCMFSA8A;
definitions COMPOS_1, AMISTD_1, TARSKI;
theorems AFINSQ_1, SCMFSA6A, SCMFSA8A, FUNCT_4, FUNCOP_1, ZFMISC_1, XREAL_1, XXREAL_0, NAT_1, COMPOS_1, TARSKI, SCMFSA7B, COMPOS_0, VALUED_1, PARTFUN1, XBOOLE_0, SCMFSA_4, FUNCT_7, AMISTD_1, SCMFSA10, MEMSTR_0, ORDINAL1, SCMFSA_2, FUNCT_1, CARD_3, AMISTD_2, XREAL_0, COMPOS_2;
schemes ;
registrations CARD_1, ORDINAL1, AFINSQ_1, COMPOS_1, XCMPLX_0, NAT_1, SCMFSA6A, FUNCT_4, FUNCOP_1, XXREAL_0, RELSET_1, XREAL_0, VALUED_1, FINSET_1, XBOOLE_0, COMPOS_0, SCMFSA_2, FUNCT_7, SCMFSA10, AMISTD_1, COMPOS_2, CARD_3, FUNCT_1, INT_1, SCMFSA6B, SCMFSA6C, MEMSTR_0, AMISTD_2, EXTPRO_1, STRUCT_0, AMI_3, SCMFSA_M;
constructors HIDDEN, SCMFSA_2, SCMFSA6A, SCMFSA_1, SCMFSA8A, XCMPLX_0, SUBSET_1, FUNCT_4, NAT_1, FUNCOP_1, CARD_3, DOMAIN_1, VALUED_1, PARTFUN1, FUNCT_7, AMISTD_1, PRE_POLY, SCMFSA10, COMPOS_2, XXREAL_2, RELSET_1, NAT_D, AMISTD_2;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities SCMFSA6A, COMPOS_1, FUNCOP_1, VALUED_1, XCMPLX_0, ORDINAL1, SCMFSA8A, AMISTD_1, MEMSTR_0, COMPOS_2;
expansions AFINSQ_1, MEMSTR_0, COMPOS_0, COMPOS_1;
Lm1:
card (Stop SCM+FSA) = 1
by AFINSQ_1:34;
Lm2:
(Stop SCM+FSA) . 0 = halt SCM+FSA
;
Lm3:
0 in dom (Stop SCM+FSA)
by COMPOS_1:3;
Lm4:
for i being No-StopCode Instruction of SCM+FSA holds Directed (Macro i) = (Macro i) ';' (Goto 1)
Lm5:
for I being Program of
for k being Nat holds stop (I ';' (Goto k)) = I ';' (Macro (goto k))