:: Relocability for { \bf SCM } over Ring
:: by Artur Korni{\l}owicz and Yasunari Shidama
::
:: Received February 6, 2004
:: Copyright (c) 2004-2011 Association of Mizar Users

begin

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

proof end;

begin

theorem :: SCMRING4:1

for R being non trivial good Ring
for loc being Element of NAT holds the Object-Kind of (SCM R) . loc = SCM-Instr R

proof end;

theorem Th2: :: SCMRING4:2

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

proof end;

theorem :: SCMRING4:3

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

proof end;

theorem :: SCMRING4:4

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

proof end;

theorem Th5: :: SCMRING4:5

for R being non trivial good Ring
for a being Data-Location of R
for loc being Element of NAT holds a <> loc

proof end;

theorem :: SCMRING4:6

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

proof end;

theorem Th7: :: SCMRING4:7

for R being non trivial 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 Th8: :: SCMRING4:8

for R being non trivial 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 ) holds
NPP s1 = NPP s2

proof end;

registration

let R be non trivial good Ring;
cluster SCM R -> relocable ;
coherence
SCM R is relocable

proof end;

end;

definition

let R be non trivial 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;

registration

let R be non trivial good Ring;
cluster SCM R -> IC-recognized ;
coherence
SCM R is IC-recognized

proof end;

end;

registration

let R be non trivial good Ring;
cluster SCM R -> CurIns-recognized ;
coherence
SCM R is CurIns-recognized

proof end;

end;

Lm2: for R being non trivial good Ring
for a being Data-Location of R
for p being PartState of (SCM R) st a in dom p holds
a in dom (NPP p)

proof end;

theorem Th9: :: SCMRING4:9

for n being Element of NAT
for R being non trivial good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R)
for P1, P2 being the Instructions of (SCM b₂) -valued ManySortedSet of NAT st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a := b & a in dom p holds
(Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b

proof end;

theorem Th10: :: SCMRING4:10

for n being Element of NAT
for R being non trivial good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R)
for P1, P2 being the Instructions of (SCM b₂) -valued ManySortedSet of NAT st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) & a in dom p holds
((Comput (P1,s1,n)) . a) + ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) + ((Comput (P2,s2,n)) . b)

proof end;

theorem Th11: :: SCMRING4:11

for n being Element of NAT
for R being non trivial good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R)
for P1, P2 being the Instructions of (SCM b₂) -valued ManySortedSet of NAT st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) & a in dom p holds
((Comput (P1,s1,n)) . a) - ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) - ((Comput (P2,s2,n)) . b)

proof end;

theorem Th12: :: SCMRING4:12

for n being Element of NAT
for R being non trivial good Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R)
for P1, P2 being the Instructions of (SCM b₂) -valued ManySortedSet of NAT st not R is trivial holds
for p being non NAT -defined autonomic FinPartState of st NPP p c= s1 & NPP p c= s2 & ProgramPart p c= P1 & ProgramPart p c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) & a in dom p holds
((Comput (P1,s1,n)) . a) * ((Comput (P1,s1,n)) . b) = ((Comput (P2,s2,n)) . a) * ((Comput (P2,s2,n)) . b)

proof end;

theorem Th13: :: SCMRING4:13

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

proof end;

begin

theorem Th14: :: SCMRING4:14

for k being Element of NAT
for R being non trivial good Ring
for s1, s2 being State of (SCM R)
for p being autonomic FinPartState of (SCM R) st IC in dom p & NPP p c= s1 & NPP (Relocated (p,k)) c= s2 holds
for P1, P2 being the Instructions of (SCM b₂) -valued ManySortedSet of NAT st ProgramPart p c= P1 & Reloc ((ProgramPart p),k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) & IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) & (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) & DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )

proof end;

registration

let R be non trivial good Ring;
cluster SCM R -> relocable1 relocable2 ;
coherence
( SCM R is relocable1 & SCM R is relocable2 )

proof end;

end;