:: On the Decomposition of the States of SCM
:: by Yasushi Tanaka
::
:: Received November 23, 1993
:: Copyright (c) 1993-2017 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, AMI_3, SUBSET_1, AMI_2, AMI_1, STRUCT_0, XBOOLE_0,
FSM_1, RELAT_1, FUNCT_1, TARSKI, FINSET_1, CARD_1, XXREAL_0, FINSEQ_1,
GRAPHSP, ARYTM_3, ARYTM_1, INT_1, FUNCT_4, FUNCOP_1, CIRCUIT2, PARTFUN1,
EXTPRO_1, RECDEF_2, CAT_1, AMISTD_5, COMPOS_1, NAT_1;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1, XCMPLX_0,
DOMAIN_1, RELAT_1, FUNCT_1, FUNCOP_1, PARTFUN1, FUNCT_4, NUMBERS, INT_1,
NAT_1, RECDEF_2, STRUCT_0, FINSET_1, FINSEQ_1, MEMSTR_0, COMPOS_0,
SCM_INST, COMPOS_1, EXTPRO_1, AMI_3, XXREAL_0, AMISTD_5;
constructors DOMAIN_1, FINSEQ_4, AMI_3, PRE_POLY, AMISTD_5, FUNCT_7, RELSET_1;
registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, INT_1,
AMI_3, FINSET_1, CARD_1, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1, MEMSTR_0,
COMPOS_0, XTUPLE_0, FACIRC_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
begin
reserve x,y for set;
theorem :: AMI_5:1
for dl being Data-Location ex i being Nat st dl = dl.i;
theorem :: AMI_5:2
for dl being Data-Location holds dl <> IC SCM;
theorem :: AMI_5:3
for il being Nat, dl being Data-Location
holds il <> dl;
reserve i, j, k for Nat;
theorem :: AMI_5:4
for s being State of SCM, d being Data-Location
holds d in dom s;
registration
cluster Data-Locations SCM -> infinite;
end;
reserve I,J,K for Element of Segm 9,
a,a1 for Nat,
b,b1,c for Element of Data-Locations SCM;
theorem :: AMI_5:5
for l being Instruction of SCM holds InsCode(l) <= 8;
reserve a, b for Data-Location,
loc for Nat;
reserve I,J,K for Element of Segm 9,
a,a1 for Nat,
b,b1,c for Element of Data-Locations SCM,
da,db for Data-Location;
::$CT
theorem :: AMI_5:7
for ins being Instruction of SCM st InsCode ins = 0 holds ins = halt SCM;
theorem :: AMI_5:8
for ins being Instruction of SCM st InsCode ins = 1 holds ex da,
db st ins = da:=db;
theorem :: AMI_5:9
for ins being Instruction of SCM st InsCode ins = 2 holds ex da,
db st ins = AddTo(da,db);
theorem :: AMI_5:10
for ins being Instruction of SCM st InsCode ins = 3 holds ex da,
db st ins = SubFrom(da,db);
theorem :: AMI_5:11
for ins being Instruction of SCM st InsCode ins = 4 holds ex da,
db st ins = MultBy(da,db);
theorem :: AMI_5:12
for ins being Instruction of SCM st InsCode ins = 5 holds ex da,
db st ins = Divide(da,db);
theorem :: AMI_5:13
for ins being Instruction of SCM st InsCode ins = 6 holds ex loc
st ins = SCM-goto loc;
theorem :: AMI_5:14
for ins being Instruction of SCM st InsCode ins = 7 holds ex loc
,da st ins = da=0_goto loc;
theorem :: AMI_5:15
for ins being Instruction of SCM st InsCode ins = 8 holds ex loc
,da st ins = da>0_goto loc;
begin :: Finite partial states of SCM
theorem :: AMI_5:16
for s being State of SCM, iloc being Nat, a
being Data-Location holds s.a = (s +* Start-At(iloc,SCM)).a;
begin :: Autonomic finite partial states of SCM
registration
cluster SCM -> IC-recognized;
end;
registration
cluster SCM -> CurIns-recognized;
end;
theorem :: AMI_5:17
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM,
s1, s2 being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db being Data-Location,
I being Instruction of SCM
st I = CurInstr(P1,Comput(P1,s1,i))
holds I = da := db & da in dom p implies
Comput(P1,s1,i).db = Comput(P2,s2,i).db;
theorem :: AMI_5:18
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM st
I = CurInstr(P1,Comput(P1,
s1,i))
holds I = AddTo(da, db) & da in dom p implies Comput(P1,s1,i).da
+
Comput(P1,s1,i).db = Comput(P2,s2,i).da + Comput(
P2,s2,i).db;
theorem :: AMI_5:19
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM st
I = CurInstr(P1,Comput(P1,
s1,i))
holds I = SubFrom(da, db) & da in dom p implies Comput(P1,s1,i).
da -
Comput(P1,s1,i).db = Comput(P2,s2,i).da - Comput(
P2,s2,i).db;
theorem :: AMI_5:20
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM
st I = CurInstr(P1,Comput(P1,s1,i))
holds I = MultBy(da, db) & da in dom p implies Comput(P1,s1,i).
da *
Comput(P1,s1,i).db = Comput(P2,s2,i).da * Comput(P2,s2,i).db;
theorem :: AMI_5:21
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM
st I = CurInstr(P1,Comput(P1,s1,i))
holds I = Divide(da, db) & da in dom p & da <> db implies
Comput(P1,s1
,i).da div Comput(P1,s1,i).db = Comput(P2,s2,i).da
div Comput(P2,s2,i).db;
theorem :: AMI_5:22
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM st
I = CurInstr(P1,Comput(P1,s1,i))
holds I = Divide(da, db) & db in dom p implies Comput(P1,s1,i).
da mod
Comput(P1,s1,i).db = Comput(P2,s2,i).da mod Comput(P2,s2,i).db;
theorem :: AMI_5:23
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da being
Data-Location, loc being Nat, I being Instruction of
SCM st I = CurInstr(P1,Comput(P1,s1,i))
holds I = da=0_goto loc & loc <> (IC Comput(P1,s1,i)) + 1
implies ( Comput(P1,s1,i).da = 0 iff Comput(P2,s2,i)
.da = 0);
theorem :: AMI_5:24
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da being
Data-Location, loc being Nat, I being Instruction of
SCM st I = CurInstr(P1,Comput(P1,s1,i))
holds I = da>0_goto loc & loc <> (IC Comput(P1,s1,i)) + 1
implies ( Comput(P1,s1,i).da > 0 iff Comput(P2,s2,i)
.da > 0);
theorem :: AMI_5:25
for s1,s2 being State of SCM st IC(s1) = IC(s2) &
(for a being Data-Location holds s1.a = s2.a)
holds s1 = s2;