:: 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

proof end;

theorem Th1: :: SCMRING4:1

for R being good Ring holds the carrier of (SCM R) = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT

proof end;

theorem :: SCMRING4:2

for R being good Ring
for loc being Instruction-Location of SCM R holds ObjectKind loc = SCM-Instr R

proof end;

theorem Th3: :: SCMRING4:3

for n being Element of NAT
for R being good Ring holds dl. R,n = [1,n]

proof end;

theorem :: SCMRING4:4

for k being natural number
for R being good Ring holds il. (SCM R),k = k

proof end;

theorem :: SCMRING4:5

for R being good Ring
for dl being Data-Location of R ex i being Element of NAT st dl = dl. R,i

proof end;

theorem :: SCMRING4:6

for R being good Ring
for i, j being Element of NAT st i <> j holds
dl. R,i <> dl. R,j

proof end;

theorem Th7: :: SCMRING4:7

for R being good Ring
for a being Data-Location of R
for loc being Instruction-Location of SCM R holds a <> loc

proof end;

Lm2: now

let R be good Ring; :: thesis: the carrier of SCM = the carrier of (SCM R)
thus the carrier of SCM = ({(IC (SCM R))} \/ SCM-Data-Loc ) \/ NAT by SCMRING2:9
.= the carrier of (SCM R) by Th1 ; :: thesis: verum

end;

theorem :: SCMRING4:8

for R being good Ring
for s being State of (SCM R) holds SCM-Data-Loc c= dom s

proof end;

theorem Th9: :: SCMRING4:9

for R being good Ring
for s being State of (SCM R) holds dom (DataPart s) = SCM-Data-Loc

proof end;

theorem :: SCMRING4:10

for R being good Ring
for p being FinPartState of (SCM R)
for q being FinPartState of SCM st p = q holds
DataPart p = DataPart q

proof end;

theorem :: SCMRING4:11

canceled;

theorem :: SCMRING4:12

for R being good Ring
for p being FinPartState of (SCM R) holds
( p is data-only iff dom p c= SCM-Data-Loc )

proof end;

theorem Th13: :: SCMRING4:13

for R being good Ring
for p being FinPartState of (SCM R) holds dom (DataPart p) c= SCM-Data-Loc

proof end;

theorem :: SCMRING4:14

for R being good Ring
for s being State of (SCM R) holds NAT c= dom s

proof end;

theorem :: SCMRING4:15

for R being good Ring
for p being FinPartState of (SCM R)
for q being FinPartState of SCM st p = q holds
ProgramPart p = ProgramPart q ;

theorem :: SCMRING4:16

for R being good Ring
for p being FinPartState of (SCM R) holds dom (ProgramPart p) c= NAT by RELAT_1:87;

theorem :: SCMRING4:17

canceled;

theorem :: SCMRING4:18

for k being natural number
for R being good Ring
for loc being Instruction-Location of SCM R holds IncAddr (goto loc),k = goto (loc + k) by SCMRING3:69;

theorem :: SCMRING4:19

for k being natural number
for R being good Ring
for a being Data-Location of R
for loc being Instruction-Location of SCM R holds IncAddr (a =0_goto loc),k = a =0_goto (loc + k) by SCMRING3:70;

theorem Th20: :: SCMRING4:20

for R being good Ring
for a being Data-Location of R
for loc being Instruction-Location of SCM R
for s being State of (SCM R) holds s . a = (s +* (Start-At loc)) . a

proof end;

theorem Th21: :: SCMRING4:21

for R being good Ring
for s1, s2 being State of (SCM R) st IC s1 = IC s2 & ( for a being Data-Location of R holds s1 . a = s2 . a ) & ( for i being Instruction-Location of SCM R holds s1 . i = s2 . i ) holds
s1 = s2

proof end;

theorem Th22: :: SCMRING4:22

for k being natural number
for R being good Ring
for s being State of (SCM R) holds Exec (IncAddr (CurInstr s),k),(s +* (Start-At ((IC s) + k))) = (Following s) +* (Start-At ((IC (Following s)) + k))

proof end;

theorem Th23: :: SCMRING4:23

