:: Relocability for { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 22, 1996
:: Copyright (c) 1996 Association of Mizar Users
:: 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: :: SCMFSA_5:1
theorem Th2: :: SCMFSA_5:2
theorem Th3: :: SCMFSA_5:3
theorem Th4: :: SCMFSA_5:4
theorem Th5: :: SCMFSA_5:5
theorem Th6: :: SCMFSA_5:6
theorem Th7: :: SCMFSA_5:7
theorem Th8: :: SCMFSA_5:8
theorem Th9: :: SCMFSA_5:9
theorem Th10: :: SCMFSA_5:10
theorem :: SCMFSA_5:11
theorem Th12: :: SCMFSA_5:12
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: :: SCMFSA_5:13
theorem Th14: :: SCMFSA_5:14
theorem Th15: :: SCMFSA_5:15
theorem Th16: :: SCMFSA_5:16
theorem Th17: :: SCMFSA_5:17
theorem :: SCMFSA_5:18