begin
theorem
:: deftheorem Def1 defines relocable AMISTD_5:def 1 :
for N being non empty with_non-empty_elements set
for S being standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting AMI-Struct of N
for I being Instruction of S holds
( I is relocable iff for j, k being natural number
for s being State of S holds Exec ((IncAddr (I,(j + k))),(IncIC (s,k))) = IncIC ((Exec ((IncAddr (I,j)),s)),k) );
:: deftheorem Def2 defines relocable AMISTD_5:def 2 :
for N being non empty with_non-empty_elements set
for S being standard-ins homogeneous regular J/A-independent non empty IC-Ins-separated halting AMI-Struct of N holds
( S is relocable iff for I being Instruction of S holds I is relocable );
theorem Th2:
:: deftheorem Def3 defines IC-recognized AMISTD_5:def 3 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated halting AMI-Struct of N holds
( S is IC-recognized iff for q being NAT -defined the Instructions of b2 -valued finite non halt-free Function
for p being b3 -autonomic FinPartState of S st not p is empty holds
IC in dom p );
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
:: deftheorem Def4 defines CurIns-recognized AMISTD_5:def 4 :
for N being non empty with_non-empty_elements set
for S being non empty IC-Ins-separated halting AMI-Struct of N holds
( S is CurIns-recognized iff for q being NAT -defined the Instructions of b2 -valued finite non halt-free Function
for p being non empty b3 -autonomic FinPartState of S
for s being State of S st p c= s holds
for P being Instruction-Sequence of S st q c= P holds
for i being Element of NAT holds IC (Comput (P,s,i)) in dom q );
theorem
for
N being non
empty with_non-empty_elements set for
S being
standard-ins non
empty IC-Ins-separated halting IC-recognized AMI-Struct of
N st
S is
CurIns-recognized holds
for
q being
NAT -defined the
Instructions 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))) )
theorem
theorem Th9:
theorem Th10:
theorem Th11:
definition
let N be non
empty with_non-empty_elements set ;
let S be
standard-ins homogeneous regular J/A-independent proper-halt non
empty IC-Ins-separated halting relocable IC-recognized AMI-Struct of
N;
attr S is
relocable1 means :
Def5:
for
k being
Element of
NAT for
q being
NAT -defined the
Instructions 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
IC in dom p &
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)));
attr S is
relocable2 means :
Def6:
for
k being
Element of
NAT for
q being
NAT -defined the
Instructions 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
IC in dom p &
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
(Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p));
end;
:: deftheorem Def5 defines relocable1 AMISTD_5:def 5 :
for N being non empty with_non-empty_elements set
for S being standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized AMI-Struct of N holds
( S is relocable1 iff for k being Element of NAT
for q being NAT -defined the Instructions 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 IC in dom p & 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))) );
:: deftheorem Def6 defines relocable2 AMISTD_5:def 6 :
for N being non empty with_non-empty_elements set
for S being standard-ins homogeneous regular J/A-independent proper-halt non empty IC-Ins-separated halting relocable IC-recognized AMI-Struct of N holds
( S is relocable2 iff for k being Element of NAT
for q being NAT -defined the Instructions 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 IC in dom p & 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 (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) );
Lm1:
for N being non empty with_non-empty_elements set
for k being Element of NAT
for q being NAT -defined the Instructions of (STC b1) -valued finite non halt-free Function
for p being b3 -autonomic FinPartState of (STC N)
for s1, s2 being State of (STC N) st IC in dom p & 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))) & (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)) )
theorem Th12:
theorem Th13:
theorem
theorem