for j, k being natural number
for R being good Ring
for I being Instruction of (SCM R)
for s being State of (SCM R) st IC s = il. (SCM R),(j + k) holds
Exec I,(s +* (Start-At ((IC s) -' k))) = (Exec (IncAddr I,k),s) +* (Start-At ((IC (Exec (IncAddr I,k),s)) -' k))

proof end;

registration

let R be good Ring;
cluster non NAT -defined autonomic Element of sproduct the Object-Kind of (SCM R);
existence
ex b₁ being FinPartState of (SCM R) st
( b₁ is autonomic & not b₁ is NAT -defined )

proof end;

end;

definition

let R be good Ring;
let a be Data-Location of R;
let r be Element of R;
:: original: .-->
redefine func a .--> r -> FinPartState of (SCM R);
coherence
a .--> r is FinPartState of (SCM R)

proof end;

end;

theorem Th24: :: SCMRING4:24

for R being good Ring st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st DataPart p <> {} holds
IC (SCM R) in dom p

proof end;

theorem Th25: :: SCMRING4:25

for R being good Ring st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of (SCM R) holds IC (SCM R) in dom p

proof end;

theorem :: SCMRING4:26

for R being good Ring
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p holds
IC p in dom p

proof end;

theorem Th27: :: SCMRING4:27

for n being Element of NAT
for R being good Ring
for s being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of (SCM R) st p c= s holds
IC (Computation s,n) in dom (ProgramPart p)

proof end;

theorem Th28: :: SCMRING4:28

for n being Element of NAT
for R being good Ring
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 holds
( IC (Computation s1,n) = IC (Computation s2,n) & CurInstr (Computation s1,n) = CurInstr (Computation s2,n) )

proof end;

theorem Th29: :: SCMRING4:29

for n being Element of NAT
for R being good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & CurInstr (Computation s1,n) = a := b & a in dom p holds
(Computation s1,n) . b = (Computation s2,n) . b

proof end;

theorem Th30: :: SCMRING4:30

for n being Element of NAT
for R being good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & CurInstr (Computation s1,n) = AddTo a,b & a in dom p holds
((Computation s1,n) . a) + ((Computation s1,n) . b) = ((Computation s2,n) . a) + ((Computation s2,n) . b)

proof end;

theorem Th31: :: SCMRING4:31

for n being Element of NAT
for R being good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & CurInstr (Computation s1,n) = SubFrom a,b & a in dom p holds
((Computation s1,n) . a) - ((Computation s1,n) . b) = ((Computation s2,n) . a) - ((Computation s2,n) . b)

proof end;

theorem Th32: :: SCMRING4:32

for n being Element of NAT
for R being good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & CurInstr (Computation s1,n) = MultBy a,b & a in dom p holds
((Computation s1,n) . a) * ((Computation s1,n) . b) = ((Computation s2,n) . a) * ((Computation s2,n) . b)

proof end;

theorem Th33: :: SCMRING4:33

for n being Element of NAT
for R being good Ring
for a being Data-Location of R
for loc being Instruction-Location of SCM R
for s1, s2 being State of (SCM R) st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of (SCM R) st p c= s1 & p c= s2 & CurInstr (Computation s1,n) = a =0_goto loc & loc <> Next (IC (Computation s1,n)) holds
( (Computation s1,n) . a = 0. R iff (Computation s2,n) . a = 0. R )

proof end;

theorem Th34: :: SCMRING4:34

for k being natural number
for R being good Ring
for s1, s2 being State of (SCM R)
for p being autonomic FinPartState of (SCM R) st p c= s1 & Relocated p,k c= s2 holds
p c= s1 +* (DataPart s2)

proof end;

theorem Th35: :: 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) )

proof end;

theorem Th36: :: SCMRING4:36

for k being natural number
for R being good Ring st not R is trivial holds
for p being autonomic FinPartState of (SCM R) st IC (SCM R) in dom p holds
( p is halting iff Relocated p,k is halting )

proof end;

theorem :: SCMRING4:37

for k being natural number
for R being good Ring
for 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= s holds
for i being Element of NAT holds Computation (s +* (Relocated p,k)),i = ((Computation s,i) +* (Start-At ((IC (Computation s,i)) + k))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th38: :: SCMRING4:38

for k being natural number
for R being good Ring
for 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 & Relocated p,k c= s holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* p),i) +* (Start-At ((IC (Computation (s +* p),i)) + k))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated p,k))

proof end;

theorem Th39: :: SCMRING4:39

for k being natural number
for R being good Ring
for p being FinPartState of (SCM R)
for s being State of (SCM R) st not R is trivial & IC (SCM R) in dom p & p c= s & Relocated p,k is autonomic holds
for i being Element of NAT holds Computation s,i = (((Computation (s +* (Relocated p,k)),i) +* (Start-At ((IC (Computation (s +* (Relocated p,k)),i)) -' k))) +* (s | (dom (ProgramPart (Relocated p,k))))) +* (ProgramPart p)

proof end;

theorem Th40: :: SCMRING4:40

for k being natural number
for R being good Ring
for p being FinPartState of (SCM R) st not R is trivial & IC (SCM R) in dom p holds
( p is autonomic iff Relocated p,k is autonomic )

proof end;

theorem Th41: :: SCMRING4:41

for k being natural number
for R being good Ring st not R is trivial holds
for p being autonomic halting FinPartState of (SCM R) st IC (SCM R) in dom p holds
DataPart (Result p) = DataPart (Result (Relocated p,k))

proof end;

theorem :: SCMRING4:42

for k being natural number
for R being good Ring
for p being FinPartState of (SCM R) st not R is trivial holds
for F being PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)) st IC (SCM R) in dom p & F is data-only holds
( p computes F iff Relocated p,k computes F )

proof end;