environ
vocabularies HIDDEN, NUMBERS, SUBSET_1, AMI_1, SCMFSA_2, EXTPRO_1, FUNCT_4, AMI_3, FUNCOP_1, RELAT_1, FUNCT_1, TARSKI, XBOOLE_0, CARD_1, CAT_1, NAT_1, ARYTM_3, XXREAL_0, AMISTD_2, VALUED_1, FSM_1, GRAPHSP, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, SCMFSA6A, RELOC, MEMSTR_0, SCMPDS_4, TURING_1, AMISTD_1, FRECHET, COMPOS_1, SCMPDS_5;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, COMPLEX1, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1, FINSEQ_2, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, NAT_D, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1, AMISTD_2, FUNCOP_1, XXREAL_0, SCMFSA_M;
definitions AFINSQ_1, COMPOS_0, COMPOS_1, AMISTD_1;
theorems FUNCT_2, RELAT_1, FUNCT_7, FUNCT_4, FUNCT_1, ZFMISC_1, FUNCOP_1, TARSKI, NAT_1, SCMFSA_4, SCMFSA_2, CARD_1, CARD_2, ENUMSET1, GRFUNC_1, RELSET_1, XBOOLE_0, XBOOLE_1, VALUED_1, AFINSQ_1, COMPOS_1, EXTPRO_1, COMPOS_0, SCMFSA_M, PARTFUN1, AMISTD_1, SCMFSA10;
schemes ;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1, XREAL_0, INT_1, SCMFSA_2, FUNCT_4, RELAT_1, VALUED_1, SCMFSA10, AMISTD_2, COMPOS_1, EXTPRO_1, AMI_3, COMPOS_0, NAT_1, CARD_1, AMISTD_1, COMPOS_2, AFINSQ_1;
constructors HIDDEN, WELLORD2, DOMAIN_1, XXREAL_0, INT_2, AMISTD_2, SCMFSA_2, RELSET_1, VALUED_1, AMI_3, PRE_POLY, AMISTD_1, FUNCT_7, MEMSTR_0, SCMFSA_1, SCMFSA_M, NAT_D, COMPOS_2, AFINSQ_1;
requirements HIDDEN, NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
equalities FUNCOP_1, COMPOS_1, FUNCT_4, MEMSTR_0;
expansions COMPOS_1;
canceled;
set q = (intloc 0) .--> 1;
set f = the_Values_of SCM+FSA;
Lm1:
for I being preProgram of SCM+FSA holds card (Directed I) = card I
Lm2:
for I being Program of holds card (stop (Directed I)) = card (stop I)