environ
vocabularies HIDDEN, NUMBERS, FUNCSDOM, SUBSET_1, AMI_3, AMI_1, FSM_1, STRUCT_0, AMI_2, TARSKI, ZFMISC_1, RELAT_1, FUNCOP_1, XBOOLE_0, CAT_1, FUNCT_1, CARD_1, GRAPHSP, FINSEQ_1, AMISTD_2, CARD_3, AMISTD_1, CIRCUIT2, FUNCT_4, SETFAM_1, SUPINF_2, ARYTM_3, XXREAL_0, GOBOARD5, ARYTM_1, GROUP_1, FRECHET, PARTFUN1, COMPOS_1, NAT_1, GOBRD13, MEMSTR_0;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, XTUPLE_0, MCART_1, SETFAM_1, RELAT_1, FUNCT_1, XXREAL_0, VALUED_1, STRUCT_0, ALGSTR_0, VECTSP_1, ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, NAT_1, FUNCOP_1, FINSEQ_1, PARTFUN1, FUNCT_4, CARD_3, FUNCT_7, GROUP_1, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, AMI_3, SCMRING1, SCMRING2, AMISTD_1, AMISTD_2, SCMRINGI;
definitions TARSKI, AMISTD_1, AMISTD_2, XBOOLE_0, COMPOS_0;
theorems TARSKI, NAT_1, SCMRING2, AMI_3, FUNCT_4, FUNCT_1, ZFMISC_1, FUNCOP_1, SCMRING1, SETFAM_1, AMISTD_1, STRUCT_0, AMI_2, RLVECT_1, LMOD_6, FINSEQ_1, CARD_3, ORDINAL1, XBOOLE_0, XBOOLE_1, ENUMSET1, PARTFUN1, PBOOLE, VALUED_1, EXTPRO_1, FUNCT_7, MEMSTR_0, COMPOS_0, XTUPLE_0;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, CARD_3, STRUCT_0, VECTSP_1, FINSET_1, AMI_3, SCMRING2, AMISTD_2, FUNCT_4, VALUED_0, EXTPRO_1, NAT_1, FUNCT_7, PRE_POLY, MEMSTR_0, CARD_1, COMPOS_0, XTUPLE_0, FINSEQ_1;
constructors HIDDEN, FINSEQ_4, REALSET2, AMI_3, SCMRING2, AMISTD_2, RELSET_1, AMISTD_1, FUNCT_7, PRE_POLY, SCMRING1, XTUPLE_0;
requirements HIDDEN, NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
equalities SCMRING2, AMISTD_1, FUNCOP_1, COMPOS_1, EXTPRO_1, NAT_1, MEMSTR_0, COMPOS_0, SCMRINGI, XTUPLE_0;
expansions AMISTD_1, XBOOLE_0, COMPOS_0;
Lm1:
for x, y being set st x in dom <*y*> holds
x = 1
Lm2:
for R being Ring
for T being InsType of the InstructionsF of (SCM R) holds
( T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 )
Lm3:
for R being Ring
for i being Instruction of (SCM R) st ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) holds
JUMP i is empty