:: A Mathematical Model of CPU
:: by Yatsuka Nakamura and Andrzej Trybulec
::
:: Received October 14, 1992
:: Copyright (c) 1992-2011 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 STRUCT_0, SUBSET_1, XBOOLE_0, FUNCT_1, NUMBERS, CARD_3, ORDINAL1,
CARD_1, FUNCOP_1, FUNCT_4, RELAT_1, TARSKI, CAT_1, FSM_1, SETFAM_1,
GLIB_000, FINSET_1, CIRCUIT2, NAT_1, ARYTM_3, XXREAL_0, MSUALG_1,
TURING_1, PARTFUN1, MCART_1, ZFMISC_1, GRAPHSP, ARYTM_1, FUNCT_7, AMI_1,
PBOOLE, SCMNORM, GROUP_9, RECDEF_2, COMPOS_1, AMISTD_1, GOBOARD5,
AMISTD_2, CARD_5, UNIALG_1, AMI_2, AMI_3, FINSEQ_1, INT_1, SCMPDS_2,
SCMPDS_1, COMPLEX1, FINSEQ_2;
notations TARSKI, XBOOLE_0, ZFMISC_1, MCART_1, SUBSET_1, SETFAM_1, ORDINAL1,
PBOOLE, CARD_1, XXREAL_0, XCMPLX_0, INT_1, NAT_1, NAT_D, NUMBERS,
FUNCT_7, CARD_3, RELAT_1, FUNCT_1, PARTFUN1, INT_2,
FINSET_1, FUNCOP_1, FUNCT_4, FINSEQ_1, FINSEQ_2, FINSEQ_4,
FUNCT_2, DOMAIN_1,
RECDEF_2, STRUCT_0, COMPOS_1, EXTPRO_1, AMISTD_1,
AMISTD_2, AMI_2, AMI_3, SCMPDS_1, SCMPDS_2;
constructors SETFAM_1, DOMAIN_1, FUNCT_4, XXREAL_0, FUNCT_7, GRAPH_2,
RELSET_1, PRE_POLY, PBOOLE, RECDEF_2, COMPOS_1, EXTPRO_1, AMISTD_1,
AMISTD_2, AMI_2, AMI_3, NAT_D, FINSEQ_4, CAT_2, INT_1, SCMPDS_1,
SCMPDS_2;
registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, FUNCT_2,
FUNCOP_1, FUNCT_4, FINSET_1, XREAL_0, FINSEQ_1, CARD_3, STRUCT_0, INT_1,
RELSET_1, GRFUNC_1, PRE_POLY, PBOOLE, COMPOS_1, EXTPRO_1, AMISTD_1,
AMISTD_2, AMI_2, AMI_3, SCMPDS_1, SCMPDS_2;
registrations NUMBERS, XXREAL_0;
requirements NUMERALS, BOOLE, SUBSET, ARITHM;
definitions TARSKI, STRUCT_0, FUNCOP_1, ORDINAL1, RELAT_1, PBOOLE, FUNCT_1,
PARTFUN1, MCART_1, ZFMISC_1, COMPOS_1, EXTPRO_1, AMISTD_2,
AMI_2, AMI_3, SCMPDS_1, SCMPDS_2;
theorems ZFMISC_1, FUNCT_2, TARSKI, NAT_1, CQC_LANG, CARD_3, FINSEQ_1,
FUNCT_4, FUNCOP_1, FINSET_1, FUNCT_1, GRFUNC_1, RELAT_1, RELSET_1,
XBOOLE_0, XBOOLE_1, ORDINAL1, MCART_1, ENUMSET1, SUBSET_1, XXREAL_0,
FUNCT_7, INT_1, PARTFUN1, PBOOLE, RECDEF_2, FUNCT_5, COMPOS_1, EXTPRO_1,
AMISTD_1, AMISTD_2, AMI_3, AMI_2, SCMPDS_1, SCMPDS_2;
schemes NAT_1, FRAENKEL;
begin :: General concepts
reserve N for with_non-empty_elements set;
definition
canceled 12;
let N be with_non-empty_elements set;
let IT be non empty AMI-Struct over N;
attr IT is steady-programmed means
:Def13:
for s being State of IT, i being Instruction of IT,
l being Element of NAT
holds Exec(i,s).l = s.l;
end;
registration
let N be with_non-empty_elements set;
cluster Trivial-AMI N -> steady-programmed;
coherence
proof
let s be State of Trivial-AMI N, i be Instruction of Trivial-AMI N,
l be Element of NAT;
thus thesis by EXTPRO_1:1;
end;
end;
registration
let N;
cluster IC-Ins-separated halting steady-programmed definite strict (non
empty stored-program AMI-Struct over N);
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
begin :: General theory
reserve x,y,z,A,B for set,
f,g,h for Function,
i,j,k for Element of NAT;
reserve S for IC-Ins-separated definite
(non empty stored-program AMI-Struct over N),
s for State of S;
reserve E for set;
reserve N for non empty with_non-empty_elements set,
S for IC-Ins-separated definite (non empty stored-program AMI-Struct
over N),
s for State of S;
reserve n for Element of NAT;
Lm1: for N being with_non-empty_elements set for S being
steady-programmed (non empty stored-program AMI-Struct over N) for i being
Instruction of S, s being State of S
holds ProgramPart Exec (i, s) = ProgramPart s
proof
let N be with_non-empty_elements set;
let S be steady-programmed (non empty stored-program AMI-Struct over N);
let i be Instruction of S, s be State of S;
A1: NAT c= the carrier of S by COMPOS_1:def 2;
A2: for x being set st x in NAT holds (Exec (i, s) | NAT).x = (s | NAT).x
proof
let x be set;
assume x in NAT;
then reconsider l = x as Element of NAT;
thus (Exec (i, s) | NAT).x = (Exec (i, s)).l by FUNCT_1:72
.= s.l by Def13
.= (s | NAT).x by FUNCT_1:72;
end;
A3: dom ProgramPart s = NAT by COMPOS_1:34;
dom (Exec (i,s)) = the carrier of S by PARTFUN1:def 4;
then dom (Exec (i, s) | NAT) = NAT by A1,RELAT_1:91;
hence thesis by A3,A2,FUNCT_1:9;
end;
Lm2:
for S being steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N)
for P being (the Instructions of S)-valued ManySortedSet of NAT
for s being State of S, n being Nat
holds ProgramPart s = ProgramPart Comput(P,s,n)
proof
let S be steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N);
let P be (the Instructions of S)-valued ManySortedSet of NAT;
let s be State of S;
defpred X[Nat]
means ProgramPart s = ProgramPart Comput(P,s,$1);
A1: now
let n be Nat;
assume X[n];
then ProgramPart s =
ProgramPart Following(P, Comput(P,s,n)) by Lm1
.= ProgramPart Comput(P,s,n+1) by EXTPRO_1:4;
hence X[n+1];
end;
A2: X[ 0] by EXTPRO_1:3;
thus for n being Nat holds X[n] from NAT_1:sch 2(A2,A1);
end;
canceled 53;
theorem Th54:
for S being steady-programmed IC-Ins-separated definite (non
empty stored-program AMI-Struct over N)
for P being (the Instructions of S)-valued ManySortedSet of NAT
for s being State of S, i be
Element of NAT, k holds s.i = Comput(P,s,k).i
proof
let S be steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N);
let P be (the Instructions of S)-valued ManySortedSet of NAT;
let s be State of S, i be Element of NAT;
defpred P[Nat] means s.i = Comput(P,s,$1).i;
A1: now
let k;
assume P[k];
then s.i = (Following(P,Comput(P,s,k))).i by Def13
.= Comput(P,s,k+1).i by EXTPRO_1:4;
hence P[k+1];
end;
A2: P[ 0] by EXTPRO_1:3;
thus for k holds P[k] from NAT_1:sch 1(A2,A1);
end;
registration
let N;
cluster halting steady-programmed realistic strict
(IC-Ins-separated definite (non empty stored-program AMI-Struct over N));
existence
proof
take Trivial-AMI N;
thus thesis;
end;
end;
canceled 26;
theorem Th81:
for S being steady-programmed IC-Ins-separated definite (non
empty stored-program AMI-Struct over N) for p being NAT-defined PartState
of S
for P being (the Instructions of S)-valued ManySortedSet of NAT
for s being State of S st p c= s for k
holds p c= Comput(P,s,k)
proof
let S be steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N);
let p be NAT-defined PartState of S;
let P be (the Instructions of S)-valued ManySortedSet of NAT,
s be State of S such that
A1: p c= s;
let k;
A2: dom p c= NAT by RELAT_1:def 18;
A3: now
let x be set;
assume
A4: x in dom p;
then reconsider l = x as Element of NAT by A2;
s.x = ( Comput(P,s,k)).l by Th54;
hence p.x = ( Comput(P,s,k)).x by A1,A4,GRFUNC_1:8;
end;
dom s = the carrier of S by PARTFUN1:def 4
.= dom( Comput(P,s,k)) by PARTFUN1:def 4;
then dom p c= dom( Comput(P,s,k)) by A1,GRFUNC_1:8;
hence thesis by A3,GRFUNC_1:8;
end;
canceled 4;
theorem
for S being steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N), s being State of S,
P being (the Instructions of S)-valued ManySortedSet of NAT,
p being NAT-defined
PartState of S, k holds p c= s iff p c= Comput(P,s,k)
proof
let S be steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N);
let s be State of S,
P be (the Instructions of S)-valued ManySortedSet of NAT,
p be NAT-defined PartState of S, k;
dom( Comput(P,s,k)) = the carrier of S by PARTFUN1:def 4;
then
A1: dom p c= dom( Comput(P,s,k)) by RELAT_1:def 18;
A2: dom p c= NAT by RELAT_1:def 18;
A3: now
hereby
assume
A4: for x being set st x in dom p holds p.x = s.x;
let x be set;
assume
A5: x in dom p;
then reconsider l = x as Element of NAT by A2;
thus Comput(P,s,k).x = s.l by Th54
.= p.x by A4,A5;
end;
assume
A6: for x being set st x in dom p holds p.x = Comput(P,s,k).x;
let x be set;
assume
A7: x in dom p;
then reconsider l = x as Element of NAT by A2;
thus s.x = Comput(P,s,k).l by Th54
.= p.x by A6,A7;
end;
dom s = the carrier of S by PARTFUN1:def 4;
then dom p c= dom s by RELAT_1:def 18;
hence thesis by A1,A3,GRFUNC_1:8;
end;
reserve N for with_non-empty_elements non empty set,
S for IC-Ins-separated (non empty AMI-Struct over N);
canceled 12;
theorem
for S being steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N) for p being PartState of S,
P being (the Instructions of S)-valued ManySortedSet of NAT,
s being
State of S st p c= s for i being Element of NAT holds ProgramPart p c=
Comput(P,s,i)
proof
let S be steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N);
let p be PartState of S,
P being (the Instructions of S)-valued ManySortedSet of NAT,
s be State of S such that
A1: p c= s;
let i be Element of NAT;
ProgramPart p c= p by RELAT_1:88;
then ProgramPart p c= s by A1,XBOOLE_1:1;
hence thesis by Th81;
end;
canceled 17;
theorem
for N being with_non-empty_elements set for S being
steady-programmed (non empty stored-program AMI-Struct over N) for i being
Instruction of S, s being State of S
holds ProgramPart Exec (i, s) = ProgramPart s by Lm1;
canceled 5;
reserve m,n for Element of NAT;
theorem
for S being steady-programmed IC-Ins-separated definite (non empty
stored-program AMI-Struct over N)
for P being (the Instructions of S)-valued ManySortedSet of NAT
for s being State of S, n being Nat
holds ProgramPart s = ProgramPart Comput(P,s,n) by Lm2;
theorem
for N being with_non-empty_elements non empty set,
S being steady-programmed
IC-Ins-separated definite (non empty stored-program AMI-Struct over N),
p being NAT-defined (the Instructions of S)-valued Function,
s1,s2 being State of S
st p c= s1 & p c= s2
holds Comput(ProgramPart s1,s1,i) | dom p
= Comput(ProgramPart s2,s2,i) | dom p
proof
let N be with_non-empty_elements non empty set,
S be steady-programmed
IC-Ins-separated definite (non empty stored-program AMI-Struct over N),
p be NAT-defined (the Instructions of S)-valued Function,
s1,s2 be State of S such that
A1: p c= s1 and
A2: p c= s2;
set Cs2= Comput(ProgramPart s2,s2,i);
set Cs1= Comput(ProgramPart s1,s1,i);
A3: now
let x be set;
assume
A4: x in dom p;
dom p c= NAT by RELAT_1:def 18;
then reconsider l=x as Element of NAT by A4;
A5: s1.l = Cs1.l & s2.l = Cs2.l by Th54;
p.x=s1.x by A1,A4,GRFUNC_1:8;
hence Cs1.x = Cs2.x by A2,A4,A5,GRFUNC_1:8;
end;
dom Cs1 = the carrier of S by PARTFUN1:def 4
.=dom Cs2 by PARTFUN1:def 4;
hence thesis by A3,FUNCT_1:166;
end;
set III = {[1,0,0],[0,0,0]};
registration
let N be with_non-empty_elements set;
cluster STC N -> steady-programmed;
coherence
proof
set IT = STC N;
set Ok = the Object-Kind of IT;
A3: the Instructions of IT = III by AMISTD_1:def 11;
let s be State of IT, i be Instruction of IT, l be Element of NAT;
consider f being Function of product the Object-Kind of IT, product the
Object-Kind of IT such that
A4: for s being Element of product the Object-Kind of IT holds f.s
= s+*(NAT .-->succ(s.NAT)) and
A5: the Execution of IT = ([1,0,0] .--> f) +* ([0,0,0] .--> id product
the Object-Kind of IT) by AMISTD_1:def 11;
A6: for s being State of IT holds f.s = s+*(NAT .-->succ(s.NAT))
proof let s be State of IT;
reconsider s as Element of product the Object-Kind of IT by PBOOLE:155;
f.s = s+*(NAT .-->succ(s.NAT)) by A4;
hence thesis;
end;
reconsider ss=s as Element of product the Object-Kind of IT
by PBOOLE:155;
not NAT in NAT;
then l <> NAT;
then not l in {NAT} by TARSKI:def 1;
then
A7: not l in dom (NAT .-->succ(s.NAT)) by FUNCOP_1:19;
per cases by A3,TARSKI:def 2;
suppose
A8: i = [1,0,0];
then
A9: i in {[1,0,0]} by TARSKI:def 1;
now
assume i in dom ([0,0,0] .--> id product the Object-Kind of IT);
then i in {[0,0,0]} by FUNCOP_1:19;
then i = [0,0,0] by TARSKI:def 1;
hence contradiction by A8,MCART_1:28;
end;
then (the Execution of IT).i = ([1,0,0] .--> f).i by A5,FUNCT_4:12
.= f by A9,FUNCOP_1:13;
hence Exec(i,s).l = (s+*(NAT .-->succ(s.NAT))).l by A6
.= s.l by A7,FUNCT_4:12;
end;
suppose
i = [0,0,0];
then
A10: i in {[0,0,0]} by TARSKI:def 1;
then i in dom ([0,0,0] .--> id product the Object-Kind of IT) by
FUNCOP_1:19;
then (the Execution of IT).i = ([0,0,0] .--> id product the Object-Kind
of IT).i by A5,FUNCT_4:14
.= id product the Object-Kind of IT by A10,FUNCOP_1:13;
then (the Execution of IT).i.ss = ss by FUNCT_1:35;
hence thesis;
end;
end;
end;
registration
let N be with_non-empty_elements non empty set;
cluster standard halting realistic steady-programmed
standard-ins (IC-Ins-separated definite (non empty stored-program AMI-Struct
over N));
existence
proof
take STC N;
thus thesis;
end;
end;
begin :: Addenda
:: from SCMRING4, 2008.03.13, A.T.
reserve i, j, k for natural number,
n for Element of NAT,
N for with_non-empty_elements non empty set,
S for standard (IC-Ins-separated definite
(non empty stored-program AMI-Struct over N)),
l for Element of NAT,
f for FinPartState of S;
Lm3: for
a,b,c being set st a c= c & b c= c \ a holds c = a \/ (c \ (a\/b)) \/ b
proof
let a,b,c be set such that
A1: a c= c and
A2: b c= c \ a;
thus a \/ (c \ (a\/b)) \/ b = a \/ (c \ a \ b) \/ b by XBOOLE_1:41
.= a \/ ((c \ a \ b) \/ b) by XBOOLE_1:4
.= a \/ ((c \ a) \/ b) by XBOOLE_1:39
.= a \/ (c \ a) by A2,XBOOLE_1:12
.= a \/ c by XBOOLE_1:39
.= c by A1,XBOOLE_1:12;
end;
Lm4: for S being IC-Ins-separated definite realistic
(non empty stored-program AMI-Struct over N) holds
NAT c= (the carrier of S) \ {IC S}
proof
let S be IC-Ins-separated definite realistic
(non empty stored-program AMI-Struct over N);
let i be set;
A1: NAT c= the carrier of S by COMPOS_1:def 2;
assume
A2: i in NAT;
then i <> IC S by COMPOS_1:3;
then not i in {IC S} by TARSKI:def 1;
hence thesis by A1,A2,XBOOLE_0:def 5;
end;
canceled 2;
registration
let N be with_non-empty_elements non empty set;
cluster standard regular J/A-independent homogeneous
halting realistic steady-programmed
with_explicit_jumps (IC-Ins-separated definite standard-ins
(non empty stored-program AMI-Struct over N));
existence
proof
take STC N;
thus thesis;
end;
end;
registration
let N be with_non-empty_elements non empty set;
cluster homogeneous realistic steady-programmed
halting
with_explicit_jumps Exec-preserving
(regular J/A-independent standard (standard-ins IC-Ins-separated definite
(non empty stored-program AMI-Struct over N)));
existence
proof
take STC N;
thus thesis;
end;
end;
registration
let N be with_non-empty_elements non empty set;
cluster IC-relocable (homogeneous realistic steady-programmed
with_explicit_jumps Exec-preserving halting
(regular J/A-independent standard (standard-ins IC-Ins-separated definite
(non empty stored-program AMI-Struct over N))));
existence
proof
take STC N;
thus thesis;
end;
end;
theorem
for S being Exec-preserving IC-Ins-separated definite realistic
steady-programmed (non empty stored-program AMI-Struct over N),
s being State of S, i being Instruction of S,
p being NAT-defined FinPartState of S
holds Exec (i, s +* p) = Exec (i,s) +* p
proof
let S be Exec-preserving IC-Ins-separated definite realistic
steady-programmed (non empty stored-program AMI-Struct over N),
s be State of S, i be Instruction of S, p be NAT-defined FinPartState of S;
set C = the carrier of S;
set I = NAT;
set D = C \ ({IC S} \/ I);
A1: dom p c= I by RELAT_1:def 18;
A2: dom s = C by PARTFUN1:def 4;
A3: dom (s+*p) = C by PARTFUN1:def 4;
A4: dom Exec(i,s) = C by PARTFUN1:def 4;
A5: dom Exec(i,s+*p) = C by PARTFUN1:def 4;
D = C \ I \ {IC S} by XBOOLE_1:41;
then
A6: D \/ {IC S} = (C \ I) \/ {IC S} by XBOOLE_1:39;
A7: {IC S} c= C by ZFMISC_1:37;
{IC S} c= C \ I
proof
let x be set;
assume
A8: x in {IC S};
then
A9: x = IC S by TARSKI:def 1;
not x in I by A9,COMPOS_1:3;
hence thesis by A7,A8,XBOOLE_0:def 5;
end;
then
A10: C \ I = D \/ {IC S} by A6,XBOOLE_1:12;
I c= C \ {IC S} by Lm4;
then
A11: C = {IC S} \/ D \/ I by A7,Lm3;
D \/ {IC S} misses I
proof
assume not thesis;
then consider o being set such that
A12: o in D \/ {IC S} and
A13: o in I by XBOOLE_0:3;
reconsider l = o as Element of NAT by A13;
A14: o in D or o in {IC S} by A12,XBOOLE_0:def 3;
per cases by A14,TARSKI:def 1;
suppose o in D;
then not o in {IC S} \/ I by XBOOLE_0:def 5;
hence contradiction by A13,XBOOLE_0:def 3;
end;
suppose o = IC S;
then l = IC S;
hence contradiction by COMPOS_1:3;
end;
end;
then
A15: D \/ {IC S} misses dom p by A1,XBOOLE_1:63;
then s|(dom s \ I) = (s+*p)|(dom(s+*p) \ I) by A2,A3,A10,FUNCT_4:76;
then NPP s = NPP(s+*p) by COMPOS_1:233;
then
A16: NPP Exec(i,s) = NPP Exec(i,s+*p) by AMISTD_2:def 20;
A17: (Exec(i,s) +* p) | (D \/ {IC S})
= Exec(i,s) | (D \/ {IC S}) by A15,FUNCT_4:76
.= Exec(i,s +* p) | (D \/ {IC S}) by A4,A5,A10,A16,COMPOS_1:233;
A18: ProgramPart Exec (i, s +* p) = ProgramPart (s +* p) by Lm1
.= ProgramPart s +* ProgramPart p by FUNCT_4:75
.= ProgramPart Exec (i,s) +* ProgramPart p by Lm1
.= ProgramPart (Exec (i, s) +* p) by FUNCT_4:75;
thus Exec (i, s +* p)
= Exec (i, s +* p)| ({IC S} \/ D \/ I) by A5,A11,RELAT_1:98
.= (Exec (i, s) +* p)| ({IC S} \/ D)
+* (Exec (i, s) +* p)|I by A17,A18,FUNCT_4:83
.= (Exec (i,s) +* p)| ({IC S} \/ D \/ I) by FUNCT_4:83
.= (Exec (i,s) +* p)| dom(Exec (i, s) +* p) by A11,PARTFUN1:def 4
.= Exec (i,s) +* p by RELAT_1:98;
end;
reserve d1,d2,d3,d4,d5 for Element of SCM-Data-Loc,
k1,k2,k3,k4,k5,k6 for
Integer;
set S1={ [0,{},<*k1*>] where k1 is Element of INT: not contradiction},
S2={ [1,{},<*
d1*>] : not contradiction},
S3={ [I1,{},<*d2,k2*>] where I1 is Element of Segm 14,
d2 is Element of SCM-Data-Loc, k2 is Element of INT : I1 in {2,3}},
S4={ [I2,{},<*
d3,k3,k4*>] where I2 is Element of Segm 14, d3 is Element of SCM-Data-Loc, k3,
k4 is Element of INT: I2 in {4,5,6,7,8} },
S5={ [I3,{},<*d4,d5,k5,k6*>] where I3
is Element of Segm 14, d4,d5 is Element of SCM-Data-Loc, k5,k6 is Element of
INT: I3 in {9,10,11,12,13} };
reserve I for Instruction of SCMPDS;
Lm2: I in S1 or I in S2 or I in S3 or I in S4 or I in S5
proof
I in S1 \/ S2 \/ S3 \/ S4 or I in S5 by XBOOLE_0:def 3;
then I in S1 \/ S2 \/ S3 or I in S4 or I in S5 by XBOOLE_0:def 3;
then I in S1 \/ S2 or I in S3 or I in S4 or I in S5 by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
theorem Th96:
for s being State of SCMPDS, i being Instruction of SCMPDS, l
being Element of NAT holds Exec(i,s).l = s.l
proof
let s be State of SCMPDS, i be Instruction of SCMPDS, l be
Element of NAT;
reconsider c = i as Element of SCMPDS-Instr;
reconsider S = s as Element of product SCMPDS-OK by PBOOLE:155;
reconsider l9 = l as Element of NAT;
now
per cases by Lm2;
case
c in S1;
then ex k1 being Element of INT st c = [0,{},<*k1*>];
hence SCM-Exec-Res(c,S).l9 = SCM-Chg(S,jump_address(S,c const_INT )).l9
by SCMPDS_1:def 24
.= S.l9 by SCMPDS_1:28;
end;
case
A1: c in S2;
set SS=SCM-Chg(S,c address_1, S.Address_Add(S,c address_1,RetSP));
ex d1 st c = [1,{},<*d1*>] by A1;
hence SCM-Exec-Res(c,S).l9 = SCM-Chg(SS,PopInstrLoc(S,Address_Add(S,c
address_1,RetIC))).l9 by SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
case
A2: c in S3;
set SS=SCM-Chg(S, c P21address, c P22const);
consider I1 being Element of Segm 14, d1 being Element of SCM-Data-Loc,
k1 being Element of INT such that
A3: c = [I1,{},<*d1,k1*>] and
A4: I1 in { 2,3 } by A2;
now
per cases by A4,TARSKI:def 2;
case
I1=2;
hence SCM-Exec-Res(c,S).l9 = SCM-Chg(SS,succ IC S).l9 by A3,
SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
case
A5: I1=3;
set SS = SCM-Chg(S,Address_Add(S,c P21address,c P22const),IC S);
thus SCM-Exec-Res(c,S).l9 = SCM-Chg(SS,succ IC S).l9 by A3,A5,
SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
end;
hence SCM-Exec-Res(c,S).l9 = S.l9;
end;
case
c in S4;
then consider
I1 being Element of Segm 14, d1 being Element of SCM-Data-Loc,
k1,k2 being Element of INT such that
A6: c = [I1,{},<*d1,k1,k2*>] and
A7: I1 in { 4,5,6,7,8};
now
per cases by A7,ENUMSET1:def 3;
case
I1 = 4;
hence SCM-Exec-Res(c,S).l9 = SCM-Chg(S, IFEQ(S.Address_Add(S,c
P31address,c P32const), 0, succ IC S,jump_address(S,c P33const ))).l9 by A6,
SCMPDS_1:def 24
.= S.l9 by SCMPDS_1:28;
end;
case
I1 = 5;
hence SCM-Exec-Res(c,S).l9 = SCM-Chg(S, IFGT(S.Address_Add(S,c
P31address,c P32const), 0, succ IC S,jump_address(S,c P33const ))).l9 by A6,
SCMPDS_1:def 24
.= S.l9 by SCMPDS_1:28;
end;
case
I1 = 6;
hence SCM-Exec-Res(c,S).l9 = SCM-Chg(S,IFGT(0, S.Address_Add(S,c
P31address,c P32const), succ IC S,jump_address(S,c P33const ))).l9 by A6,
SCMPDS_1:def 24
.= S.l9 by SCMPDS_1:28;
end;
case
A8: I1 = 7;
set SS=SCM-Chg(S,Address_Add(S,c P31address,c P32const),c P33const);
thus SCM-Exec-Res(c,S).l9 =SCM-Chg(SS,succ IC S).l9 by A6,A8,
SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
case
A9: I1 = 8;
set SS=SCM-Chg(S,Address_Add(S,c P31address,c P32const), S.
Address_Add(S,c P31address,c P32const)+ (c P33const));
thus SCM-Exec-Res(c,S).l9 = SCM-Chg(SS,succ IC S).l9 by A6,A9,
SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
end;
hence SCM-Exec-Res(c,S).l9 = S.l9;
end;
case
c in S5;
then consider I1 being Element of Segm 14, d1,d2 being Element of
SCM-Data-Loc, k1,k2 being Element of INT such that
A10: c = [I1,{},<*d1,d2,k1,k2*>]and
A11: I1 in { 9,10,11,12,13 };
now
per cases by A11,ENUMSET1:def 3;
case
A12: I1 = 9;
set SS=SCM-Chg(S, Address_Add(S,c P41address,c P43const), S.
Address_Add(S,c P41address,c P43const)+ S.Address_Add(S,c P42address,c P44const
));
thus SCM-Exec-Res(c,S).l9 = SCM-Chg(SS,succ IC S).l9 by A10,A12,
SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
case
A13: I1 = 10;
set SS=SCM-Chg(S, Address_Add(S,c P41address,c P43const), S.
Address_Add(S,c P41address,c P43const)- S.Address_Add(S,c P42address,c P44const
));
thus SCM-Exec-Res(c,S).l9 = SCM-Chg(SS,succ IC S).l9 by A10,A13,
SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
case
A14: I1 = 11;
set SS=SCM-Chg(S, Address_Add(S,c P41address,c P43const), S.
Address_Add(S,c P41address,c P43const)* S.Address_Add(S,c P42address,c P44const
));
thus SCM-Exec-Res(c,S).l9 = SCM-Chg(SS,succ IC S).l9 by A10,A14,
SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
case
A15: I1 = 12;
set SA= SCM-Chg(S,Address_Add(S,c P41address,c P43const), S.
Address_Add(S,c P41address,c P43const) div S.Address_Add(S,c P42address,c
P44const)), SB=SCM-Chg(SA, Address_Add(S,c P42address,c P44const), S.
Address_Add(S,c P41address,c P43const) mod S.Address_Add(S,c P42address,c
P44const));
thus SCM-Exec-Res(c,S).l9 = SCM-Chg(SB,succ IC S).l9 by A10,A15,
SCMPDS_1:def 24
.= SB.l9 by SCMPDS_1:28
.= SA.l9 by SCMPDS_1:32
.= S.l9 by SCMPDS_1:32;
end;
case
A16: I1 = 13;
set SS=SCM-Chg(S, Address_Add(S,c P41address,c P43const), S.
Address_Add(S,c P42address,c P44const));
thus SCM-Exec-Res(c,S).l9 = SCM-Chg(SS,succ IC S).l9 by A10,A16,
SCMPDS_1:def 24
.= SS.l9 by SCMPDS_1:28
.= S.l9 by SCMPDS_1:32;
end;
end;
hence SCM-Exec-Res(c,S).l9 = S.l9;
end;
end;
hence thesis by SCMPDS_1:def 25;
end;
registration
cluster SCMPDS -> steady-programmed;
coherence
proof
let s be State of SCMPDS, i be Instruction of SCMPDS, l be
Element of NAT;
thus Exec(i,s).l = s.l by Th96;
end;
end;