:: On the Instructions of { \bf SCM }
:: by Artur Korni{\l}owicz
::
:: Received May 8, 2001
:: Copyright (c) 2001-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, AMI_3, AMI_1, FSM_1, ORDINAL1, CAT_1, XBOOLE_0, FUNCT_1,
RELAT_1, FINSEQ_1, CARD_1, AMISTD_2, GRAPHSP, CARD_3, AMISTD_1, SUBSET_1,
CIRCUIT2, FUNCT_4, FUNCOP_1, SETFAM_1, XXREAL_0, TARSKI, ARYTM_3,
GOBOARD5, FRECHET, ARYTM_1, INT_1, PARTFUN1, NAT_1, COMPOS_1, GOBRD13,
MEMSTR_0;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
CARD_1, ORDINAL1, NUMBERS, XCMPLX_0, INT_1, FUNCOP_1, PARTFUN1, FINSEQ_1,
FUNCT_4, XXREAL_0, VALUED_1, CARD_3, FUNCT_7, MEMSTR_0, COMPOS_0,
COMPOS_1, EXTPRO_1, AMI_3, AMISTD_1, AMISTD_2;
constructors NAT_D, AMI_3, AMISTD_2, RELSET_1, AMISTD_1, PRE_POLY, FUNCT_7,
DOMAIN_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, NAT_1,
INT_1, FINSEQ_1, CARD_3, AMI_3, AMISTD_2, FUNCT_4, VALUED_0, EXTPRO_1,
FUNCT_7, PRE_POLY, MEMSTR_0, CARD_1, COMPOS_0, XTUPLE_0;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, AMISTD_1, AMISTD_2, XBOOLE_0, COMPOS_0;
equalities AMISTD_1, AMI_3, FUNCOP_1, COMPOS_1, EXTPRO_1, MEMSTR_0, COMPOS_0,
XTUPLE_0;
expansions AMISTD_1, XBOOLE_0;
theorems TARSKI, NAT_1, AMI_3, FUNCT_4, AMI_5, FUNCT_1, FUNCOP_1, SETFAM_1,
AMISTD_1, FINSEQ_1, MEMSTR_0, FUNCT_7, CARD_3, XBOOLE_0, XBOOLE_1, NAT_D,
ORDINAL1, PARTFUN1, PBOOLE, VALUED_1, EXTPRO_1, AMI_2, COMPOS_0,
XTUPLE_0;
begin
reserve a, b, d1, d2 for Data-Location,
il, i1, i2 for Nat,
I for Instruction of SCM,
s, s1, s2 for State of SCM,
T for InsType of the InstructionsF of SCM,
k,k1 for Nat;
theorem
T = 0 or ... or T = 8
proof
consider y being object such that
A1: [T,y] in proj1 the InstructionsF of SCM by XTUPLE_0:def 12;
consider x being object such that
A2: [[T,y],x] in the InstructionsF of SCM by A1,XTUPLE_0:def 12;
reconsider I = [T,y,x] as Instruction of SCM by A2;
T = InsCode I;
hence thesis by AMI_5:5;
end;
theorem Th2:
JumpPart halt SCM = {};
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 by A1,A3,AMI_5:7;
hence a in {0} by A2,TARSKI:def 1;
end;
let a be object;
assume a in {0};
then
A4: a = 0 by TARSKI:def 1;
InsCode halt SCM = 0;
hence thesis by A1,Th2,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 such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = a:=b by A1,A3,AMI_5:8;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location;
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 such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = AddTo(a,b) by A1,A3,AMI_5:9;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location;
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 such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = SubFrom(a,b) by A1,A3,AMI_5:10;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location;
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 such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = MultBy(a,b) by A1,A3,AMI_5:11;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location;
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 such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = Divide(a,b) by A1,A3,AMI_5:12;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Data-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart Divide(a,a);
InsCode Divide(a,a) = 5;
hence thesis by A5,A1;
end;
theorem Th9:
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 SCM-goto i1 = 6;
then
A2: JumpPart SCM-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 SCM-goto i1 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 such that
A4: f = JumpPart I and
A5: InsCode I = T;
consider i1 such that
A6: I = SCM-goto i1 by A1,A5,AMI_5:13;
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 Th10:
T = 7 implies dom product" JumpParts T = {1}
proof
set i1 = the Element of NAT,a = the Data-Location;
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 such that
A4: f = JumpPart I and
A5: InsCode I = T;
consider i1, a such that
A6: I = a =0_goto i1 by A1,A5,AMI_5:14;
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 Th11:
T = 8 implies dom product" JumpParts T = {1}
proof
set i1 = the Element of NAT,a = the Data-Location;
assume
A1: T = 8;
hereby
let x be object;
InsCode (a >0_goto i1) = 8;
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 such that
A4: f = JumpPart I and
A5: InsCode I = T;
consider i1, a such that
A6: I = a >0_goto i1 by A1,A5,AMI_5:15;
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 SCM-goto k1).1 = NAT
proof
dom product" JumpParts InsCode SCM-goto k1 = {1}
by Th9;
then
A1: 1 in dom product" JumpParts InsCode SCM-goto k1 by TARSKI:def 1;
hereby
let x be object;
assume x in (product" JumpParts InsCode SCM-goto k1).1;
then x in pi(JumpParts InsCode SCM-goto k1,1) by A1,CARD_3:def 12;
then consider g being Function such that
A2: g in JumpParts InsCode SCM-goto k1 and
A3: x = g.1 by CARD_3:def 6;
consider I being Instruction of SCM such that
A4: g = JumpPart I and
A5: InsCode I = InsCode SCM-goto k1 by A2;
InsCode I = 6 by A5;
then consider i2 such that
A6: I = SCM-goto i2 by AMI_5:13;
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 SCM-goto x = <*x*> & InsCode SCM-goto k1
= InsCode SCM-goto x;
then
A7: <*x*> in JumpParts InsCode SCM-goto k1;
<*x*>.1 = x;
then x in pi(JumpParts InsCode SCM-goto k1,1) by A7,CARD_3:def 6;
hence thesis by A1,CARD_3:def 12;
end;
theorem
(product" JumpParts InsCode (a =0_goto k1)).1 = NAT
proof
dom product" JumpParts InsCode (a =0_goto k1) = {1} by Th10;
then
A1: 1 in dom product" JumpParts InsCode (a =0_goto k1) by TARSKI:def 1;
hereby
let x be object;
assume x in (product" JumpParts InsCode (a =0_goto k1)).1;
then x in pi(JumpParts InsCode (a =0_goto k1),1) by A1,CARD_3:def 12;
then consider g being Function such that
A2: g in JumpParts InsCode (a =0_goto k1) and
A3: x = g.1 by CARD_3:def 6;
consider I being Instruction of SCM such that
A4: g = JumpPart I and
A5: InsCode I = InsCode (a =0_goto k1) by A2;
InsCode I = 7 by A5;
then consider i2, b such that
A6: I = b =0_goto i2 by AMI_5:14;
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 k1) = InsCode
(a =0_goto x);
then
A7: <*x*> in JumpParts InsCode (a =0_goto k1);
<*x*>.1 = x;
then x in pi(JumpParts InsCode (a =0_goto k1),1) by A7,CARD_3:def 6;
hence thesis by A1,CARD_3:def 12;
end;
theorem
(product" JumpParts InsCode (a >0_goto k1)).1 = NAT
proof
dom product" JumpParts InsCode (a >0_goto k1) = {1} by Th11;
then
A1: 1 in dom product" JumpParts InsCode (a >0_goto k1) by TARSKI:def 1;
hereby
let x be object;
assume x in (product" JumpParts InsCode (a >0_goto k1)).1;
then x in pi(JumpParts InsCode (a >0_goto k1),1) by A1,CARD_3:def 12;
then consider g being Function such that
A2: g in JumpParts InsCode (a >0_goto k1) and
A3: x = g.1 by CARD_3:def 6;
consider I being Instruction of SCM such that
A4: g = JumpPart I and
A5: InsCode I = InsCode (a >0_goto k1) by A2;
InsCode I = 8 by A5;
then consider i2, b such that
A6: I = b >0_goto i2 by AMI_5:15;
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 k1) = InsCode
(a >0_goto x);
then
A7: <*x*> in JumpParts InsCode (a >0_goto k1);
<*x*>.1 = x;
then x in pi(JumpParts InsCode (a >0_goto k1),1) by A7,CARD_3:def 6;
hence thesis by A1,CARD_3:def 12;
end;
Lm1: for i being Instruction of SCM 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;
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 {succ p} in X;
then x in {succ p} by A2,SETFAM_1:def 1;
then
A3: x = succ p by TARSKI:def 1;
NIC(i,q) = {q+1} by A1;
then {succ q} in X;
then x in {succ q} by A2,SETFAM_1:def 1;
hence contradiction by A3,TARSKI:def 1;
end;
registration
cluster JUMP halt SCM -> empty;
coherence;
end;
registration
let a, b;
cluster a:=b -> sequential;
coherence
by AMI_3:2;
cluster AddTo(a,b) -> sequential;
coherence
by AMI_3:3;
cluster SubFrom(a,b) -> sequential;
coherence
by AMI_3:4;
cluster MultBy(a,b) -> sequential;
coherence
by AMI_3:5;
cluster Divide(a,b) -> sequential;
coherence
by AMI_3:6;
end;
registration
let 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 Lm1;
end;
end;
registration
let 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 Lm1;
end;
end;
registration
let 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 Lm1;
end;
end;
registration
let 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 Lm1;
end;
end;
registration
let a, b;
cluster JUMP Divide(a,b) -> empty;
coherence
proof
for l being Element of NAT holds NIC(Divide(a,b),l)={l+1} by AMISTD_1:12;
hence thesis by Lm1;
end;
end;
theorem Th15:
NIC(SCM-goto k, il) = {k}
proof
now
let x be object;
A1: now
il in NAT by ORDINAL1:def 12;
then reconsider il1 = il as Element of Values IC SCM by MEMSTR_0:def 6;
set I = SCM-goto k;
set t = the State of SCM,
Q = the Instruction-Sequence of SCM;
assume
A2: x = k;
reconsider n = il as Element of NAT by ORDINAL1:def 12;
reconsider u = t+*(IC SCM,il1)
as Element of product the_Values_of SCM by CARD_3:107;
reconsider P = Q +* (il,I)
as Instruction-Sequence of SCM;
reconsider ill=il as Element of NAT by ORDINAL1:def 12;
A3: P/.ill = P.ill by PBOOLE:143;
IC SCM in dom t by MEMSTR_0:2;
then
A4: IC u = n by FUNCT_7:31;
il in NAT by ORDINAL1:def 12;
then il in dom Q by PARTFUN1:def 2;
then
A5: P.n = I by FUNCT_7:31;
then IC Following(P,u) = k by A3,A4,AMI_3:7;
hence x in {IC Exec(SCM-goto k,s)
where s is Element of product the_Values_of SCM
: IC s = il} by A2,A4,A3,A5;
end;
now
assume x in {IC Exec(SCM-goto k,s)
where s is Element of product the_Values_of SCM
: IC s = il};
then ex s being Element of product the_Values_of SCM
st x = IC Exec(SCM-goto k,s) & IC s = il;
hence x = k by AMI_3:7;
end;
hence
x in {k} iff x in {IC Exec(SCM-goto k,s)
where s is Element of product the_Values_of SCM
: IC s = il} by A1,TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem Th16:
JUMP SCM-goto k = {k}
proof
set X = the set of all NIC(SCM-goto k, il) ;
now
let x be object;
hereby
set il1 = 1;
A1: NIC(SCM-goto k, il1) in X;
assume x in meet X;
then x in NIC(SCM-goto k, il1) by A1,SETFAM_1:def 1;
hence x in {k} by Th15;
end;
assume x in {k};
then
A2: x = k by TARSKI:def 1;
A3: now
let Y be set;
assume Y in X;
then consider il being Nat such that
A4: Y = NIC(SCM-goto k, il);
NIC(SCM-goto k, il) = {k} by Th15;
hence k in Y by A4,TARSKI:def 1;
end;
reconsider k as Element of NAT by ORDINAL1:def 12;
NIC(SCM-goto k, k) in X;
hence x in meet X by A2,A3,SETFAM_1:def 1;
end;
hence thesis by TARSKI:2;
end;
registration
let i1;
cluster JUMP SCM-goto i1 -> 1-element;
coherence
proof
JUMP SCM-goto i1 = {i1} by Th16;
hence thesis;
end;
end;
theorem Th17:
NIC(a=0_goto k, il) = {k, il+1}
proof
set t = the State of SCM,
Q = the Instruction-Sequence of SCM;
hereby
let x be object;
assume x in NIC(a=0_goto k, il);
then consider s being Element of product the_Values_of SCM
such that
A1: x = IC Exec(a=0_goto k,s) & IC s = il;
per cases;
suppose
s.a = 0;
then x = k by A1,AMI_3:8;
hence x in {k, il+1} by TARSKI:def 2;
end;
suppose
s.a <> 0;
then x = il + 1 by A1,AMI_3:8;
hence x in {k, il+1} by TARSKI:def 2;
end;
end;
let x be object;
set I = a=0_goto k;
A2: IC SCM <> a by AMI_5:2;
reconsider n = il as Element of NAT by ORDINAL1:def 12;
reconsider il1 = n as Element of Values IC SCM by MEMSTR_0:def 6;
reconsider u = t+*(IC SCM,il1)
as Element of product the_Values_of SCM by CARD_3:107;
reconsider P = Q +* (il,I)
as Instruction-Sequence of SCM;
assume
A3: x in {k,il+1};
per cases by A3,TARSKI:def 2;
suppose
A4: x = k;
reconsider v = u+*(a .--> 0)
as Element of product the_Values_of SCM by CARD_3:107;
A5: IC SCM in dom t by MEMSTR_0:2;
not IC SCM in dom (a .--> 0) by A2,TARSKI:def 1;
then
A7: IC v = IC u by FUNCT_4:11
.= n by A5,FUNCT_7:31;
reconsider il as Element of NAT by ORDINAL1:def 12;
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 .--> 0) by TARSKI:def 1;
then
v.a = (a .--> 0).a by FUNCT_4:13
.= 0 by FUNCOP_1:72;
then IC Following(P,v) = k by A7,A9,A8,AMI_3:8;
hence thesis by A4,A7,A9,A8;
end;
suppose
A10: x = il+1;
reconsider v = u+*(a .--> 1)
as Element of product the_Values_of SCM by CARD_3:107;
A11: IC SCM in dom t by MEMSTR_0:2;
not IC SCM in dom (a .--> 1) by A2,TARSKI:def 1;
then
A13: IC v = IC u by FUNCT_4:11
.= n by A11,FUNCT_7:31;
reconsider il as Element of NAT by ORDINAL1:def 12;
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 .--> 1) by TARSKI:def 1;
then v.a = (a .--> 1).a by FUNCT_4:13
.= 1 by FUNCOP_1:72;
then IC Following(P,v) = il+1 by A13,A15,A14,AMI_3:8;
hence thesis by A10,A13,A15,A14;
end;
end;
theorem Th18:
JUMP (a=0_goto k) = {k}
proof
set X = the set of all NIC(a=0_goto k, il) ;
now
let x be object;
A1: now
let Y be set;
assume Y in X;
then consider il being Nat such that
A2: Y = NIC(a=0_goto k, il);
NIC(a=0_goto k, il) = {k, il+1} by Th17;
hence k in Y by A2,TARSKI:def 2;
end;
hereby
set il1 = 1, il2 = 2;
assume
A3: x in meet X;
A4: NIC(a=0_goto k, il2) = {k, il2+1} by Th17;
NIC(a=0_goto k, il2) in X;
then x in NIC(a=0_goto k, il2) by A3,SETFAM_1:def 1;
then
A5: x = k or x = il2+1 by A4,TARSKI:def 2;
A6: NIC(a=0_goto k, il1) = {k, il1+1} by Th17;
NIC(a=0_goto k, il1) in X;
then x in NIC(a=0_goto k, il1) by A3,SETFAM_1:def 1;
then x = k or x = il1+1 by A6,TARSKI:def 2;
hence x in {k} by A5,TARSKI:def 1;
end;
assume x in {k};
then
A7: x = k by TARSKI:def 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
NIC(a=0_goto k, k) in X;
hence x in meet X by A7,A1,SETFAM_1:def 1;
end;
hence thesis by TARSKI:2;
end;
registration
let a, i1;
cluster JUMP (a =0_goto i1) -> 1-element;
coherence
proof
JUMP (a =0_goto i1) = {i1} by Th18;
hence thesis;
end;
end;
theorem Th19:
NIC(a>0_goto k, il) = {k, il+1}
proof
set t = the State of SCM,
Q = the Instruction-Sequence of SCM;
hereby
let x be object;
assume x in NIC(a>0_goto k, il);
then consider s being Element of product the_Values_of SCM
such that
A1: x = IC Exec(a>0_goto k,s) & IC s = il;
per cases;
suppose
s.a > 0;
then x = k by A1,AMI_3:9;
hence x in {k, il+1} by TARSKI:def 2;
end;
suppose
s.a <= 0;
then x = il+1 by A1,AMI_3:9;
hence x in {k, il+1} by TARSKI:def 2;
end;
end;
let x be object;
set I = a>0_goto k;
A2: IC SCM <> a by AMI_5:2;
assume
A3: x in {k,il+1};
reconsider n = il as Element of NAT by ORDINAL1:def 12;
reconsider il1 = n as Element of Values IC SCM by MEMSTR_0:def 6;
reconsider u = t+*(IC SCM,il1)
as Element of product the_Values_of SCM by CARD_3:107;
reconsider P = Q +* (il,I)
as Instruction-Sequence of SCM;
per cases by A3,TARSKI:def 2;
suppose
A4: x = k;
reconsider v = u+*(a .--> 1)
as Element of product the_Values_of SCM by CARD_3:107;
A5: IC SCM in dom t by MEMSTR_0:2;
not IC SCM in dom (a .--> 1) by A2,TARSKI:def 1;
then
A7: IC v = IC u by FUNCT_4:11
.= n by A5,FUNCT_7:31;
reconsider il as Element of NAT by ORDINAL1:def 12;
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 .--> 1) by TARSKI:def 1;
then v.a = (a .--> 1).a by FUNCT_4:13
.= 1 by FUNCOP_1:72;
then IC Following(P,v) = k by A7,A9,A8,AMI_3:9;
hence thesis by A4,A7,A9,A8;
end;
suppose
A10: x = il+1;
reconsider v = u+*(a .--> 0)
as Element of product the_Values_of SCM by CARD_3:107;
A11: IC SCM in dom t by MEMSTR_0:2;
not IC SCM in dom (a .--> 0) by A2,TARSKI:def 1;
then
A13: IC v = IC u by FUNCT_4:11
.= n by A11,FUNCT_7:31;
reconsider il as Element of NAT by ORDINAL1:def 12;
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 .--> 0) by TARSKI:def 1;
then v.a = (a .--> 0).a by FUNCT_4:13
.= 0 by FUNCOP_1:72;
then IC Following(P,v) = il+1 by A13,A15,A14,AMI_3:9;
hence thesis by A10,A13,A15,A14;
end;
end;
theorem Th20:
JUMP (a>0_goto k) = {k}
proof
set X = the set of all NIC(a>0_goto k, il) ;
now
let x be object;
A1: now
let Y be set;
assume Y in X;
then consider il being Nat such that
A2: Y = NIC(a>0_goto k, il);
NIC(a>0_goto k, il) = {k, il+1} by Th19;
hence k in Y by A2,TARSKI:def 2;
end;
hereby
set il1 = 1, il2 = 2;
assume
A3: x in meet X;
A4: NIC(a>0_goto k, il2) = {k, il2+1} by Th19;
NIC(a>0_goto k, il2) in X;
then x in NIC(a>0_goto k, il2) by A3,SETFAM_1:def 1;
then
A5: x = k or x = il2+1 by A4,TARSKI:def 2;
A6: NIC(a>0_goto k, il1) = {k, il1+1} by Th19;
NIC(a>0_goto k, il1) in X;
then x in NIC(a>0_goto k, il1) by A3,SETFAM_1:def 1;
then x = k or x = il1+1 by A6,TARSKI:def 2;
hence x in {k} by A5,TARSKI:def 1;
end;
assume x in {k};
then
A7: x = k by TARSKI:def 1;
reconsider k as Element of NAT by ORDINAL1:def 12;
NIC(a>0_goto k, k) in X;
hence x in meet X by A7,A1,SETFAM_1:def 1;
end;
hence thesis by TARSKI:2;
end;
registration
let a, i1;
cluster JUMP (a >0_goto i1) -> 1-element;
coherence
proof
JUMP (a >0_goto i1) = {i1} by Th20;
hence thesis;
end;
end;
theorem Th21:
SUCC(il,SCM) = {il, il+1}
proof
set X = the set of all
NIC(I, il) \ JUMP I where I is Element of the InstructionsF of SCM;
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 such that
A3: Y = NIC(i, il) \ JUMP i by A2;
per cases by AMI_3:24;
suppose
i = [0,{},{}];
then x in {il} \ JUMP halt SCM 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 a,b st i = Divide(a,b);
then consider a, b such that
A8: i = Divide(a,b);
x in {il+1} \ JUMP Divide(a,b) by A1,A3,A8,AMISTD_1:12;
then x = il+1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex k st i = SCM-goto k;
then consider k such that
A9: i = SCM-goto k;
x in {k} \ JUMP i by A1,A3,A9,Th15;
then x in {k} \ {k} by A9,Th16;
hence x in N by XBOOLE_1:37;
end;
suppose
ex a,k st i = a=0_goto k;
then consider a, k such that
A10: i = a=0_goto k;
A11: NIC(i, il) = {k, il+1} by A10,Th17;
x in NIC(i, il) by A1,A3,XBOOLE_0:def 5;
then
A12: x = k or x = il+1 by A11,TARSKI:def 2;
x in NIC(i, il) \ {k} by A1,A3,A10,Th18;
then not x in {k} by XBOOLE_0:def 5;
hence x in N by A12,TARSKI:def 1,def 2;
end;
suppose
ex a,k st i = a>0_goto k;
then consider a, k such that
A13: i = a>0_goto k;
A14: NIC(i, il) = {k, il+1} by A13,Th19;
x in NIC(i, il) by A1,A3,XBOOLE_0:def 5;
then
A15: x = k or x = il+1 by A14,TARSKI:def 2;
x in NIC(i, il) \ {k} by A1,A3,A13,Th20;
then not x in {k} by XBOOLE_0:def 5;
hence x in N by A15,TARSKI:def 1,def 2;
end;
end;
assume
A16: x in {il, il+1};
per cases by A16,TARSKI:def 2;
suppose
A17: x = il;
set i = halt SCM;
NIC(i, il) \ JUMP i = {il} by AMISTD_1:2;
then
A18: {il} in X;
x in {il} by A17,TARSKI:def 1;
hence x in union X by A18,TARSKI:def 4;
end;
suppose
A19: x = il+1;
set a = the Data-Location;
set i = AddTo(a,a);
NIC(i, il) \ JUMP i = {il+1} by AMISTD_1:12;
then
A20: {il+1} in X;
x in {il+1} by A19,TARSKI:def 1;
hence x in union X by A20,TARSKI:def 4;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th22:
for k being Nat holds k+1 in SUCC(k,SCM) &
for j being Nat st j in SUCC(k,SCM) holds k <= j
proof
let k be Nat;
reconsider fk = k as Element of NAT by ORDINAL1:def 12;
A1: SUCC(k,SCM) = {k, fk+1} by Th21;
hence k+1 in SUCC(k,SCM) by TARSKI:def 2;
let j be Nat;
assume
A2: j in SUCC(k,SCM);
reconsider fk = k as Element of NAT by ORDINAL1:def 12;
per cases by A1,A2,TARSKI:def 2;
suppose
j = k;
hence thesis;
end;
suppose
j = fk + 1;
hence thesis by NAT_1:11;
end;
end;
registration
cluster SCM -> standard;
coherence by Th22,AMISTD_1:3;
end;
registration
cluster InsCode halt SCM -> jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
now
let s be State of SCM, o be Object of SCM, I be Instruction of SCM;
assume that
A1: InsCode I = InsCode halt SCM and
o in Data-Locations SCM;
I = halt SCM by A1,AMI_5:7;
hence Exec(I, s).o = s.o by EXTPRO_1:def 3;
end;
hence thesis;
end;
end;
registration
cluster halt SCM -> jump-only;
coherence;
end;
registration
let i1;
cluster InsCode SCM-goto i1 -> jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
let T be InsType of the InstructionsF of SCM such that
A1: T = InsCode SCM-goto i1;
let s be State of SCM, o be Object of SCM, I be Instruction of SCM;
assume that
A2: InsCode I = T and
A3: o in Data-Locations SCM;
InsCode I = 6 by A2,A1;
then
A4: ex i2 st I = SCM-goto i2 by AMI_5:13;
o is Data-Location by A3,AMI_2:def 16,AMI_3:27;
hence Exec(I, s).o = s.o by A4,AMI_3:7;
end;
end;
registration
let i1;
cluster SCM-goto i1 -> jump-only non sequential non ins-loc-free;
coherence
proof
thus InsCode SCM-goto i1 is jump-only;
JUMP SCM-goto i1 <> {};
hence SCM-goto i1 is non sequential by AMISTD_1:13;
thus JumpPart SCM-goto i1 is not empty;
end;
end;
registration
let a, i1;
cluster InsCode (a =0_goto i1) -> jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
set S = SCM;
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;
InsCode I = 7 by A1;
then
A3: ex i2, b st I = (b =0_goto i2) by AMI_5:14;
o is Data-Location by A2,AMI_2:def 16,AMI_3:27;
hence Exec(I, s).o = s.o by A3,AMI_3:8;
end;
hence thesis;
end;
cluster InsCode (a >0_goto i1) -> jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
set S = SCM;
now
let s be State of S, o be Object of S, I be Instruction of S;
assume that
A4: InsCode I = InsCode (a >0_goto i1) and
A5: o in Data-Locations SCM;
InsCode I = 8 by A4;
then
A6: ex i2, b st I = (b >0_goto i2) by AMI_5:15;
o is Data-Location by A5,AMI_2:def 16,AMI_3:27;
hence Exec(I, s).o = s.o by A6,AMI_3:9;
end;
hence thesis;
end;
end;
registration
let a, i1;
cluster a =0_goto i1 -> jump-only non sequential non ins-loc-free;
coherence
proof
thus InsCode (a =0_goto i1) is jump-only;
JUMP (a =0_goto i1) <> {};
hence a =0_goto i1 is non sequential by AMISTD_1:13;
thus JumpPart(a =0_goto i1) is not empty;
end;
cluster a >0_goto i1 -> jump-only non sequential non ins-loc-free;
coherence
proof
thus InsCode (a >0_goto i1) is jump-only;
JUMP (a >0_goto i1) <> {};
hence a >0_goto i1 is non sequential by AMISTD_1:13;
thus JumpPart(a >0_goto i1) is not empty;
end;
end;
Lm2: dl.0 <> dl.1 by AMI_3:10;
registration
let a, b;
cluster InsCode (a:=b) -> non jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
set w = the State of SCM;
set t = w+*((dl.0, dl.1)-->(0,1));
A1: InsCode (a:=b) = 1
.= InsCode (dl.0:=dl.1);
A2: dl.0 in Data-Locations SCM by AMI_3:28;
A3: dom ((dl.0, dl.1)-->(0,1)) = {dl.0, dl.1} by FUNCT_4:62;
then
A4: dl.1 in dom ((dl.0, dl.1)-->(0,1)) by TARSKI:def 2;
dl.0 in dom ((dl.0, dl.1)-->(0,1)) by A3,TARSKI:def 2;
then
A5: t.dl.0 = (dl.0, dl.1)-->(0,1).dl.0 by FUNCT_4:13
.= 0 by AMI_3:10,FUNCT_4:63;
Exec((dl.0:=dl.1), t).dl.0 = t.dl.1 by AMI_3:2
.= (dl.0, dl.1)-->(0,1).dl.1 by A4,FUNCT_4:13
.= 1 by FUNCT_4:63;
hence thesis by A1,A2,A5;
end;
cluster InsCode AddTo(a,b) -> non jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
set w = the State of SCM;
set t = w+*((dl.0, dl.1)-->(0,1));
A6: InsCode AddTo(a,b) = 2
.= InsCode AddTo(dl.0, dl.1);
A7: dom ((dl.0, dl.1)-->(0,1)) = {dl.0, dl.1} by FUNCT_4:62;
then dl.0 in dom ((dl.0, dl.1)-->(0,1)) by TARSKI:def 2;
then
A8: t.dl.0 = (dl.0, dl.1)-->(0,1).dl.0 by FUNCT_4:13
.= 0 by AMI_3:10,FUNCT_4:63;
A9: dl.0 in Data-Locations SCM by AMI_3:28;
dl.1 in dom ((dl.0, dl.1)-->(0,1)) by A7,TARSKI:def 2;
then t.dl.1 = (dl.0, dl.1)-->(0,1).dl.1 by FUNCT_4:13
.= 1 by FUNCT_4:63;
then dl.0 <> IC SCM &
Exec(AddTo(dl.0, dl.1), t).dl.0 = (0 qua Nat)+1 by A8,AMI_3:3,13;
hence thesis by A6,A8,A9;
end;
cluster InsCode SubFrom(a,b) -> non jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
set w = the State of SCM;
set t = w+*((dl.0, dl.1)-->(0,1));
A10: InsCode SubFrom(a,b) = 3
.= InsCode SubFrom(dl.0, dl.1);
A11: dom ((dl.0, dl.1)-->(0,1)) = {dl.0, dl.1} by FUNCT_4:62;
then dl.0 in dom ((dl.0, dl.1)-->(0,1)) by TARSKI:def 2;
then
A12: t.dl.0 = (dl.0, dl.1)-->(0,1).dl.0 by FUNCT_4:13
.= 0 by AMI_3:10,FUNCT_4:63;
A13: dl.0 in Data-Locations SCM by AMI_3:28;
dl.1 in dom ((dl.0, dl.1)-->(0,1)) by A11,TARSKI:def 2;
then
A14: t.dl.1 = (dl.0, dl.1)-->(0,1).dl.1 by FUNCT_4:13
.= 1 by FUNCT_4:63;
Exec(SubFrom(dl.0, dl.1), t).dl.0 = t.dl.0 - t.dl.1 by AMI_3:4
.= -1 by A12,A14;
hence thesis by A10,A12,A13;
end;
cluster InsCode MultBy(a,b) -> non jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
set w = the State of SCM;
set t = w+*((dl.0, dl.1)-->(1,0));
A15: InsCode MultBy(a,b) = 4
.= InsCode MultBy(dl.0, dl.1);
A16: dom ((dl.0, dl.1)-->(1,0)) = {dl.0, dl.1} by FUNCT_4:62;
then dl.0 in dom ((dl.0, dl.1)-->(1,0)) by TARSKI:def 2;
then
A17: t.dl.0 = (dl.0, dl.1)-->(1,0).dl.0 by FUNCT_4:13
.= 1 by AMI_3:10,FUNCT_4:63;
A18: dl.0 in Data-Locations SCM by AMI_3:28;
dl.1 in dom ((dl.0, dl.1)-->(1,0)) by A16,TARSKI:def 2;
then
A19: t.dl.1 = (dl.0, dl.1)-->(1,0).dl.1 by FUNCT_4:13
.= 0 by FUNCT_4:63;
Exec(MultBy(dl.0, dl.1), t).dl.0 = t.dl.0 * t.dl.1 by AMI_3:5
.= 0 by A19;
hence thesis by A15,A17,A18;
end;
cluster InsCode Divide(a,b) -> non jump-only
for InsType of the InstructionsF of SCM;
coherence
proof
set w = the State of SCM;
set t = w+*((dl.0, dl.1)-->(7,3));
A20: InsCode Divide(a,b) = 5
.= InsCode Divide(dl.0, dl.1);
A21: dom ((dl.0, dl.1)-->(7,3)) = {dl.0, dl.1} by FUNCT_4:62;
then dl.0 in dom ((dl.0, dl.1)-->(7,3)) by TARSKI:def 2;
then
A22: t.dl.0 = (dl.0, dl.1)-->(7,3).dl.0 by FUNCT_4:13
.= 7 by AMI_3:10,FUNCT_4:63;
A23: 7 = 2 * 3 + 1;
A24: dl.0 in Data-Locations SCM by AMI_3:28;
dl.1 in dom ((dl.0, dl.1)-->(7,3)) by A21,TARSKI:def 2;
then t.dl.1 = (dl.0, dl.1)-->(7,3).dl.1 by FUNCT_4:13
.= 3 by FUNCT_4:63;
then Exec(Divide(dl.0, dl.1), t).dl.0 = 7 div (3 qua Element of NAT) by A22
,Lm2,AMI_3:6
.= 2 by A23,NAT_D:def 1;
hence thesis by A20,A22,A24;
end;
end;
registration
let a, b;
cluster a:=b -> non jump-only;
coherence;
cluster AddTo(a,b) -> non jump-only;
coherence;
cluster SubFrom(a,b) -> non jump-only;
coherence;
cluster MultBy(a,b) -> non jump-only;
coherence;
cluster Divide(a,b) -> non jump-only;
coherence;
end;
registration
cluster SCM -> with_explicit_jumps;
coherence
proof
let I be Instruction of SCM;
thus JUMP I c= rng JumpPart I
proof
let f be object such that
A1: f in JUMP I;
per cases by AMI_3:24;
suppose
I = [0,{},{}];
hence thesis by A1,AMI_3:26;
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
ex a,b st I = Divide(a,b);
hence thesis by A1;
end;
suppose
A2: ex k st I = SCM-goto k;
consider k1 such that
A3: I = SCM-goto k1 by A2;
A4: rng<*k1*> = {k1} by FINSEQ_1:39;
JUMP SCM-goto k1 = {k1} by Th16;
hence thesis by A1,A3,A4;
end;
suppose
A5: ex a,k1 st I = a=0_goto k1;
consider a, k1 such that
A6: I = a=0_goto k1 by A5;
A7: rng<*k1*> = {k1} by FINSEQ_1:39;
JUMP (a=0_goto k1) = {k1} by Th18;
hence thesis by A1,A6,A7;
end;
suppose
A8: ex a,k1 st I = a>0_goto k1;
consider a, k1 such that
A9: I = a>0_goto k1 by A8;
A10: rng<*k1*> = {k1} by FINSEQ_1:39;
JUMP (a>0_goto k1) = {k1} by Th20;
hence thesis by A1,A9,A10;
end;
end;
let f being object;
assume f in rng JumpPart I;
then consider k being object such that
A11: k in dom JumpPart I and
A12: f = (JumpPart I).k by FUNCT_1:def 3;
per cases by AMI_3:24;
suppose
I = [0,{},{}];
then dom JumpPart I = dom {};
hence thesis by A11;
end;
suppose
ex a,b st I = a:=b;
then consider a, b such that
A13: I = a:=b;
k in dom {} by A11,A13;
hence thesis;
end;
suppose
ex a,b st I = AddTo(a,b);
then consider a, b such that
A14: I = AddTo(a,b);
k in dom {} by A11,A14;
hence thesis;
end;
suppose
ex a,b st I = SubFrom(a,b);
then consider a, b such that
A15: I = SubFrom(a,b);
k in dom {} by A11,A15;
hence thesis;
end;
suppose
ex a,b st I = MultBy(a,b);
then consider a, b such that
A16: I = MultBy(a,b);
k in dom {} by A11,A16;
hence thesis;
end;
suppose
ex a,b st I = Divide(a,b);
then consider a, b such that
A17: I = Divide(a,b);
k in dom {} by A11,A17;
hence thesis;
end;
suppose
ex k st I = SCM-goto k;
then consider k1 such that
A18: I = SCM-goto k1;
A19: JumpPart I = <*k1*> by A18;
then k = 1 by A11,FINSEQ_1:90;
then
A20: f = k1 by A19,A12;
JUMP I = {k1} by A18,Th16;
hence thesis by A20,TARSKI:def 1;
end;
suppose
ex a,k st I = a=0_goto k;
then consider a, k1 such that
A21: I = a=0_goto k1;
A22: JumpPart I = <*k1*> by A21;
then k = 1 by A11,FINSEQ_1:90;
then
A23: f = k1 by A22,A12;
JUMP I = {k1} by A21,Th18;
hence thesis by A23,TARSKI:def 1;
end;
suppose
ex a,k1 st I = a>0_goto k1;
then consider a, k1 such that
A24: I = a>0_goto k1;
A25: JumpPart I = <*k1*> by A24;
then k = 1 by A11,FINSEQ_1:90;
then
A26: f = k1 by A25,A12;
JUMP I = {k1} by A24,Th20;
hence thesis by A26,TARSKI:def 1;
end;
end;
end;
theorem Th23:
IncAddr(SCM-goto i1,k) = SCM-goto(i1+k)
proof
A1: JumpPart IncAddr(SCM-goto i1,k) = k + JumpPart SCM-goto i1
by COMPOS_0:def 9;
then
A2: dom JumpPart IncAddr(SCM-goto i1,k) = dom JumpPart SCM-goto i1
by VALUED_1:def 2;
A3: dom JumpPart SCM-goto(i1+k)
= dom <*i1+k*>
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i1*> by FINSEQ_1:def 8
.= dom JumpPart SCM-goto i1;
A4: for x being object st x in dom JumpPart SCM-goto i1 holds (JumpPart
IncAddr(SCM-goto i1,k)).x = (JumpPart SCM-goto(i1+k)).x
proof
let x be object;
assume
A5: x in dom JumpPart SCM-goto i1;
then x in dom <*i1*>;
then
A6: x = 1 by FINSEQ_1:90;
set f = (JumpPart SCM-goto i1).x;
A7: (JumpPart IncAddr(SCM-goto i1,k)).x = k + f by A5,A2,A1,VALUED_1:def 2;
thus
(JumpPart IncAddr(SCM-goto i1,k)).x = <*i1+k*>.x
by A6,A7
.= (JumpPart SCM-goto(i1+k)).x;
end;
A8: AddressPart IncAddr(SCM-goto i1,k) = AddressPart SCM-goto i1
by COMPOS_0:def 9
.= {}
.= AddressPart SCM-goto(i1+k);
A9: InsCode IncAddr(SCM-goto i1,k) = InsCode SCM-goto i1 by COMPOS_0:def 9
.= 6
.= InsCode SCM-goto(i1+k);
JumpPart IncAddr(SCM-goto i1,k) = JumpPart SCM-goto(i1+k)
by A2,A3,A4,FUNCT_1:2;
hence thesis by A8,A9,COMPOS_0:1;
end;
theorem Th24:
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;
set f = (JumpPart (a=0_goto i1)).x;
A7: (JumpPart IncAddr(a=0_goto i1,k)).x = k + f by A1,A2,A5,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: AddressPart IncAddr(a=0_goto i1,k) = AddressPart (a=0_goto i1)
by COMPOS_0:def 9
.= <*a*>
.= AddressPart (a=0_goto(i1+k));
A9: InsCode IncAddr(a=0_goto i1,k) = InsCode (a=0_goto i1) by COMPOS_0:def 9
.= 7
.= InsCode (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;
theorem Th25:
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;
set f = (JumpPart (a>0_goto i1)).x;
A7: (JumpPart IncAddr(a>0_goto i1,k)).x = k + f by A1,A2,A5,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: AddressPart IncAddr(a>0_goto i1,k) = AddressPart (a>0_goto i1)
by COMPOS_0:def 9
.= <*a*>
.= AddressPart (a>0_goto(i1+k));
A9: InsCode IncAddr(a>0_goto i1,k) = InsCode (a>0_goto i1) by COMPOS_0:def 9
.= 8
.= InsCode (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
cluster SCM -> IC-relocable;
coherence
proof
thus SCM is IC-relocable
proof
let I be Instruction of SCM;
per cases by AMI_3:24;
suppose
I = [0,{},{}];
hence thesis by AMI_3:26;
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
ex a,b st I = Divide(a,b);
hence thesis;
end;
suppose
A1: ex k st I = SCM-goto k;
let j,k be Nat, s1 be State of SCM;
set s2 = IncIC(s1,k);
consider k1 such that
A2: I = SCM-goto k1 by A1;
reconsider i1=k1 as Element of NAT by ORDINAL1:def 12;
thus IC Exec(IncAddr(I,j),s1) + k
= IC Exec(SCM-goto(j+k1),s1) + k by A2,Th23
.= j+k1+k by AMI_3:7
.= IC Exec(SCM-goto(j+i1+k),s2) by AMI_3:7
.= IC Exec(SCM-goto(j+k+i1),s2)
.= IC Exec(IncAddr(I,j+k), s2) by A2,Th23;
end;
suppose
ex a,k st I = a=0_goto k;
then consider a, k1 such that
A3: I = a=0_goto k1;
reconsider i1=k1 as Element of NAT by ORDINAL1:def 12;
let j,k be Nat, s1 be State of SCM;
set s2 = IncIC(s1,k);
a <> IC SCM & dom (IC SCM .--> (IC s1 + k)) = {IC SCM}
by AMI_5:2;
then not a in dom (IC SCM .--> (IC s1 + k)) by TARSKI:def 1;
then
A4: s1.a = s2.a by FUNCT_4:11;
now
per cases;
suppose
A5: s1.a = 0;
thus IC Exec(IncAddr(I,j),s1) + k
= IC Exec(a=0_goto(j+k1),s1) + k by A3,Th24
.= j+k1+k by A5,AMI_3:8
.= IC Exec(a=0_goto(j+i1+k),s2) by A4,A5,AMI_3:8
.= IC Exec(a=0_goto(j+k+i1),s2)
.= IC Exec(IncAddr(I,j+k), s2) by A3,Th24;
end;
suppose
A6: s1.a <> 0;
A7: IncAddr(I,j) = a=0_goto(i1+j) by A3,Th24;
A8: IncAddr(I,j+k) = a=0_goto(i1+(j+k)) by A3,Th24;
IC SCM in dom (IC SCM .--> (IC s1 + k)) by TARSKI:def 1;
then
A9: IC s2 = (IC SCM .--> (IC s1 + k)).IC SCM 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,AMI_3:8
.= IC s1 + 1 + k
.= IC s2 + 1 by A9
.= IC Exec(IncAddr(I,j+k), s2) by A8,A6,A4,AMI_3:8;
end;
end;
hence thesis;
end;
suppose
ex a,k st I = a>0_goto k;
then consider a, k1 such that
A10: I = a>0_goto k1;
reconsider i1=k1 as Element of NAT by ORDINAL1:def 12;
let j,k be Nat, s1 be State of SCM;
set s2 = IncIC(s1,k);
a <> IC SCM & dom (IC SCM .--> (IC s1 + k)) = {IC SCM}
by AMI_5:2;
then not a in dom (IC SCM .--> (IC s1 + k)) by TARSKI:def 1;
then
A11: s1.a = s2.a by FUNCT_4:11;
per cases;
suppose
A12: s1.a > 0;
thus IC Exec(IncAddr(I,j),s1) + k
= IC Exec(a>0_goto(j+k1),s1) + k by A10,Th25
.= j+k1+k by A12,AMI_3:9
.= IC Exec(a>0_goto(j+i1+k),s2) by A11,A12,AMI_3:9
.= IC Exec(a>0_goto(j+k+i1),s2)
.= IC Exec(IncAddr(I,j+k), s2) by A10,Th25;
end;
suppose
A13: s1.a <= 0;
A14: IncAddr(I,j) = a>0_goto(i1+j) by A10,Th25;
A15: IncAddr(I,j+k) = a>0_goto(i1+(j+k)) by A10,Th25;
IC SCM in dom (IC SCM .--> (IC s1 + k)) by TARSKI:def 1;
then
A16: IC s2 = (IC SCM .--> (IC s1 + k)).IC SCM by FUNCT_4:13
.= (IC s1 + k) by FUNCOP_1:72;
thus IC Exec(IncAddr(I,j),s1) + k
= IC s1 + 1 + k by A14,A13,AMI_3:9
.= IC s1 + 1 + k
.= IC s2 + 1 by A16
.= IC Exec(IncAddr(I,j+k), s2) by A15,A13,A11,AMI_3:9;
end;
end;
end;
end;
end;