environ
vocabularies HIDDEN, NUMBERS, AMI_1, SCMFSA_2, AMISTD_2, ARYTM_3, FUNCT_4, XBOOLE_0, FUNCT_1, RELAT_1, TARSKI, FSM_1, CIRCUIT2, CARD_1, XXREAL_0, EXTPRO_1, GRAPHSP, AMI_3, ARYTM_1, INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, NAT_1, RELOC, AMISTD_5, COMPOS_1, FINSET_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, FINSET_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_2, INT_1, NAT_1, PARTFUN1, RELAT_1, FUNCT_1, FINSEQ_1, FINSEQ_2, FUNCT_4, FUNCT_7, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, SCMFSA_2, XXREAL_0, AMISTD_5;
definitions AMISTD_5;
theorems GRFUNC_1, FUNCT_1, RELAT_1, SCMFSA_2, SCMFSA_3, SCMFSA_4, XBOOLE_0, XBOOLE_1, PBOOLE, PARTFUN1, COMPOS_1, EXTPRO_1, AMISTD_5, MEMSTR_0, AMI_2, COMPOS_0;
schemes NAT_1;
registrations FUNCT_1, XREAL_0, INT_1, SCMFSA_2, ORDINAL1, RELAT_1, AMISTD_2, SCMFSA10, COMPOS_1, EXTPRO_1, SCMFSA_4, SCMFSA_3, FUNCT_4, FINSEQ_1, AMI_3, COMPOS_0, NAT_1, MEMSTR_0;
constructors HIDDEN, DOMAIN_1, NAT_D, RELSET_1, FUNCT_7, PRE_POLY, AMISTD_2, SCMFSA_3, AMISTD_5, AMI_3, SCMFSA_1;
requirements HIDDEN, NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
equalities EXTPRO_1, MEMSTR_0, SCMFSA_2;
expansions AMISTD_5;
theorem Th1:
for
k being
Nat for
q being
NAT -defined the
InstructionsF of
SCM+FSA -valued finite non
halt-free Function for
p being non
empty b2 -autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
p c= s1 &
IncIC (
p,
k)
c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
SCM+FSA 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)) )