begin
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
Element of
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
Element of
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
Element of
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 Element of 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 Element of 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 Element of 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 Element of 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))) )