environ
vocabularies HIDDEN, NUMBERS, ARYTM_1, ARYTM_3, CARD_1, AMI_1, XBOOLE_0, RELAT_1, TARSKI, FUNCOP_1, GLIB_000, GOBOARD5, AMISTD_1, FUNCT_1, STRUCT_0, VALUED_1, FSM_1, FUNCT_4, TURING_1, CIRCUIT2, AMISTD_2, PARTFUN1, EXTPRO_1, NAT_1, RELOC, AMISTD_5, COMPOS_1, MSUALG_1, FINSET_1, QUANTAL1, MEMSTR_0, SCMFSA6B;
notations HIDDEN, TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, SETFAM_1, MEMBERED, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, PBOOLE, FINSET_1, 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, MEASURE6, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1, AMISTD_2;
definitions EXTPRO_1, AMISTD_1, AMISTD_2;
theorems AMISTD_1, FUNCOP_1, FUNCT_1, FUNCT_4, GRFUNC_1, RELAT_1, TARSKI, ZFMISC_1, XBOOLE_0, XBOOLE_1, PBOOLE, PARTFUN1, VALUED_1, COMPOS_1, EXTPRO_1, NAT_D, AMISTD_2, MEMSTR_0, COMPOS_0;
schemes NAT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, FINSET_1, XREAL_0, NAT_1, AMISTD_1, FUNCT_4, RELSET_1, GRFUNC_1, ORDINAL1, VALUED_1, COMPOS_1, EXTPRO_1, AMISTD_2, MEMSTR_0, MEASURE6, COMPOS_0, XTUPLE_0;
constructors HIDDEN, WELLORD2, REALSET1, NAT_D, AMISTD_1, XXREAL_2, PRE_POLY, AFINSQ_1, ORDINAL4, VALUED_1, AMISTD_2, PBOOLE, RELSET_1, FUNCT_7, FUNCT_4, MEMSTR_0, MEASURE6, XTUPLE_0;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
equalities COMPOS_1, EXTPRO_1, FUNCOP_1, NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0;
expansions EXTPRO_1, AMISTD_1;
theorem
for
N being
with_zero set for
S being non
empty with_non-empty_values IC-Ins-separated halting IC-recognized CurIns-recognized AMI-Struct over
N for
q being
NAT -defined the
InstructionsF of
b2 -valued finite non
halt-free Function for
p being non
empty b3 -autonomic FinPartState of
S for
s1,
s2 being
State of
S st
p c= s1 &
p c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
S st
q c= P1 &
q c= P2 holds
for
i being
Nat holds
(
IC (Comput (P1,s1,i)) = IC (Comput (P2,s2,i)) &
CurInstr (
P1,
(Comput (P1,s1,i)))
= CurInstr (
P2,
(Comput (P2,s2,i))) )
definition
let N be
with_zero set ;
let S be non
empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over
N;
attr S is
relocable1 means :
Def5:
for
k being
Nat for
q being
NAT -defined the
InstructionsF of
S -valued finite non
halt-free Function for
p being non
empty b2 -autonomic FinPartState of
S for
s1,
s2 being
State of
S st
p c= s1 &
IncIC (
p,
k)
c= s2 holds
for
P1,
P2 being
Instruction-Sequence of
S st
q c= P1 &
Reloc (
q,
k)
c= P2 holds
for
i being
Nat holds
IncAddr (
(CurInstr (P1,(Comput (P1,s1,i)))),
k)
= CurInstr (
P2,
(Comput (P2,s2,i)));
end;
::
deftheorem Def5 defines
relocable1 AMISTD_5:def 5 :
for N being with_zero set
for S being non empty with_non-empty_values IC-Ins-separated halting relocable IC-recognized CurIns-recognized AMI-Struct over N holds
( S is relocable1 iff for k being Nat
for q being NAT -defined the InstructionsF of b2 -valued finite non halt-free Function
for p being non empty b4 -autonomic FinPartState of S
for s1, s2 being State of S st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of S st q c= P1 & Reloc (q,k) c= P2 holds
for i being Nat holds IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) );
Lm1:
for N being with_zero set
for k being Nat
for q being NAT -defined the InstructionsF of (STC b1) -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of (STC N)
for s1, s2 being State of (STC N) st p c= s1 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (STC N) 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))) )