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


begin

theorem Th1: :: SCMRING4:1
for n being Element of NAT
for R being non trivial Ring holds dl. (R,n) = [1,n]
proofend;

theorem :: SCMRING4:2
for R being non trivial Ring
for dl being Data-Location of R ex i being Element of NAT st dl = dl. (R,i)
proofend;

theorem :: SCMRING4:3
for R being non trivial Ring
for i, j being Element of NAT st i <> j holds
dl. (R,i) <> dl. (R,j)
proofend;

theorem :: SCMRING4:4
for R being non trivial Ring
for s being State of (SCM R) holds Data-Locations c= dom s
proofend;

theorem Th5: :: SCMRING4:5
for R being non trivial 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
proofend;

theorem Th6: :: SCMRING4:6
for R being non trivial Ring
for s1, s2 being State of (SCM R) st IC s1 = IC s2 &amp; ( for a being Data-Location of R holds s1 . a = s2 . a ) holds
s1 = s2
proofend;

registration
let R be non trivial Ring;
cluster SCM R ->  relocable ;
coherence
 SCM R is relocable
proofend;
end;

definition
let R be non trivial Ring;
let a be Data-Location of R;
let r be Element of R;
:: original:.-->
redefine funca .--> r ->  FinPartState of (SCM R);
coherence
 a .--> r is FinPartState of (SCM R)
proofend;
end;

registration
let R be non trivial Ring;
cluster SCM R ->  IC-recognized ;
coherence
 SCM R is IC-recognized
proofend;
end;

registration
let R be non trivial Ring;
cluster SCM R ->  CurIns-recognized ;
coherence
 SCM R is CurIns-recognized
proofend;
end;

theorem Th7: :: SCMRING4:7
for n being Element of NAT
for R being non trivial Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R)
for P1, P2 being Instruction-Sequence of (SCM R)
for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function
for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 &amp; CurInstr (P1,(Comput (P1,s1,n))) = a := b &amp; a in dom p holds
(Comput (P1,s1,n)) . b = (Comput (P2,s2,n)) . b
proofend;

theorem Th8: :: SCMRING4:8
for n being Element of NAT
for R being non trivial Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R)
for P1, P2 being Instruction-Sequence of (SCM R)
for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function
for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 &amp; CurInstr (P1,(Comput (P1,s1,n))) = AddTo (a,b) &amp; 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)
proofend;

theorem Th9: :: SCMRING4:9
for n being Element of NAT
for R being non trivial Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R)
for P1, P2 being Instruction-Sequence of (SCM R)
for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function
for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 &amp; CurInstr (P1,(Comput (P1,s1,n))) = SubFrom (a,b) &amp; 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)
proofend;

theorem Th10: :: SCMRING4:10
for n being Element of NAT
for R being non trivial Ring
for a, b being Data-Location of R
for s1, s2 being State of (SCM R)
for P1, P2 being Instruction-Sequence of (SCM R)
for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function
for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 &amp; CurInstr (P1,(Comput (P1,s1,n))) = MultBy (a,b) &amp; 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)
proofend;

theorem Th11: :: SCMRING4:11
for n being Element of NAT
for R being non trivial 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 Instruction-Sequence of (SCM R)
for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function
for p being non empty b9 -autonomic FinPartState of (SCM R) st p c= s1 &amp; p c= s2 &amp; q c= P1 &amp; q c= P2 &amp; CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc &amp; loc <> succ (IC (Comput (P1,s1,n))) holds
( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R )
proofend;

begin

theorem Th12: :: SCMRING4:12
for k being Element of NAT
for R being non trivial Ring
for s1, s2 being State of (SCM R)
for q being NAT -defined the InstructionsF of (SCM b2) -valued finite non halt-free Function
for p being non empty b5 -autonomic FinPartState of (SCM R) st p c= s1 &amp; IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 &amp; Reloc (q,k) c= P2 holds
for i being Element of NAT holds
( (IC (Comput (P1,s1,i))) + k = IC (Comput (P2,s2,i)) &amp; IncAddr ((CurInstr (P1,(Comput (P1,s1,i)))),k) = CurInstr (P2,(Comput (P2,s2,i))) &amp; (Comput (P1,s1,i)) | (dom (DataPart p)) = (Comput (P2,s2,i)) | (dom (DataPart p)) &amp; DataPart (Comput (P1,(s1 +* (DataPart s2)),i)) = DataPart (Comput (P2,s2,i)) )
proofend;

registration
let R be non trivial Ring;
cluster SCM R ->  relocable1 relocable2 ;
coherence
 ( SCM R is relocable1 &amp; SCM R is relocable2 )
proofend;
end;