begin
:: deftheorem defines Relocated SCMFSA_5:def 1 :
Lm1:
NAT misses Int-Locations \/ FinSeq-Locations
by SCMFSA_2:13, SCMFSA_2:14, XBOOLE_1:70;
theorem Th1:
theorem Th2:
theorem Th3:
theorem Th4:
theorem Th5:
theorem Th6:
theorem Th7:
theorem Th8:
theorem Th9:
theorem Th10:
begin
theorem
theorem Th12:
for
k being
Element of
NAT for
p being
autonomic FinPartState of
SCM+FSA for
s1,
s2 being
State of
SCM+FSA st
IC SCM+FSA in dom p &
p c= s1 &
Relocated p,
k c= s2 holds
for
i being
Element of
NAT holds
(
(IC (Computation s1,i)) + k = IC (Computation s2,i) &
IncAddr (CurInstr (Computation s1,i)),
k = CurInstr (Computation s2,i) &
(Computation s1,i) | (dom (DataPart p)) = (Computation s2,i) | (dom (DataPart (Relocated p,k))) &
DataPart (Computation (s1 +* (DataPart s2)),i) = DataPart (Computation s2,i) )
theorem Th13:
theorem Th14:
theorem Th15:
theorem Th16:
theorem Th17:
theorem