environ
vocabularies HIDDEN, NUMBERS, ORDINAL1, SETFAM_1, ARYTM_1, ARYTM_3, CARD_1, SUBSET_1, AMI_1, XBOOLE_0, RELAT_1, TARSKI, FUNCOP_1, GLIB_000, GOBOARD5, AMISTD_1, FUNCT_1, CARD_3, FRECHET, STRUCT_0, FSM_1, FUNCT_4, TURING_1, CIRCUIT2, AMISTD_2, PARTFUN1, EXTPRO_1, NAT_1, RELOC, XXREAL_0, COMPOS_1, QUANTAL1, GOBRD13, MEMSTR_0;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, PBOOLE, CARD_1, NUMBERS, XCMPLX_0, XXREAL_0, NAT_1, CARD_3, FINSEQ_1, FUNCOP_1, NAT_D, FUNCT_7, VALUED_0, VALUED_1, AFINSQ_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, MEASURE6, EXTPRO_1, AMISTD_1;
definitions AMISTD_1, XBOOLE_0, TARSKI, COMPOS_0;
theorems AMISTD_1, FUNCOP_1, FUNCT_1, FUNCT_4, GRFUNC_1, MCART_1, SETFAM_1, TARSKI, CARD_3, XBOOLE_0, PARTFUN1, VALUED_1, COMPOS_1, EXTPRO_1, ORDINAL1, NAT_1, MEMSTR_0, COMPOS_0;
schemes NAT_1;
registrations RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, MEMBERED, CARD_3, STRUCT_0, AMISTD_1, CARD_1, FUNCT_4, AFINSQ_1, EXTPRO_1, MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0;
constructors HIDDEN, WELLORD2, REALSET1, NAT_D, AMISTD_1, XXREAL_2, PRE_POLY, AFINSQ_1, ORDINAL4, VALUED_1, NAT_1, FUNCT_7, PBOOLE, FUNCT_4, MEMSTR_0, RELSET_1, MEASURE6, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities COMPOS_1, EXTPRO_1, AMISTD_1, XBOOLE_0, FUNCOP_1, NAT_1, AFINSQ_1, VALUED_1, MEMSTR_0, COMPOS_0, XTUPLE_0;
expansions AMISTD_1, XBOOLE_0;
Lm1:
for N being with_zero set
for I being Instruction of (Trivial-AMI N) holds JumpPart I = 0
Lm2:
for N being with_zero set
for T being InsType of the InstructionsF of (Trivial-AMI N) holds JumpParts T = {0}