:: Relocability for { \bf SCM } over Ring
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received February 6, 2004
:: Copyright (c) 2004 Association of Mizar Users
Lm1:
for a, A being set st A /\ {a} <> {} holds
a in A
theorem Th14: :: SCMRING4:1
theorem :: SCMRING4:2
theorem Th16: :: SCMRING4:3
theorem :: SCMRING4:4
theorem :: SCMRING4:5
theorem :: SCMRING4:6
theorem Th20: :: SCMRING4:7
theorem :: SCMRING4:8
theorem Th22: :: SCMRING4:9
theorem :: SCMRING4:10
theorem :: SCMRING4:11
canceled;
theorem :: SCMRING4:12
theorem Th26: :: SCMRING4:13
theorem :: SCMRING4:14
theorem :: SCMRING4:15
theorem :: SCMRING4:16
theorem :: SCMRING4:17
canceled;
theorem :: SCMRING4:18
theorem :: SCMRING4:19
theorem Th33: :: SCMRING4:20
theorem Th34: :: SCMRING4:21
theorem Th35: :: SCMRING4:22
theorem Th36: :: SCMRING4:23
theorem Th37: :: SCMRING4:24
theorem Th38: :: SCMRING4:25
theorem :: SCMRING4:26
theorem Th40: :: SCMRING4:27
theorem Th41: :: SCMRING4:28
theorem Th42: :: SCMRING4:29
theorem Th43: :: SCMRING4:30
theorem Th44: :: SCMRING4:31
theorem Th45: :: SCMRING4:32
theorem Th46: :: SCMRING4:33
theorem Th58: :: SCMRING4:34
theorem Th59: :: SCMRING4:35
for
k being
natural number for
R being
good Ring for
s1,
s2,
s being
State of
(SCM R) st not
R is
trivial holds
for
p being
autonomic FinPartState of
(SCM R) st
IC (SCM R) in dom p &
p c= s1 &
Relocated p,
k c= s2 &
s = s1 +* (DataPart 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 s,i) = DataPart (Computation s2,i) )
theorem Th60: :: SCMRING4:36
theorem :: SCMRING4:37
theorem Th62: :: SCMRING4:38
theorem Th63: :: SCMRING4:39
theorem Th64: :: SCMRING4:40
theorem Th65: :: SCMRING4:41
theorem :: SCMRING4:42