environ
vocabularies HIDDEN, NUMBERS, AMI_3, AMI_1, FSM_1, ORDINAL1, CAT_1, XBOOLE_0, FUNCT_1, RELAT_1, FINSEQ_1, CARD_1, AMISTD_2, GRAPHSP, CARD_3, AMISTD_1, SUBSET_1, CIRCUIT2, FUNCT_4, FUNCOP_1, SETFAM_1, XXREAL_0, TARSKI, ARYTM_3, GOBOARD5, FRECHET, ARYTM_1, INT_1, PARTFUN1, NAT_1, COMPOS_1, GOBRD13, MEMSTR_0;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, FUNCOP_1, PARTFUN1, FINSEQ_1, FUNCT_4, XXREAL_0, VALUED_1, CARD_3, FUNCT_7, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_3, AMISTD_1, AMISTD_2;
definitions TARSKI, AMISTD_1, AMISTD_2, XBOOLE_0, COMPOS_0;
theorems TARSKI, NAT_1, AMI_3, FUNCT_4, AMI_5, FUNCT_1, FUNCOP_1, SETFAM_1, AMISTD_1, FINSEQ_1, MEMSTR_0, FUNCT_7, CARD_3, XBOOLE_0, XBOOLE_1, NAT_D, ORDINAL1, PARTFUN1, PBOOLE, VALUED_1, EXTPRO_1, AMI_2, COMPOS_0, XTUPLE_0;
schemes ;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, NAT_1, INT_1, FINSEQ_1, CARD_3, AMI_3, AMISTD_2, FUNCT_4, VALUED_0, EXTPRO_1, FUNCT_7, PRE_POLY, MEMSTR_0, CARD_1, COMPOS_0, XTUPLE_0;
constructors HIDDEN, NAT_D, AMI_3, AMISTD_2, RELSET_1, AMISTD_1, PRE_POLY, FUNCT_7, DOMAIN_1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities AMISTD_1, AMI_3, FUNCOP_1, COMPOS_1, EXTPRO_1, NAT_1, MEMSTR_0, COMPOS_0, XTUPLE_0;
expansions AMISTD_1, XBOOLE_0;
Lm1:
for i being Instruction of SCM st ( for l being Element of NAT holds NIC (i,l) = {(l + 1)} ) holds
JUMP i is empty
Lm2:
dl. 0 <> dl. 1
by AMI_3:10;