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

begin

Lm1: for a, A being set st A /\ {a} <> {} holds
a in A

proof end;

begin

theorem Th1: :: SCMRING4:1

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

proof end;

theorem :: SCMRING4:2

for R being good Ring
for loc being Element of NAT holds the Object-Kind of (SCM R) . 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

canceled;

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 Element of NAT holds a <> loc

proof end;

theorem :: SCMRING4:8

for R being good Ring
for s being State of (SCM R) holds Data-Locations SCM 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) = Data-Locations SCM

proof end;

theorem :: SCMRING4:10

canceled;

theorem :: SCMRING4:11

canceled;

theorem :: SCMRING4:12

canceled;

theorem Th13: :: SCMRING4:13

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

proof end;

theorem :: SCMRING4:14

canceled;

theorem :: SCMRING4:15

canceled;

theorem :: SCMRING4:16

canceled;

theorem :: SCMRING4:17

canceled;

theorem :: SCMRING4:18

canceled;

theorem :: SCMRING4:19

canceled;

theorem :: SCMRING4:20

canceled;

theorem :: SCMRING4:21

canceled;

theorem Th20: :: SCMRING4:22

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

proof end;

theorem Th21: :: SCMRING4:23

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 Element of NAT holds s1 . i = s2 . i ) holds
s1 = s2

proof end;

theorem Th22: :: SCMRING4:24

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

proof end;

theorem Th23: :: SCMRING4:25

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

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

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

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

proof end;

theorem :: SCMRING4:28

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

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 st p c= s holds
IC (Comput ((ProgramPart s),s,n)) in dom (ProgramPart p)

proof end;

theorem Th28: :: SCMRING4:30

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 st p c= s1 & p c= s2 holds
( IC (Comput ((ProgramPart s1),s1,n)) = IC (Comput ((ProgramPart s2),s2,n)) & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,n))),(Comput ((ProgramPart s2),s2,n))) )

proof end;

theorem Th29: :: 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 st p c= s1 & p c= s2 & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = a := b & a in dom p holds
(Comput ((ProgramPart s1),s1,n)) . b = (Comput ((ProgramPart s2),s2,n)) . b

proof end;

theorem Th30: :: 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 st p c= s1 & p c= s2 & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = AddTo (a,b) & a in dom p holds
((Comput ((ProgramPart s1),s1,n)) . a) + ((Comput ((ProgramPart s1),s1,n)) . b) = ((Comput ((ProgramPart s2),s2,n)) . a) + ((Comput ((ProgramPart s2),s2,n)) . b)

proof end;

theorem Th31: :: SCMRING4:33

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 st p c= s1 & p c= s2 & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = SubFrom (a,b) & a in dom p holds
((Comput ((ProgramPart s1),s1,n)) . a) - ((Comput ((ProgramPart s1),s1,n)) . b) = ((Comput ((ProgramPart s2),s2,n)) . a) - ((Comput ((ProgramPart s2),s2,n)) . b)

proof end;

theorem Th32: :: SCMRING4:34

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 st p c= s1 & p c= s2 & CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,n))),(Comput ((ProgramPart s1),s1,n))) = MultBy (a,b) & a in dom p holds
((Comput ((ProgramPart s1),s1,n)) . a) * ((Comput ((ProgramPart s1),s1,n)) . b) = ((Comput ((ProgramPart s2),s2,n)) . a) * ((Comput ((ProgramPart s2),s2,n)) . b)

proof end;

theorem Th33: :: SCMRING4:35

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

proof end;

begin

theorem Th34: :: SCMRING4:36

for k being Element of NAT
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:37

for k being Element of NAT
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 (Comput ((ProgramPart s1),s1,i))) + k = IC (Comput ((ProgramPart s2),s2,i)) & IncAddr ((CurInstr ((ProgramPart (Comput ((ProgramPart s1),s1,i))),(Comput ((ProgramPart s1),s1,i)))),k) = CurInstr ((ProgramPart (Comput ((ProgramPart s2),s2,i))),(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 s),s,i)) = DataPart (Comput ((ProgramPart s2),s2,i)) )

proof end;

theorem Th36: :: SCMRING4:38

for k being Element of NAT
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:39

for k 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 autonomic FinPartState of (SCM R) st IC (SCM R) in dom p & 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 R)))) +* (ProgramPart (Relocated (p,k)))

proof end;

theorem Th38: :: SCMRING4:40

for k 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 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 Comput ((ProgramPart s),s,i) = (((Comput ((ProgramPart (s +* p)),(s +* p),i)) +* (Start-At (((IC (Comput ((ProgramPart (s +* p)),(s +* p),i))) + k),(SCM R)))) +* (s | (dom (ProgramPart p)))) +* (ProgramPart (Relocated (p,k)))

proof end;

theorem Th39: :: SCMRING4:41

for k being Element of NAT
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 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 R)))) +* (s | (dom (ProgramPart (Relocated (p,k)))))) +* (ProgramPart p)

proof end;

theorem Th40: :: SCMRING4:42

for k being Element of NAT
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;

registration

let R be non trivial good Ring;
let l be Element of NAT ;
let p be l -started autonomic halting FinPartState of (SCM R);
let k be Element of NAT ;
cluster Relocated (p,k) -> halting ;
coherence
Relocated (p,k) is halting

proof end;

end;

theorem Th41: :: SCMRING4:43

for k being Element of NAT
for R being non trivial good Ring
for l being Element of NAT
for p being b₃ -started non program-free autonomic halting FinPartState of (SCM R) st IC (SCM R) in dom p holds
DataPart (Result ((ProgramPart p),p)) = DataPart (Result ((ProgramPart (Relocated (p,k))),(Relocated (p,k))))

proof end;

theorem :: SCMRING4:44

for k being Element of NAT
for R being non trivial good Ring
for l being Element of NAT
for p being b₃ -started non program-free autonomic halting FinPartState of (SCM R)
for F being PartFunc of (FinPartSt (SCM R)),(FinPartSt (SCM R)) st IC (SCM R) in dom p & F is data-only holds
( ProgramPart p,p computes F iff ProgramPart (Relocated (p,k)), Relocated (p,k) computes F )

proof end;