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

environ

vocabularies HIDDEN, SUBSET_1, NUMBERS, XBOOLE_0, SETFAM_1, FUNCSDOM, AMI_3, AMI_1, FSM_1, STRUCT_0, AMI_2, FUNCT_1, TARSKI, RELAT_1, AMISTD_2, ARYTM_3, FUNCT_4, CIRCUIT2, CARD_1, GRAPHSP, ARYTM_1, SUPINF_2, FUNCOP_1, ZFMISC_1, PARTFUN1, RELOC, NAT_1, AMISTD_5, COMPOS_1, FINSET_1, GOBRD13, MEMSTR_0, EXTPRO_1;
notations HIDDEN, TARSKI, XBOOLE_0, SUBSET_1, SETFAM_1, DOMAIN_1, ORDINAL1, RELAT_1, FINSET_1, NUMBERS, FUNCT_1, PARTFUN1, STRUCT_0, ALGSTR_0, VECTSP_1, FUNCOP_1, XCMPLX_0, NAT_1, FUNCT_4, FUNCT_7, NAT_D, VALUED_1, PBOOLE, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, AMI_3, SCMRING1, SCMRING2, SCMRING3, AMISTD_2, AMISTD_5;
definitions FUNCT_1, EXTPRO_1, AMISTD_5;
theorems TARSKI, SCMRING2, AMI_3, FUNCT_4, FUNCT_1, ZFMISC_1, FUNCOP_1, SCMRING1, AMI_2, STRUCT_0, XBOOLE_0, XBOOLE_1, RELAT_1, GRFUNC_1, SCMRING3, AMISTD_2, PBOOLE, PARTFUN1, ORDINAL1, COMPOS_1, EXTPRO_1, AMISTD_5, MEMSTR_0, COMPOS_0, XTUPLE_0;
schemes NAT_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, FUNCOP_1, XREAL_0, NAT_1, CARD_3, STRUCT_0, AMI_3, SCMRING2, AMISTD_2, SCMRING3, FINSET_1, ORDINAL1, FUNCT_4, COMPOS_1, EXTPRO_1, AMI_5, MEMSTR_0, INT_3, COMPOS_0;
constructors HIDDEN, XXREAL_0, REALSET2, AMI_3, AMISTD_2, SCMRING3, PRE_POLY, NAT_D, AMISTD_1, AMISTD_5, PBOOLE, INT_3, FUNCT_7, RELSET_1, MEMSTR_0, SCMRING1;
requirements HIDDEN, NUMERALS, BOOLE, SUBSET, ARITHM, REAL;
equalities EXTPRO_1, FUNCOP_1, AMI_3, NAT_1, STRUCT_0, MEMSTR_0;
expansions AMISTD_5;


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;