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