environ
vocabularies HIDDEN, SUBSET_1, NUMBERS, AMI_1, AMI_3, AMISTD_2, ARYTM_3, GRAPHSP, CARD_1, RELAT_1, FUNCT_1, TARSKI, FUNCT_4, XBOOLE_0, FSM_1, CIRCUIT2, EXTPRO_1, ARYTM_1, INT_1, XXREAL_0, STRUCT_0, RELOC, FINSET_1, FINSEQ_1, NAT_1, AMISTD_5, COMPOS_1;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, NAT_1, VALUED_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, PBOOLE, FINSEQ_1, NAT_D, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_3, XXREAL_0, AMISTD_2, AMISTD_5;
definitions FUNCT_1, AMISTD_5;
theorems AMI_3, GRFUNC_1, TARSKI, FUNCT_4, FUNCT_1, AMI_5, RELAT_1, XBOOLE_1, PARTFUN1, VALUED_1, FINSEQ_1, COMPOS_1, EXTPRO_1, ORDINAL1, AMISTD_2, AMISTD_5, STRUCT_0, MEMSTR_0, AMI_2, COMPOS_0;
schemes NAT_1;
registrations FUNCT_1, ORDINAL1, XREAL_0, INT_1, AMI_3, FUNCT_4, AMI_6, VALUED_0, AMISTD_2, COMPOS_1, EXTPRO_1, NAT_1, FINSEQ_1, AMI_5, MEMSTR_0, COMPOS_0, XTUPLE_0;
constructors HIDDEN, DOMAIN_1, XXREAL_0, AMI_3, NAT_D, PRE_POLY, AMISTD_2, VALUED_1, AMI_2, AMISTD_1, AMISTD_5, PBOOLE, MEMSTR_0, RELSET_1, XTUPLE_0;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities EXTPRO_1, AMI_3, MEMSTR_0;
expansions AMISTD_5;
Lm1:
for k being Nat
for q being NAT -defined the InstructionsF of SCM -valued finite non halt-free Function
for p being non empty b2 -autonomic FinPartState of SCM
for s1, s2 being State of SCM st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of SCM st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )