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


theorem Th1: :: SCMRING4:1
for n being Nat
for R being non trivial Ring holds dl. (R,n) = [1,n]
proof end;

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

theorem :: SCMRING4:3
for R being non trivial Ring
for i, j being Nat st i <> j holds
dl. (R,i) <> dl. (R,j)
proof end;

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

theorem Th5: :: SCMRING4:5
for R being non trivial Ring
for a being Data-Location of R
for loc being Nat
for s being State of (SCM R) holds s . a = (s +* (Start-At (loc,(SCM R)))) . a
proof end;

theorem Th6: :: SCMRING4:6
for R being non trivial 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
s1 = s2
proof end;

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

definition
let R be non trivial 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 Ring;
cluster SCM R -> IC-recognized ;
coherence
SCM R is IC-recognized
proof end;
end;

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

theorem Th7: :: SCMRING4:7
for n being 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 & p c= s2 & q c= P1 & q 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 Th8: :: SCMRING4:8
for n being 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 & p c= s2 & q c= P1 & q 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 Th9: :: SCMRING4:9
for n being 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 & p c= s2 & q c= P1 & q 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 Th10: :: SCMRING4:10
for n being 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 & p c= s2 & q c= P1 & q 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 Th11: :: SCMRING4:11
for n being Nat
for R being non trivial Ring
for a being Data-Location of R
for loc being 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 & p c= s2 & q c= P1 & q c= P2 & CurInstr (P1,(Comput (P1,s1,n))) = a =0_goto loc & loc <> (IC (Comput (P1,s1,n))) + 1 holds
( (Comput (P1,s1,n)) . a = 0. R iff (Comput (P2,s2,n)) . a = 0. R )
proof end;

theorem Th12: :: SCMRING4:12
for k being 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 & IncIC (p,k) c= s2 holds
for P1, P2 being Instruction-Sequence of (SCM R) st q c= P1 & Reloc (q,k) c= P2 holds
for i being 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 Ring;
cluster SCM R -> relocable1 relocable2 ;
coherence
( SCM R is relocable1 & SCM R is relocable2 ) by Th12;
end;