:: The Properties of Instructions of { \bf SCM } over Ring
:: by Artur Korni{\l}owicz
::
:: Received April 14, 2000
:: Copyright (c) 2000-2026 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, FUNCSDOM, SUBSET_1, AMI_3, AMI_1, FSM_1, STRUCT_0,
AMI_2, TARSKI, ZFMISC_1, RELAT_1, FUNCOP_1, XBOOLE_0, CAT_1, FUNCT_1,
CARD_1, GRAPHSP, FINSEQ_1, AMISTD_2, CARD_3, AMISTD_1, CIRCUIT2, FUNCT_4,
SETFAM_1, SUPINF_2, ARYTM_3, XXREAL_0, GOBOARD5, ARYTM_1, GROUP_1,
FRECHET, PARTFUN1, COMPOS_1, NAT_1, GOBRD13, MEMSTR_0;
notations TARSKI, XBOOLE_0, SUBSET_1, ENUMSET1, XTUPLE_0, MCART_1, SETFAM_1,
RELAT_1, FUNCT_1, XXREAL_0, VALUED_1, STRUCT_0, ALGSTR_0, VECTSP_1,
ORDINAL1, CARD_1, NUMBERS, XCMPLX_0, NAT_1, FUNCOP_1, FINSEQ_1, PARTFUN1,
FUNCT_4, CARD_3, FUNCT_7, GROUP_1, MEMSTR_0, COMPOS_0, COMPOS_1,
EXTPRO_1, AMI_2, AMI_3, SCMRING1, SCMRING2, AMISTD_1, AMISTD_2, SCMRINGI;
constructors FINSEQ_4, REALSET2, AMI_3, SCMRING2, AMISTD_2, RELSET_1,
AMISTD_1, FUNCT_7, PRE_POLY, SCMRING1, XTUPLE_0;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, CARD_3,
STRUCT_0, VECTSP_1, FINSET_1, SCMRING2, AMISTD_2, FUNCT_4, VALUED_0,
EXTPRO_1, NAT_1, FUNCT_7, PRE_POLY, MEMSTR_0, CARD_1, COMPOS_0, XTUPLE_0,
FINSEQ_1;
requirements NUMERALS, REAL, BOOLE, SUBSET, ARITHM;
definitions TARSKI, AMISTD_2, XBOOLE_0;
equalities SCMRING2, AMISTD_1, FUNCOP_1, COMPOS_1, EXTPRO_1, MEMSTR_0,
COMPOS_0, SCMRINGI, XTUPLE_0;
expansions AMISTD_1, XBOOLE_0, COMPOS_0;
theorems TARSKI, NAT_1, SCMRING2, AMI_3, FUNCT_4, FUNCT_1, ZFMISC_1, FUNCOP_1,
SCMRING1, SETFAM_1, AMISTD_1, STRUCT_0, AMI_2, RLVECT_1, LMOD_6,
FINSEQ_1, CARD_3, ORDINAL1, XBOOLE_0, XBOOLE_1, ENUMSET1, PARTFUN1,
PBOOLE, VALUED_1, EXTPRO_1, FUNCT_7, MEMSTR_0, COMPOS_0, XTUPLE_0;
begin
reserve R for Ring,
r for Element of R,
a, b, d1, d2 for Data-Location of R,
il, i1, i2 for Nat,
I for Instruction of SCM R,
s,s1, s2 for State of SCM R,
T for InsType of the InstructionsF of SCM R,
k for Nat;
theorem Th1:
Values a = the carrier of R
proof
a in Data-Locations SCM & the_Values_of SCM R = (SCM-VAL R)*SCM-OK
by SCMRING2:1,24;
hence thesis by AMI_3:27,SCMRING1:4;
end;
definition
let R be Ring;
let la, lb be Data-Location of R;
let a, b be Element of R;
redefine func (la,lb) --> (a,b) -> FinPartState of SCM R; :: redefines --> (FUNCT_4, definition)
coherence
proof
reconsider b9 = b as Element of Values lb by Th1;
reconsider a9 = a as Element of Values la by Th1;
(la,lb) --> (a9,b9) is FinPartState of SCM R;
hence thesis;
end;
end;
theorem Th2:
a <> IC SCM R
proof
a in SCM-Data-Loc by AMI_2:def 16;
then a <> NAT by AMI_2:20;
hence thesis by SCMRING2:8;
end;
theorem
for o being Object of SCM R
holds o = IC SCM R or o is Data-Location of R
proof
let o be Object of SCM R;
assume o <> IC SCM R;
then not o in {IC SCM R} by TARSKI:def 1;
then
A1: not o in {NAT} by SCMRING2:8;
not o in {NAT} by A1;
then o in (the carrier of SCM R) \ ({NAT}) by XBOOLE_0:def 5;
then o in SCM-Data-Loc by SCMRING2:25;
hence thesis by AMI_2:def 16;
end;
::$CT
theorem
InsCode (a:=b) = 1;
theorem
InsCode AddTo(a,b) = 2;
theorem
InsCode SubFrom(a,b) = 3;
theorem
InsCode MultBy(a,b) = 4;
theorem
InsCode (a:=r) = 5;
theorem
InsCode goto(i1,R) = 6;
theorem
InsCode (a=0_goto i1) = 7;
theorem Th11:
InsCode I = 0 implies I = halt SCM R
proof
A1: I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or
(ex
a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto(i1,R)) or
(ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r by SCMRING2:7;
assume InsCode I = 0;
hence thesis by A1;
end;
theorem Th12:
InsCode I = 1 implies ex a, b st I = a:=b
proof
A1: I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex
a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto(i1,R)) or
(ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r by SCMRING2:7;
assume InsCode I = 1;
hence thesis by A1;
end;
theorem Th13:
InsCode I = 2 implies ex a, b st I = AddTo(a,b)
proof
A1: I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex
a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto(i1,R)) or
(ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r by SCMRING2:7;
assume InsCode I = 2;
hence thesis by A1;
end;
theorem Th14:
InsCode I = 3 implies ex a, b st I = SubFrom(a,b)
proof
A1: I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex
a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto(i1,R)) or
(ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r by SCMRING2:7;
assume InsCode I = 3;
hence thesis by A1;
end;
theorem Th15:
InsCode I = 4 implies ex a, b st I = MultBy(a,b)
proof
A1: I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex
a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto(i1,R)) or
(ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r by SCMRING2:7;
assume InsCode I = 4;
hence thesis by A1;
end;
theorem Th16:
InsCode I = 5 implies ex a, r st I = a:=r
proof
A1: I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex
a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto(i1,R)) or
(ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r by SCMRING2:7;
assume InsCode I = 5;
hence thesis by A1;
end;
theorem Th17:
InsCode I = 6 implies ex i2 st I = goto(i2,R)
proof
A1: I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex
a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto(i1,R)) or
(ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r by SCMRING2:7;
assume InsCode I = 6;
hence thesis by A1;
end;
theorem Th18:
InsCode I = 7 implies ex a, i1 st I = a=0_goto i1
proof
A1: I = [0,{},{}] or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b)) or (ex
a,b st I = SubFrom(a,b)) or (ex a,b st I = MultBy(a,b)) or
(ex i1 st I = goto(i1,R)) or
(ex a,i1 st I = a=0_goto i1) or ex a,r st I = a:=r by SCMRING2:7;
assume InsCode I = 7;
hence thesis by A1;
end;
Lm1: for x, y being set st x in dom <*y*> holds x = 1
proof
let x, y be set;
assume x in dom <*y*>;
then x in Seg 1 by FINSEQ_1:def 8;
hence thesis by FINSEQ_1:2,TARSKI:def 1;
end;
Lm2: T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7
proof
consider y being object such that
A1: [T,y] in proj1 the InstructionsF of SCM R by XTUPLE_0:def 12;
consider x being object such that
A2: [[T,y],x] in the InstructionsF of SCM R by A1,XTUPLE_0:def 12;
[T,y,x] in SCM-Instr R by A2,SCMRING2:def 1;
then
[T,y,x] in { [0,{},{}] }
\/ { [I,{},<*a,b*>]
where I is Element of Segm 8, a, b is Element of Data-Locations SCM:
I in { 1,2,3,4 } }
\/ the set of all [6,<*i*>,{}] where i is Nat
\/ the set of all [7,<*i*>,<*a*>]
where i is Nat, a is Element of Data-Locations SCM
or [T,y,x] in the set of all [5,{},<*a,r*>]
where a is Element of Data-Locations SCM, r is Element of R
by AMI_3:27,XBOOLE_0:def 3;
then
[T,y,x] in { [0,{},{}] } \/ { [I,{},<*a,b*>]
where I is Element of Segm 8, a, b
is Element of Data-Locations SCM: I in { 1,2,3,4 } } \/ the set of all
[6,<*i*>,{}]
where i is Nat or [T,y,x] in the set of all [7,<*i*>,<*a*>]
where i is Nat, a is Element of Data-Locations SCM or
[T,y,x] in the set of all
[5,{},<*a,r*>] where a is Element of Data-Locations SCM, r is Element of R
by XBOOLE_0:def 3;
then
A3: [T,y,x] in { [0,{},{}] }
\/ { [I,{},<*a,b*>] where I is Element of Segm 8, a, b
is Element of Data-Locations SCM: I in { 1,2,3,4 } } or
[T,y,x] in the set of all [6,<*i*>,{}] where i
is Nat or
[T,y,x] in the set of all [7,<*i*>,<*a*>] where i is
Nat, a is Element of Data-Locations SCM or
[T,y,x] in the set of all
[5,{},<*a,r*>] where a is Element of Data-Locations SCM, r is Element of R
by XBOOLE_0:def 3;
per cases by A3,XBOOLE_0:def 3;
suppose
[T,y,x] in { [0,{},{}] };
then [T,y,x] = [0,{},{}] by TARSKI:def 1;
hence thesis by XTUPLE_0:3;
end;
suppose
[T,y,x] in { [I,{},<*a,b*>] where I is Element of Segm 8, a, b is
Element of Data-Locations SCM: I in { 1,2,3,4 } };
then
ex I being Element of Segm 8, a,b being Element of Data-Locations SCM
st [T,y,x] = [I,{},<*a,b*>] & I in { 1,2,3,4 };
then T in { 1,2,3,4 } by XTUPLE_0:3;
hence thesis by ENUMSET1:def 2;
end;
suppose
[T,y,x] in the set of all [6,<*i*>,{}] where i is Nat;
then ex i being Nat st [T,y,x] = [6,<*i*>,{}];
hence thesis by XTUPLE_0:3;
end;
suppose
[T,y,x] in the set of all [7,<*i*>,<*a*>] where i is Nat, a is Element of
Data-Locations SCM;
then
ex i being Nat, a being Element of Data-Locations SCM
st [T,y,x] =
[7,<*i*>,<*a*>];
hence thesis by XTUPLE_0:3;
end;
suppose
[T,y,x] in the set of all
[5,{},<*a,r*>] where a is Element of Data-Locations SCM, r is
Element of R;
then
ex a being Element of Data-Locations SCM, r being Element of R
st [T,y,x] = [5,{},<*a,r*>];
hence thesis by XTUPLE_0:3;
end;
end;
theorem
T = 0 implies JumpParts T = {0}
proof
assume
A1: T = 0;
hereby
let a be object;
assume a in JumpParts T;
then consider I such that
A2: a = JumpPart I and
A3: InsCode I = T;
I = halt SCM R by A1,A3,Th11;
then a = {} by A2;
hence a in {0} by TARSKI:def 1;
end;
let a be object;
assume a in {0};
then
A4: a = 0 by TARSKI:def 1;
InsCode halt SCM R = 0 & JumpPart halt SCM R = 0;
hence thesis by A1,A4;
end;
theorem
T = 1 implies JumpParts T = {{}}
proof
assume
A1: T = 1;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM R such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = a:=b by A1,A3,Th12;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location of R;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart(a:= a);
InsCode(a:= a) = 1;
hence thesis by A5,A1;
end;
theorem
T = 2 implies JumpParts T = {{}}
proof
assume
A1: T = 2;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM R such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = AddTo(a,b) by A1,A3,Th13;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location of R;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart AddTo(a,a);
InsCode AddTo(a,a) = 2;
hence thesis by A5,A1;
end;
theorem
T = 3 implies JumpParts T = {{}}
proof
assume
A1: T = 3;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM R such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = SubFrom(a,b) by A1,A3,Th14;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location of R;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart SubFrom(a,a);
InsCode SubFrom(a,a) = 3;
hence thesis by A5,A1;
end;
theorem
T = 4 implies JumpParts T = {{}}
proof
assume
A1: T = 4;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM R such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = MultBy(a,b) by A1,A3,Th15;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location of R;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart MultBy(a,a);
InsCode MultBy(a,a) = 4;
hence thesis by A5,A1;
end;
theorem
T = 5 implies JumpParts T = {{}}
proof
assume
A1: T = 5;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM R such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,r such that
A4: I = a:=r by A1,A3,Th16;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location of R, r = the Element of R;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart(a:=r);
InsCode(a:=r) = 5;
hence thesis by A5,A1;
end;
theorem Th25:
T = 6 implies dom product" JumpParts T = {1}
proof
set i1 = the Element of NAT;
assume
A1: T = 6;
hereby
let x be object;
InsCode goto(i1,R) = 6;
then
A2: JumpPart goto(i1,R) in JumpParts T by A1;
assume x in dom product" JumpParts T;
then x in DOM JumpParts T by CARD_3:def 12;
then x in dom JumpPart goto(i1,R) by A2,CARD_3:108;
hence x in {1} by FINSEQ_1:2,def 8;
end;
let x be object;
assume
A3: x in {1};
for f being Function st f in JumpParts T holds x in dom f
proof
let f be Function;
assume f in JumpParts T;
then consider I being Instruction of SCM R such that
A4: f = JumpPart I and
A5: InsCode I = T;
consider i1 such that
A6: I = goto(i1,R) by A1,A5,Th17;
f = <*i1*> by A4,A6;
hence thesis by A3,FINSEQ_1:2,def 8;
end;
then x in DOM JumpParts T by CARD_3:109;
hence thesis by CARD_3:def 12;
end;
theorem Th26:
T = 7 implies dom product" JumpParts T = {1}
proof
set i1 = the Element of NAT,a = the Data-Location of R;
assume
A1: T = 7;
hereby
let x be object;
InsCode (a =0_goto i1) = 7;
then
A2: JumpPart (a =0_goto i1) in JumpParts T by A1;
assume x in dom product" JumpParts T;
then x in DOM JumpParts T by CARD_3:def 12;
then x in dom JumpPart (a =0_goto i1) by A2,CARD_3:108;
hence x in {1} by FINSEQ_1:2,38;
end;
let x be object;
assume
A3: x in {1};
for f being Function st f in JumpParts T holds x in dom f
proof
let f be Function;
assume f in JumpParts T;
then consider I being Instruction of SCM R such that
A4: f = JumpPart I and
A5: InsCode I = T;
consider a, i1 such that
A6: I = a =0_goto i1 by A1,A5,Th18;
f = <*i1*> by A4,A6;
hence thesis by A3,FINSEQ_1:2,38;
end;
then x in DOM JumpParts T by CARD_3:109;
hence thesis by CARD_3:def 12;
end;
theorem
(product" JumpParts InsCode goto(i1,R)).1 = NAT
proof
dom product" JumpParts InsCode goto(i1,R) = {1} by Th25;
then
A1: 1 in dom product" JumpParts InsCode goto(i1,R) by TARSKI:def 1;
hereby
let x be object;
assume x in (product" JumpParts InsCode goto(i1,R)).1;
then x in pi(JumpParts InsCode goto(i1,R),1) by A1,CARD_3:def 12;
then consider g being Function such that
A2: g in JumpParts InsCode goto(i1,R) and
A3: x = g.1 by CARD_3:def 6;
consider I being Instruction of SCM R such that
A4: g = JumpPart I and
A5: InsCode I = InsCode goto(i1,R) by A2;
consider i2 such that
A6: I = goto(i2,R) by A5,Th17;
g = <*i2*> by A4,A6;
then x = i2 by A3;
hence x in NAT by ORDINAL1:def 12;
end;
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
JumpPart goto(x,R) = <*x*> & InsCode goto(i1,R) = InsCode goto(x,R);
then
A7: <*x*> in JumpParts InsCode goto(i1,R);
<*x*>.1 = x;
then x in pi(JumpParts InsCode goto(i1,R),1) by A7,CARD_3:def 6;
hence thesis by A1,CARD_3:def 12;
end;
theorem
(product" JumpParts InsCode (a =0_goto i1)).1 = NAT
proof
dom product" JumpParts InsCode (a =0_goto i1) = {1} by Th26;
then
A1: 1 in dom product" JumpParts InsCode (a =0_goto i1) by TARSKI:def 1;
hereby
let x be object;
assume x in (product" JumpParts InsCode (a =0_goto i1)).1;
then x in pi(JumpParts InsCode (a =0_goto i1),1) by A1,CARD_3:def 12;
then consider g being Function such that
A2: g in JumpParts InsCode (a =0_goto i1) and
A3: x = g.1 by CARD_3:def 6;
consider I being Instruction of SCM R such that
A4: g = JumpPart I and
A5: InsCode I = InsCode (a =0_goto i1) by A2;
consider b, i2 such that
A6: I = b =0_goto i2 by A5,Th18;
g = <*i2*> by A4,A6;
then x = i2 by A3;
hence x in NAT by ORDINAL1:def 12;
end;
let x be object;
assume x in NAT;
then reconsider x as Element of NAT;
JumpPart (a =0_goto x) = <*x*> & InsCode (a =0_goto i1) = InsCode
(a =0_goto x);
then
A7: <*x*> in JumpParts InsCode (a =0_goto i1);
<*x*>.1 = x;
then x in pi(JumpParts InsCode (a =0_goto i1),1) by A7,CARD_3:def 6;
hence thesis by A1,CARD_3:def 12;
end;
Lm3: for i being Instruction of SCM R holds (for l being Element of NAT
holds NIC(i,l)={l+1}) implies JUMP i is empty
proof
set p=1, q=2;
let i be Instruction of SCM R;
assume
A1: for l being Element of NAT holds NIC(i,l)={l+1};
set X = the set of all NIC(i,f) where f is Nat;
reconsider p, q as Element of NAT;
assume not thesis;
then consider x being object such that
A2: x in meet X;
NIC(i,p) = {p + 1} by A1;
then {p + 1} in X;
then x in {p + 1} by A2,SETFAM_1:def 1;
then
A3: x = p + 1 by TARSKI:def 1;
NIC(i,q) = {q + 1} by A1;
then {q + 1} in X;
then x in {q + 1} by A2,SETFAM_1:def 1;
hence contradiction by A3,TARSKI:def 1;
end;
registration
let R;
cluster JUMP halt SCM R -> empty;
coherence;
end;
registration
let R, a, b;
cluster a:=b -> sequential;
coherence
by SCMRING2:11;
cluster AddTo(a,b) -> sequential;
coherence
by SCMRING2:12;
cluster SubFrom(a,b) -> sequential;
coherence
by SCMRING2:13;
cluster MultBy(a,b) -> sequential;
coherence
by SCMRING2:14;
end;
registration
let R, a, r;
cluster a:=r -> sequential;
coherence
by SCMRING2:17;
end;
registration
let R, a, b;
cluster JUMP (a := b) -> empty;
coherence
proof
for l being Element of NAT holds NIC(a:=b,l)={l + 1}
by AMISTD_1:12;
hence thesis by Lm3;
end;
end;
registration
let R, a, b;
cluster JUMP AddTo(a, b) -> empty;
coherence
proof
for l being Element of NAT holds NIC(AddTo(a,b),l)={
l + 1} by AMISTD_1:12;
hence thesis by Lm3;
end;
end;
registration
let R, a, b;
cluster JUMP SubFrom(a, b) -> empty;
coherence
proof
for l being Element of NAT holds NIC(SubFrom(a,b),l)={
l + 1 } by AMISTD_1:12;
hence thesis by Lm3;
end;
end;
registration
let R, a, b;
cluster JUMP MultBy(a,b) -> empty;
coherence
proof
for l being Element of NAT holds NIC(MultBy(a,b),l)={
l + 1 } by AMISTD_1:12;
hence thesis by Lm3;
end;
end;
registration
let R, a, r;
cluster JUMP (a := r) -> empty;
coherence
proof
for l being Element of NAT holds NIC(a:=r,l)={l + 1}
by AMISTD_1:12;
hence thesis by Lm3;
end;
end;
theorem Th29:
NIC(goto(i1,R), il) = {i1}
proof
now
let x be object;
A1: il in NAT by ORDINAL1:def 12;
A2: now
reconsider il1 = il as Element of Values IC SCM R by MEMSTR_0:def 6,A1;
set I = goto(i1,R);
set t = the State of SCM R,
Q = the Instruction-Sequence of SCM R;
assume
A3: x = i1;
reconsider u = t+*(IC SCM R,il1)
as Element of product the_Values_of SCM R by CARD_3:107;
reconsider P = Q +* (il,I)
as Instruction-Sequence of SCM R;
A4: P/.il = P.il by PBOOLE:143,A1;
IC SCM R in dom t by MEMSTR_0:2;
then
A5: IC u = il by FUNCT_7:31;
il in NAT by ORDINAL1:def 12;
then il in dom Q by PARTFUN1:def 2;
then
A6: P.il = I by FUNCT_7:31;
then IC Following(P,u) = i1 by A5,A4,SCMRING2:15;
hence x in {IC Exec(goto(i1,R),s)
where s is Element of product the_Values_of SCM R
: IC s = il} by A3,A4,A5,A6;
end;
now
assume x in {IC Exec(goto(i1,R),s)
where s is Element of product the_Values_of SCM R
: IC s = il};
then
ex s being Element of product the_Values_of SCM R
st x = IC Exec(goto(i1,R),s) & IC s = il;
hence x = i1 by SCMRING2:15;
end;
hence
x in {i1} iff x in {IC Exec(goto(i1,R),s)
where s is Element of product the_Values_of SCM R
: IC s = il } by A2,TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem Th30:
JUMP goto(i1,R) = {i1}
proof
set X = the set of all NIC(goto(i1,R), il) ;
now
let x be object;
hereby
reconsider il1 = 1 as Element of NAT;
A1: NIC(goto(i1,R), il1) in X;
assume x in meet X;
then x in NIC(goto(i1,R), il1) by A1,SETFAM_1:def 1;
hence x in {i1} by Th29;
end;
assume x in {i1};
then
A2: x = i1 by TARSKI:def 1;
A3: now
let Y be set;
assume Y in X;
then consider il being Nat such that
A4: Y = NIC(goto(i1,R), il);
NIC(goto(i1,R), il) = {i1} by Th29;
hence i1 in Y by A4,TARSKI:def 1;
end;
NIC(goto(i1,R), i1) in X;
hence x in meet X by A2,A3,SETFAM_1:def 1;
end;
hence thesis by TARSKI:2;
end;
registration
let R, i1;
cluster JUMP goto(i1,R) -> 1-element;
coherence
proof
JUMP goto(i1,R) = {i1} by Th30;
hence thesis;
end;
end;
theorem Th31:
i1 in NIC(a=0_goto i1, il) & NIC(a=0_goto i1, il) c= {i1, il + 1}
proof
set t = the State of SCM R,
Q = the Instruction-Sequence of SCM R;
set I = a=0_goto i1;
reconsider a9 = a as Element of Data-Locations SCM by SCMRING2:1;
A1: il in NAT by ORDINAL1:def 12;
reconsider il1 = il as Element of Values IC SCM R by MEMSTR_0:def 6,A1;
Values a = ((SCM-VAL R)*SCM-OK).a9 by SCMRING2:24
.= the carrier of R by AMI_3:27,SCMRING1:4;
then reconsider 0R = 0.R as Element of Values a;
reconsider u = t+*(IC SCM R,il1)
as Element of product the_Values_of SCM R by CARD_3:107;
reconsider P = Q +* (il,I)
as Instruction-Sequence of SCM R;
reconsider v = u+*(a .--> 0R)
as Element of product the_Values_of SCM R by CARD_3:107;
A2: IC SCM R in dom t by MEMSTR_0:2;
IC SCM R <> a by Th2;
then not IC SCM R in dom (a .--> 0R) by TARSKI:def 1;
then
A4: IC v = IC u by FUNCT_4:11
.= il by A2,FUNCT_7:31;
A5: P/.il = P.il by PBOOLE:143,A1;
il in NAT by ORDINAL1:def 12;
then il in dom Q by PARTFUN1:def 2;
then
A6: P.il = I by FUNCT_7:31;
a in dom (a .--> 0R) by TARSKI:def 1;
then v.a = (a .--> 0R).a by FUNCT_4:13
.= 0.R by FUNCOP_1:72;
then IC Following(P,v) = i1 by A4,A6,A5,SCMRING2:16;
hence i1 in NIC(a=0_goto i1, il) by A4,A6,A5;
let x be object;
assume x in NIC(a=0_goto i1, il);
then consider s being Element of product the_Values_of SCM R
such that
A7: x = IC Exec(a=0_goto i1,s) & IC s = il;
per cases;
suppose
s.a = 0.R;
then x = i1 by A7,SCMRING2:16;
hence thesis by TARSKI:def 2;
end;
suppose
s.a <> 0.R;
then x = il+1 by A7,SCMRING2:16;
hence thesis by TARSKI:def 2;
end;
end;
theorem
for R being non trivial Ring, a being Data-Location of R, il, i1
being Element of NAT holds NIC(a=0_goto i1, il) = {i1, il + 1}
proof
let R be non trivial Ring, a be Data-Location of R, il, i1 be
Element of NAT;
set t = the State of SCM R,
Q = the Instruction-Sequence of SCM R;
set I = a=0_goto i1;
reconsider a9 = a as Element of Data-Locations SCM by SCMRING2:1;
A1: Values a = ((SCM-VAL R)*SCM-OK).a9 by SCMRING2:24
.= the carrier of R by AMI_3:27,SCMRING1:4;
reconsider il1 = il as Element of Values IC SCM R by MEMSTR_0:def 6;
thus NIC(a=0_goto i1, il) c= {i1, il + 1} by Th31;
reconsider u = t+*(IC SCM R,il1)
as Element of product the_Values_of SCM R by CARD_3:107;
reconsider P = Q +* (il,I) as Instruction-Sequence of SCM R;
let x be object;
A2: IC SCM R <> a by Th2;
A3: IC SCM R in dom t by MEMSTR_0:2;
assume
A4: x in {i1, il + 1};
per cases by A4,TARSKI:def 2;
suppose
A5: x = i1;
reconsider 0R = 0.R as Element of Values a by A1;
reconsider v = u+*(a .--> 0R)
as Element of product the_Values_of SCM R by CARD_3:107;
not IC SCM R in dom (a .--> 0R) by A2,TARSKI:def 1;
then
A7: IC v = IC u by FUNCT_4:11
.= il by A3,FUNCT_7:31;
A8: P/.il = P.il by PBOOLE:143;
il in NAT;
then il in dom Q by PARTFUN1:def 2;
then
A9: P.il = I by FUNCT_7:31;
a in dom (a .--> 0R) by TARSKI:def 1;
then v.a = (a .--> 0R).a by FUNCT_4:13
.= 0.R by FUNCOP_1:72;
then IC Following(P,v) = i1 by A7,A8,A9,SCMRING2:16;
hence thesis by A5,A7,A8,A9;
end;
suppose
A10: x = il + 1;
consider e being Element of R such that
A11: e <> 0.R by STRUCT_0:def 18;
reconsider E = e as Element of Values a by A1;
reconsider v = u+*(a .--> E)
as Element of product the_Values_of SCM R by CARD_3:107;
not IC SCM R in dom (a .--> E) by A2,TARSKI:def 1;
then
A13: IC v = IC u by FUNCT_4:11
.= il by A3,FUNCT_7:31;
A14: P/.il = P.il by PBOOLE:143;
il in NAT;
then il in dom Q by PARTFUN1:def 2;
then
A15: P.il = I by FUNCT_7:31;
a in dom (a .--> E) by TARSKI:def 1;
then v.a = (a .--> E).a by FUNCT_4:13
.= E by FUNCOP_1:72;
then IC Following(P,v) = il + 1 by A11,A13,A14,A15,SCMRING2:16;
hence thesis by A10,A13,A14,A15;
end;
end;
theorem Th33:
JUMP (a=0_goto i1) = {i1}
proof
set X = the set of all NIC(a=0_goto i1, il) ;
now
let x be object;
A1: now
let Y be set;
assume Y in X;
then ex il being Nat st Y = NIC(a=0_goto i1,il);
hence i1 in Y by Th31;
end;
hereby
reconsider il1 = 1, il2 = 2 as Element of NAT;
assume
A2: x in meet X;
A3: NIC(a=0_goto i1, il2) c= {i1, il2 + 1} by Th31;
NIC(a=0_goto i1, il2) in X;
then x in NIC(a=0_goto i1, il2) by A2,SETFAM_1:def 1;
then
A4: x = i1 or x = il2 + 1 by A3,TARSKI:def 2;
A5: NIC(a=0_goto i1, il1) c= {i1, il1 + 1} by Th31;
NIC(a=0_goto i1, il1) in X;
then x in NIC(a=0_goto i1, il1) by A2,SETFAM_1:def 1;
then x = i1 or x = il1 + 1 by A5,TARSKI:def 2;
hence x in {i1} by A4,TARSKI:def 1;
end;
assume x in {i1};
then
A6: x = i1 by TARSKI:def 1;
NIC(a=0_goto i1, i1) in X;
hence x in meet X by A6,A1,SETFAM_1:def 1;
end;
hence thesis by TARSKI:2;
end;
registration
let R, a, i1;
cluster JUMP (a =0_goto i1) -> 1-element;
coherence
proof
JUMP (a =0_goto i1) = {i1} by Th33;
hence thesis;
end;
end;
theorem Th34:
SUCC(il,SCM R) = {il, il + 1}
proof
set X = the set of all
NIC(I, il) \ JUMP I where I is Element of the InstructionsF of SCM
R;
set N = {il, il + 1};
now
let x be object;
hereby
assume x in union X;
then consider Y being set such that
A1: x in Y and
A2: Y in X by TARSKI:def 4;
consider i being Element of the InstructionsF of SCM R such that
A3: Y = NIC(i, il) \ JUMP i by A2;
per cases by SCMRING2:7;
suppose
i = [0,{},{}];
then i = halt SCM R;
then x in {il} \ JUMP halt SCM R by A1,A3,AMISTD_1:2;
then x = il by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex a,b st i = a:=b;
then consider a, b such that
A4: i = a:=b;
x in {il + 1} \ JUMP (a:=b) by A1,A3,A4,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex a,b st i = AddTo(a,b);
then consider a, b such that
A5: i = AddTo(a,b);
x in {il + 1} \ JUMP AddTo(a,b) by A1,A3,A5,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex a,b st i = SubFrom(a,b);
then consider a, b such that
A6: i = SubFrom(a,b);
x in {il + 1} \ JUMP SubFrom(a,b) by A1,A3,A6,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex a,b st i = MultBy(a,b);
then consider a, b such that
A7: i = MultBy(a,b);
x in {il + 1} \ JUMP MultBy(a,b) by A1,A3,A7,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex i1 st i = goto(i1,R);
then consider i1 such that
A8: i = goto(i1,R);
x in {i1} \ JUMP i by A1,A3,A8,Th29;
then x in {i1} \ {i1} by A8,Th30;
hence x in N by XBOOLE_1:37;
end;
suppose
ex a,i1 st i = a=0_goto i1;
then consider a, i1 such that
A9: i = a=0_goto i1;
A10: NIC(i, il) c= {i1, il + 1} by A9,Th31;
x in NIC(i, il) by A1,A3,XBOOLE_0:def 5;
then
A11: x = i1 or x = il + 1 by A10,TARSKI:def 2;
x in NIC(i, il) \ {i1} by A1,A3,A9,Th33;
then not x in {i1} by XBOOLE_0:def 5;
hence x in N by A11,TARSKI:def 1,def 2;
end;
suppose
ex a,r st i = a:=r;
then consider a, r such that
A12: i = a := r;
x in {il + 1} \ JUMP (a:=r) by A1,A3,A12,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
end;
assume
A13: x in {il, il + 1};
per cases by A13,TARSKI:def 2;
suppose
A14: x = il;
set i = halt SCM R;
NIC(i, il) \ JUMP i = {il} by AMISTD_1:2;
then
A15: {il} in X;
x in {il} by A14,TARSKI:def 1;
hence x in union X by A15,TARSKI:def 4;
end;
suppose
A16: x = il + 1;
set a = the Data-Location of R;
set i = AddTo(a,a);
NIC(i, il) \ JUMP i = {il + 1} by AMISTD_1:12;
then
A17: {il + 1} in X;
x in {il + 1} by A16,TARSKI:def 1;
hence x in union X by A17,TARSKI:def 4;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th35:
for k being Nat holds k+1 in SUCC(k,SCM R) &
for j being Nat st j in SUCC(k,SCM R) holds k <= j
proof
let k be Nat;
A1: SUCC(k,SCM R) = {k, k + 1} by Th34;
hence k+1 in SUCC(k,SCM R) by TARSKI:def 2;
let j be Nat;
assume
A2: j in SUCC(k,SCM R);
per cases by A1,A2,TARSKI:def 2;
suppose
j = k;
hence thesis;
end;
suppose
j = k + 1;
hence thesis by NAT_1:11;
end;
end;
registration
let R;
cluster SCM R -> standard;
coherence
proof
deffunc U(Element of NAT) = $1;
for k being Nat
holds k+1 in SUCC(k,SCM R) &
for j being Nat st j in SUCC(k,SCM R) holds k <= j by Th35;
hence thesis by AMISTD_1:3;
end;
end;
definition
let R be Ring, k be Nat;
func dl.(R,k) -> Data-Location of R equals
dl.k;
coherence
by AMI_2:def 16,AMI_3:27,SCMRING2:1;
end;
registration
let R;
cluster InsCode halt SCM R -> jump-only
for InsType of the InstructionsF of SCM R;
coherence
proof
now
let s be State of SCM R, o be Object of SCM R, I be Instruction of SCM R;
assume that
A1: InsCode I = InsCode halt SCM R and
o in Data-Locations SCM R;
I = halt SCM R by A1,Th11;
hence Exec(I, s).o = s.o by EXTPRO_1:def 3;
end;
hence thesis;
end;
end;
registration
let R;
cluster halt SCM R -> jump-only;
coherence;
end;
registration
let R, i1;
cluster InsCode goto(i1,R) -> jump-only
for InsType of the InstructionsF of SCM R;
coherence
proof
set S = SCM R;
now
let s be State of S, o be Object of S, I be Instruction of S;
assume that
A1: InsCode I = InsCode goto(i1,R) and
A2: o in Data-Locations SCM R;
A3: ex i2 st I = goto(i2,R) by A1,Th17;
o in Data-Locations SCM by A2,SCMRING2:22;
then o is Data-Location of R by SCMRING2:1;
hence Exec(I, s).o = s.o by A3,SCMRING2:15;
end;
hence thesis;
end;
end;
registration
let R, i1;
cluster goto(i1,R) -> jump-only;
coherence;
end;
registration
let R, a, i1;
cluster InsCode (a =0_goto i1) -> jump-only
for InsType of the InstructionsF of SCM R;
coherence
proof
set S = SCM R;
now
let s be State of S, o be Object of S, I be Instruction of S;
assume that
A1: InsCode I = InsCode (a =0_goto i1) and
A2: o in Data-Locations SCM R;
A3: ex b, i2 st I = (b =0_goto i2) by A1,Th18;
o in Data-Locations SCM by A2,SCMRING2:22;
then o is Data-Location of R by SCMRING2:1;
hence Exec(I, s).o = s.o by A3,SCMRING2:16;
end;
hence thesis;
end;
end;
registration
let R, a, i1;
cluster a =0_goto i1 -> jump-only;
coherence;
end;
reserve S for non trivial Ring,
p, q for Data-Location of S,
w for Element of S;
registration
let S, p, q;
cluster InsCode (p:=q) -> non jump-only
for InsType of the InstructionsF of SCM S;
coherence
proof
set w = the State of SCM S;
consider e being Element of S such that
A1: e <> 0.S by STRUCT_0:def 18;
reconsider e as Element of S;
set t = w+*((dl.(S,0), dl.(S,1))-->(0.S,e));
A2: dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) = {dl.(S,0), dl.(S,1)} by FUNCT_4:62;
then
A3: dl.(S,1) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by TARSKI:def 2;
A4: InsCode (p:=q) = 1
.= InsCode (dl.(S,0):=dl.(S,1));
dl.(S,0) in Data-Locations SCM by SCMRING2:1;
then
A5: dl.(S,0) in Data-Locations SCM S by SCMRING2:22;
dl.(S,0) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by A2,TARSKI:def 2;
then
A6: t.dl.(S,0) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,0) by FUNCT_4:13
.= 0.S by AMI_3:10,FUNCT_4:63;
Exec((dl.(S,0):=dl.(S,1)), t).dl.(S,0) = t.dl.(S,1) by SCMRING2:11
.= (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,1) by A3,FUNCT_4:13
.= e by FUNCT_4:63;
hence thesis by A1,A4,A6,A5;
end;
end;
registration
let S, p, q;
cluster p:=q -> non jump-only;
coherence;
end;
registration
let S, p, q;
cluster InsCode AddTo(p,q) -> non jump-only
for InsType of the InstructionsF of SCM S;
coherence
proof
set w = the State of SCM S;
consider e being Element of S such that
A1: e <> 0.S by STRUCT_0:def 18;
reconsider e as Element of S;
set t = w+*((dl.(S,0), dl.(S,1))-->(0.S,e));
A2: dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) = {dl.(S,0), dl.(S,1)} by FUNCT_4:62;
then dl.(S,0) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by TARSKI:def 2;
then
A3: t.dl.(S,0) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,0) by FUNCT_4:13
.= 0.S by AMI_3:10,FUNCT_4:63;
A4: InsCode AddTo(p,q) = 2
.= InsCode AddTo(dl.(S,0), dl.(S,1));
dl.(S,1) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by A2,TARSKI:def 2;
then
A5: t.dl.(S,1) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,1) by FUNCT_4:13
.= e by FUNCT_4:63;
dl.(S,0) in Data-Locations SCM by SCMRING2:1;
then
A6: dl.(S,0) in Data-Locations SCM S by SCMRING2:22;
Exec(AddTo(dl.(S,0), dl.(S,1)), t).dl.(S,0) = t.dl.(S,0) + t.dl.(S,1)
by SCMRING2:12
.= e by A3,A5,RLVECT_1:4;
hence thesis by A1,A4,A3,A6;
end;
end;
registration
let S, p, q;
cluster AddTo(p, q) -> non jump-only;
coherence;
end;
registration
let S, p, q;
cluster InsCode SubFrom(p,q) -> non jump-only
for InsType of the InstructionsF of SCM S;
coherence
proof
set w = the State of SCM S;
consider e being Element of S such that
A1: e <> 0.S by STRUCT_0:def 18;
reconsider e as Element of S;
A2: now
assume -e = 0.S;
then e = -0.S by RLVECT_1:17;
hence contradiction by A1,RLVECT_1:12;
end;
set t = w+*((dl.(S,0), dl.(S,1))-->(0.S,e));
A3: InsCode SubFrom(p,q) = 3
.= InsCode SubFrom(dl.(S,0), dl.(S,1));
A4: dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) = {dl.(S,0), dl.(S,1)} by FUNCT_4:62;
then dl.(S,0) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by TARSKI:def 2;
then
A5: t.dl.(S,0) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,0) by FUNCT_4:13
.= 0.S by AMI_3:10,FUNCT_4:63;
dl.(S,1) in dom ((dl.(S,0), dl.(S,1))-->(0.S,e)) by A4,TARSKI:def 2;
then
A6: t.dl.(S,1) = (dl.(S,0), dl.(S,1))-->(0.S,e).dl.(S,1) by FUNCT_4:13
.= e by FUNCT_4:63;
dl.(S,0) in Data-Locations SCM by SCMRING2:1;
then
A7: dl.(S,0) in Data-Locations SCM S by SCMRING2:22;
Exec(SubFrom(dl.(S,0), dl.(S,1)), t).dl.(S,0) = t.dl.(S,0) - t.dl.(S,
1) by SCMRING2:13
.= -e by A5,A6,RLVECT_1:14;
hence thesis by A3,A5,A2,A7;
end;
end;
registration
let S, p, q;
cluster SubFrom(p, q) -> non jump-only;
coherence;
end;
registration
let S, p, q;
cluster InsCode MultBy(p,q) -> non jump-only
for InsType of the InstructionsF of SCM S;
coherence
proof
IC SCM S = IC SCM by AMI_3:1,SCMRING2:8;
then
A1: 0.S <> 1_S & dl.(S,0) <> IC SCM S by AMI_3:13,LMOD_6:def 1;
set w = the State of SCM S;
set t = w+*((dl.(S,0), dl.(S,1))-->(1_S,0.S));
A2: InsCode MultBy(p,q) = 4
.= InsCode MultBy(dl.(S,0), dl.(S,1));
A3: dom ((dl.(S,0), dl.(S,1))-->(1_S,0.S)) = {dl.(S,0), dl.(S,1)} by FUNCT_4:62
;
then dl.(S,0) in dom ((dl.(S,0), dl.(S,1))-->(1_S,0.S)) by TARSKI:def 2;
then
A4: t.dl.(S,0) = (dl.(S,0), dl.(S,1))-->(1_S,0.S).dl.(S,0) by FUNCT_4:13
.= 1_S by AMI_3:10,FUNCT_4:63;
dl.(S,1) in dom ((dl.(S,0), dl.(S,1))-->(1_S,0.S)) by A3,TARSKI:def 2;
then
A5: t.dl.(S,1) = (dl.(S,0), dl.(S,1))-->(1_S,0.S).dl.(S,1) by FUNCT_4:13
.= 0.S by FUNCT_4:63;
dl.(S,0) in Data-Locations SCM by SCMRING2:1;
then
A6: dl.(S,0) in Data-Locations SCM S by SCMRING2:22;
Exec(MultBy(dl.(S,0), dl.(S,1)), t).dl.(S,0) = t.dl.(S,0) * t.dl.(S,1)
by SCMRING2:14
.= 0.S by A5;
hence thesis by A2,A1,A4,A6;
end;
end;
registration
let S, p, q;
cluster MultBy(p, q) -> non jump-only;
coherence;
end;
registration
let S, p, w;
cluster InsCode (p:=w) -> non jump-only
for InsType of the InstructionsF of SCM S;
coherence
proof
set j = the State of SCM S;
A1: InsCode (p:=w) = 5
.= InsCode (dl.(S,0):=w);
the carrier of S <> {w};
then consider e being object such that
A2: e in the carrier of S and
A3: e <> w by ZFMISC_1:35;
Values dl.(S,0) = the carrier of S by Th1;
then reconsider e as Element of Values dl.(S,0) by A2;
reconsider v = dl.(S,0) .--> e as PartState of SCM S;
set t = j+*v;
dl.(S,0) in dom (dl.(S,0).-->e) by TARSKI:def 1;
then
A4: t.dl.(S,0) = (dl.(S,0) .--> e).dl.(S,0) by FUNCT_4:13
.= e by FUNCOP_1:72;
dl.(S,0) in Data-Locations SCM by SCMRING2:1;
then
A5: dl.(S,0) in Data-Locations SCM S by SCMRING2:22;
Exec((dl.(S,0):=w), t).dl.(S,0) = w by SCMRING2:17;
hence thesis by A3,A1,A4,A5;
end;
end;
registration
let S, p, w;
cluster p:=w -> non jump-only;
coherence;
end;
registration
let R, i1;
cluster goto(i1,R) -> non sequential;
coherence
proof
JUMP goto(i1,R) <> {};
hence thesis by AMISTD_1:13;
end;
end;
registration
let R, a, i1;
cluster a =0_goto i1 -> non sequential;
coherence
proof
JUMP (a =0_goto i1) <> {};
hence thesis by AMISTD_1:13;
end;
end;
registration
let R, i1;
cluster goto(i1,R) -> non ins-loc-free;
coherence;
end;
registration
let R, a, i1;
cluster a =0_goto i1 -> non ins-loc-free;
coherence;
end;
registration
let R;
cluster SCM R -> with_explicit_jumps;
coherence
proof
let I be Instruction of SCM R;
thus JUMP I c= rng JumpPart I
proof
let f be object such that
A1: f in JUMP I;
per cases by SCMRING2:7;
suppose
A2: I = [0,{},{}];
JUMP halt SCM R is empty;
hence thesis by A1,A2;
end;
suppose
ex a,b st I = a:=b;
hence thesis by A1;
end;
suppose
ex a,b st I = AddTo(a,b);
hence thesis by A1;
end;
suppose
ex a,b st I = SubFrom(a,b);
hence thesis by A1;
end;
suppose
ex a,b st I = MultBy(a,b);
hence thesis by A1;
end;
suppose
A3: ex i1 st I = goto(i1,R);
consider i1 such that
A4: I = goto(i1,R) by A3;
rng<*i1*> = {i1} by FINSEQ_1:39;
hence f in rng JumpPart I by A1,A4,Th30;
end;
suppose
A5: ex a,i1 st I = a=0_goto i1;
consider a, i1 such that
A6: I = a=0_goto i1 by A5;
rng<*i1*> = {i1} by FINSEQ_1:39;
hence thesis by A1,A6,Th33;
end;
suppose
ex a,r st I = a:=r;
hence thesis by A1;
end;
end;
let f being object;
assume f in rng JumpPart I;
then consider k being object such that
A7: k in dom JumpPart I and
A8: f = (JumpPart I).k by FUNCT_1:def 3;
per cases by SCMRING2:7;
suppose
I = [0,{},{}];
then I = halt SCM R;
hence thesis by A7;
end;
suppose
ex a,b st I = a:=b;
then consider a, b such that
A9: I = a:=b;
k in dom {} by A7,A9;
hence thesis;
end;
suppose
ex a,b st I = AddTo(a,b);
then consider a, b such that
A10: I = AddTo(a,b);
k in dom {} by A7,A10;
hence thesis;
end;
suppose
ex a,b st I = SubFrom(a,b);
then consider a, b such that
A11: I = SubFrom(a,b);
k in dom {} by A7,A11;
hence thesis;
end;
suppose
ex a,b st I = MultBy(a,b);
then consider a, b such that
A12: I = MultBy(a,b);
k in dom {} by A7,A12;
hence thesis;
end;
suppose
ex i1 st I = goto(i1,R);
then consider i1 such that
A13: I = goto(i1,R);
A14: JumpPart I = <*i1*> by A13;
then k = 1 by A7,Lm1;
then
A15: f = i1 by A14,A8;
JUMP I = {i1} by A13,Th30;
hence thesis by A15,TARSKI:def 1;
end;
suppose
ex a,i1 st I = a=0_goto i1;
then consider a, i1 such that
A16: I = a=0_goto i1;
A17: JumpPart I = <*i1*> by A16;
then k = 1 by A7,Lm1;
then
A18: f = i1 by A17,A8;
JUMP I = {i1} by A16,Th33;
hence thesis by A18,TARSKI:def 1;
end;
suppose
ex a,r st I = a:=r;
then consider a, r such that
A19: I = a:=r;
k in dom {} by A7,A19;
hence thesis;
end;
end;
end;
theorem Th36:
IncAddr(goto(i1,R),k) = goto(i1 + k,R)
proof
A1: JumpPart IncAddr(goto(i1,R),k) = k + JumpPart goto(i1,R)
by COMPOS_0:def 9;
then
A2: dom JumpPart IncAddr(goto(i1,R),k) = dom JumpPart goto(i1,R) by
VALUED_1:def 2;
A3: dom JumpPart goto(i1 + k,R)
= dom <*i1 + k*>
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i1*> by FINSEQ_1:def 8
.= dom JumpPart goto(i1,R);
A4: for x being object st x in dom JumpPart goto(i1,R) holds (JumpPart
IncAddr(goto(i1,R),k)).x = (JumpPart
goto(i1 + k,R)).x
proof
let x be object;
assume
A5: x in dom JumpPart goto(i1,R);
then x in dom <*i1*>;
then
A6: x = 1 by Lm1;
reconsider f = (JumpPart goto(i1,R)).x as Element of NAT
by ORDINAL1:def 12;
A7: (JumpPart IncAddr(goto(i1,R),k)).x = k + f by A5,A1,A2,VALUED_1:def 2;
thus (JumpPart IncAddr(goto(i1,R),k)).x
= <*i1 + k*>.x
by A6,A7
.= (JumpPart goto(i1 + k,R)).x;
end;
A8: InsCode IncAddr(goto(i1,R),k) = InsCode goto(i1,R) by COMPOS_0:def 9
.= 6
.= InsCode goto(i1 + k,R);
A9: AddressPart IncAddr(goto(i1,R),k)
= AddressPart goto(i1,R) by COMPOS_0:def 9
.= {}
.= AddressPart goto(i1 + k,R);
JumpPart IncAddr(goto(i1,R),k) = JumpPart goto(i1 + k,R)
by A2,A3,A4,FUNCT_1:2;
hence thesis by A8,A9,COMPOS_0:1;
end;
theorem Th37:
IncAddr(a=0_goto i1,k) = a=0_goto (i1 + k)
proof
A1: JumpPart IncAddr(a=0_goto i1,k) = k + JumpPart (a=0_goto i1)
by COMPOS_0:def 9;
then
A2: dom JumpPart IncAddr(a=0_goto i1,k) = dom JumpPart (a=0_goto i1)
by VALUED_1:def 2;
A3: dom JumpPart (a=0_goto (i1 + k))
= dom <*i1 + k*>
.= Seg 1 by FINSEQ_1:38
.= dom <*i1*> by FINSEQ_1:38
.= dom JumpPart (a=0_goto i1);
A4: for x being object st x in dom JumpPart (a=0_goto i1) holds (JumpPart
IncAddr(a=0_goto i1,k)).x = (JumpPart (a=0_goto (i1 + k))).x
proof
let x be object;
assume
A5: x in dom JumpPart (a=0_goto i1);
then x in dom <*i1*>;
then
A6: x = 1 by FINSEQ_1:90;
reconsider f = (JumpPart (a=0_goto i1)).x as Element of NAT
by ORDINAL1:def 12;
A7: (JumpPart IncAddr(a=0_goto i1,k)).x = k + f by A5,A1,A2,VALUED_1:def 2;
thus (JumpPart IncAddr(a=0_goto i1,k)).x
= <*i1 + k*>.x by A6,A7
.= (JumpPart (a=0_goto (i1 + k))).x;
end;
A8: InsCode IncAddr(a=0_goto i1,k) = InsCode (a=0_goto i1) by COMPOS_0:def 9
.= 7
.= InsCode (a=0_goto ( i1 + k));
A9: AddressPart IncAddr(a=0_goto i1,k)
= AddressPart (a=0_goto i1) by COMPOS_0:def 9
.= <*a*>
.= AddressPart (a=0_goto ( i1 + k));
JumpPart IncAddr(a=0_goto i1,k) = JumpPart (a=0_goto ( i1 + k))
by A2,A3,A4,FUNCT_1:2;
hence thesis by A8,A9,COMPOS_0:1;
end;
registration
let R;
cluster SCM R -> IC-relocable;
coherence
proof
thus SCM R is IC-relocable
proof
let I be Instruction of SCM R;
per cases by SCMRING2:7;
suppose
I = [0,{},{}];
then I = halt SCM R;
hence thesis;
end;
suppose
ex a,b st I = a:=b;
hence thesis;
end;
suppose
ex a,b st I = AddTo(a,b);
hence thesis;
end;
suppose
ex a,b st I = SubFrom(a,b);
hence thesis;
end;
suppose
ex a,b st I = MultBy(a,b);
hence thesis;
end;
suppose
A1: ex i1 st I = goto(i1,R);
let j,k be Nat, s1 be State of SCM R;
set s2 = IncIC(s1,k);
consider i1 such that
A2: I = goto(i1,R) by A1;
thus IC Exec(IncAddr(I,j),s1) + k
= IC Exec(goto(j+i1,R),s1) + k by A2,Th36
.= j+i1+k by SCMRING2:15
.= IC Exec(goto(j+i1+k,R),s2) by SCMRING2:15
.= IC Exec(goto(j+k+i1,R),s2)
.= IC Exec(IncAddr(I,j+k), s2) by A2,Th36;
end;
suppose
ex a,i1 st I = a=0_goto i1;
then consider a, i1 such that
A3: I = a=0_goto i1;
let j,k be Nat, s1 be State of SCM R;
set s2 = IncIC(s1,k);
a <> IC SCM R & dom (IC SCM R .--> (IC s1 + k)) = {IC SCM R}
by Th2;
then not a in dom (IC SCM R .--> (IC s1 + k)) by TARSKI:def 1;
then
A4: s1.a = s2.a by FUNCT_4:11;
per cases;
suppose
A5: s1.a = 0.R;
thus IC Exec(IncAddr(I,j),s1) + k
= IC Exec(a=0_goto(j+i1),s1) + k by A3,Th37
.= j+i1+k by A5,SCMRING2:16
.= IC Exec(a=0_goto(j+i1+k),s2) by A4,A5,SCMRING2:16
.= IC Exec(a=0_goto(j+k+i1),s2)
.= IC Exec(IncAddr(I,j+k), s2) by A3,Th37;
end;
suppose
A6: s1.a <> 0.R;
A7: IncAddr(I,j) = a=0_goto(i1+j) by A3,Th37;
A8: IncAddr(I,j+k) = a=0_goto(i1+(j+k)) by A3,Th37;
IC SCM R in dom (IC SCM R .--> (IC s1 + k)) by TARSKI:def 1;
then
A9: IC s2 = (IC SCM R .--> (IC s1 + k)).IC SCM R by FUNCT_4:13
.= (IC s1 + k) by FUNCOP_1:72;
thus IC Exec(IncAddr(I,j),s1) + k
= IC s1 + 1 + k by A7,A6,SCMRING2:16
.= IC s1 + 1 + k
.= IC s2 + 1 by A9
.= IC Exec(IncAddr(I,j+k), s2) by A8,A6,A4,SCMRING2:16;
end;
end;
suppose
ex a,r st I = a:=r;
hence thesis;
end;
end;
end;
end;
theorem
InsCode I <= 7
proof
set T = InsCode I;
T = 0 or T = 1 or T = 2 or T = 3 or T = 4 or T = 5 or T = 6 or T = 7 by Lm2;
hence thesis;
end;