begin
:: deftheorem RELOC:def 1 :
canceled;
:: deftheorem RELOC:def 2 :
canceled;
:: deftheorem Def3 defines IncAddr RELOC:def 3 :
theorem
canceled;
theorem
canceled;
theorem
canceled;
theorem
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
theorem Th11:
theorem Th12:
theorem Th13:
theorem Th14:
theorem
canceled;
theorem
canceled;
theorem
canceled;
:: deftheorem Def5 defines IncAddr RELOC:def 4 :
:: deftheorem defines Reloc RELOC:def 5 :
theorem
canceled;
theorem Th19:
:: deftheorem defines Relocated RELOC:def 6 :
theorem
canceled;
theorem Th21:
theorem Th22:
theorem Th23:
theorem Th24:
theorem Th25:
theorem Th26:
theorem Th27:
theorem Th28:
theorem Th29:
theorem Th30:
theorem Th31:
theorem Th32:
begin
theorem
for
k being
Element of
NAT for
p being
autonomic FinPartState of
SCM st
IC SCM in dom p holds
for
s being
State of
SCM st
p c= s holds
for
i being
Element of
NAT holds
Comput (ProgramPart (s +* (Relocated p,k))),
(s +* (Relocated p,k)),
i = ((Comput (ProgramPart s),s,i) +* (Start-At ((IC (Comput (ProgramPart s),s,i)) + k),SCM )) +* (ProgramPart (Relocated p,k))
Lm1:
for k being Element of NAT
for p being autonomic FinPartState of SCM
for s1, s2 being State of SCM st IC SCM in dom p & p c= s1 & Relocated p,k c= s2 holds
for i being Element of NAT holds
( (IC (Comput (ProgramPart s1),s1,i)) + k = IC (Comput (ProgramPart s2),s2,i) & IncAddr (CurInstr (ProgramPart s1),(Comput (ProgramPart s1),s1,i)),k = CurInstr (ProgramPart s2),(Comput (ProgramPart s2),s2,i) & (Comput (ProgramPart s1),s1,i) | (dom (DataPart p)) = (Comput (ProgramPart s2),s2,i) | (dom (DataPart (Relocated p,k))) & DataPart (Comput (ProgramPart s1),(s1 +* (DataPart s2)),i) = DataPart (Comput (ProgramPart s2),s2,i) )
theorem
theorem Th35:
theorem
theorem
theorem Th38:
theorem Th39:
theorem Th40:
for
k being
Element of
NAT for
p being
FinPartState of
SCM st
IC SCM in dom p holds
for
s being
State of
SCM st
p c= s &
Relocated p,
k is
autonomic holds
for
i being
Element of
NAT holds
Comput (ProgramPart s),
s,
i = (((Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i) +* (Start-At ((IC (Comput (ProgramPart (s +* (Relocated p,k))),(s +* (Relocated p,k)),i)) -' k),SCM )) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)
theorem Th41:
theorem Th42:
theorem