:: On the Instructions of { \bf SCM+FSA }
:: 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, SCMFSA_2, AMI_3, AMI_1, FSM_1, INT_1, FUNCOP_1,
SUBSET_1, SCMFSA_1, CAT_1, XBOOLE_0, GRAPHSP, FINSEQ_1, RELAT_1, CARD_1,
AMI_2, AMISTD_2, CARD_3, FUNCT_1, AMISTD_1, CIRCUIT2, FUNCT_4, SETFAM_1,
XXREAL_0, TARSKI, ARYTM_3, GOBOARD5, FRECHET, ARYTM_1, COMPLEX1,
PARTFUN1, FINSEQ_2, RECDEF_2, NAT_1, COMPOS_1, GOBRD13, MEMSTR_0;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, SETFAM_1, RELAT_1, FUNCT_1,
PARTFUN1, ORDINAL1, XCMPLX_0, INT_1, FUNCOP_1, FINSEQ_1, FINSEQ_2,
FUNCT_4, FUNCT_7, COMPLEX1, CARD_1, CARD_3, XXREAL_0, NAT_1, RECDEF_2,
VALUED_1, NUMBERS, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMISTD_1,
AMISTD_2, AMI_3, SCM_INST, SCMFSA_1, SCMFSA_3, SCMFSA_2;
constructors REAL_1, NAT_D, AMI_3, SCMFSA_3, AMISTD_2, RELSET_1, AMISTD_1,
SCMFSA_1, PRE_POLY, FUNCT_7, DOMAIN_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, NUMBERS,
XREAL_0, NAT_1, INT_1, SCMFSA_2, AMISTD_2, CARD_3, FUNCT_4, VALUED_0,
EXTPRO_1, FUNCT_7, PRE_POLY, MEMSTR_0, CARD_1, COMPOS_0, XTUPLE_0,
FINSEQ_1;
requirements NUMERALS, BOOLE, SUBSET, REAL, ARITHM;
definitions TARSKI, AMISTD_1, AMISTD_2, XBOOLE_0, COMPOS_0;
equalities SCMFSA_2, AMISTD_1, FUNCOP_1, COMPOS_1, EXTPRO_1, AMI_3, MEMSTR_0,
COMPOS_0;
expansions AMISTD_1, XBOOLE_0;
theorems TARSKI, NAT_1, AMI_3, FUNCT_4, FUNCT_1, FUNCOP_1, SETFAM_1, AMISTD_1,
FINSEQ_1, FUNCT_7, CARD_3, SCMFSA_2, INT_1, BVFUNC14, ABSVALUE, FINSEQ_2,
XBOOLE_0, XBOOLE_1, NAT_D, MEMSTR_0, PARTFUN1, PBOOLE, VALUED_1,
EXTPRO_1, AMI_2, COMPOS_0, ORDINAL1;
begin
reserve a, b, d1, d2, d3, d4 for Int-Location,
A, B for Data-Location,
f, f1, f2, f3 for FinSeq-Location,
il, i1, i2 for Nat,
L for Nat,
I for Instruction of SCM+FSA,
s,s1,s2 for State of SCM+FSA,
T for InsType of the InstructionsF of SCM+FSA,
k for Nat;
definition
let la, lb be Int-Location, a, b be Integer;
redefine func (la,lb) --> (a,b) -> PartState of SCM+FSA; :: redefines --> (FUNCT_4, definition)
coherence
proof
A1: Values lb = INT by SCMFSA_2:11;
b is Element of INT by INT_1:def 2;
then reconsider b as Element of Values lb by A1;
A2: Values la = INT by SCMFSA_2:11;
a is Element of INT by INT_1:def 2;
then reconsider a as Element of Values la by A2;
(la,lb) --> (a,b) is PartState of SCM+FSA;
hence thesis;
end;
end;
theorem Th1:
for o being Object of SCM+FSA st o in Data-Locations SCM+FSA
holds o is Int-Location or o is FinSeq-Location
proof
let o be Object of SCM+FSA;
assume o in Data-Locations SCM+FSA;
then o in SCM-Data-Loc or o in SCM+FSA-Data*-Loc
by SCMFSA_2:100,XBOOLE_0:def 3;
hence thesis by AMI_2:def 16,SCMFSA_2:def 5;
end;
theorem Th2:
a := b = [1,{},<*a,b*>]
proof
ex A,B st a = A & b = B & a := b = A:=B by SCMFSA_2:def 8;
hence thesis;
end;
theorem Th3:
AddTo(a,b) = [2,{},<*a,b*>]
proof
ex A,B st a = A & b = B & AddTo(a,b) = AddTo(A,B) by SCMFSA_2:def 9;
hence thesis;
end;
theorem Th4:
SubFrom(a,b) = [3,{},<* a,b *>]
proof
ex A,B st a = A & b = B & SubFrom(a,b) = SubFrom(A,B) by SCMFSA_2:def 10;
hence thesis;
end;
theorem Th5:
MultBy(a,b) = [4,{},<* a,b *>]
proof
ex A,B st a = A & b = B & MultBy(a,b) = MultBy(A,B) by SCMFSA_2:def 11;
hence thesis;
end;
theorem Th6:
Divide(a,b) = [5,{},<* a,b *>]
proof
ex A,B st a = A & b = B & Divide(a,b) = Divide(A,B) by SCMFSA_2:def 12;
hence thesis;
end;
theorem Th7:
a=0_goto il = [7, <* il*>,<*a *>]
proof
ex A st A = a & A=0_goto il = a=0_goto il by SCMFSA_2:def 14;
hence thesis;
end;
theorem Th8:
a>0_goto il = [8, <* il*>,<*a *>]
proof
ex A st A = a & A>0_goto il = a>0_goto il by SCMFSA_2:def 15;
hence thesis;
end;
reserve J,K for Element of Segm 13,
b,b1,c,c1 for Element of SCM-Data-Loc,
f,f1 for Element of SCM+FSA-Data*-Loc;
theorem Th9:
JumpPart halt SCM+FSA = {};
reserve a, b, d1, d2, d3, d4 for Int-Location,
A, B for Data-Location,
f, f1,
f2, f3 for FinSeq-Location;
theorem Th10:
JumpPart (a:=b) = {}
proof
thus JumpPart (a:=b) = [ 1,{}, <*a,b*>]`2_3 by Th2
.= {};
end;
theorem Th11:
JumpPart AddTo(a,b) = {}
proof
thus JumpPart AddTo(a,b) = [ 2,{}, <*a,b*>]`2_3 by Th3
.= {};
end;
theorem Th12:
JumpPart SubFrom(a,b) = {}
proof
thus JumpPart SubFrom(a,b) = [ 3,{}, <*a,b*>]`2_3 by Th4
.= {};
end;
theorem Th13:
JumpPart MultBy(a,b) = {}
proof
thus JumpPart MultBy(a,b) = [ 4,{}, <*a,b*>]`2_3 by Th5
.= {};
end;
theorem Th14:
JumpPart Divide(a,b) = {}
proof
thus JumpPart Divide(a,b) = [ 5,{}, <*a,b*>]`2_3 by Th6
.= {};
end;
theorem Th15:
JumpPart (a=0_goto i1) = <*i1*>
proof
thus JumpPart (a=0_goto i1) = [ 7,<*i1*>,<*a*>]`2_3 by Th7
.= <*i1*>;
end;
theorem Th16:
JumpPart (a>0_goto i1) = <*i1*>
proof
thus JumpPart (a>0_goto i1) = [ 8,<*i1*>,<*a*>]`2_3 by Th8
.= <*i1*>;
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+FSA by A1,A3,SCMFSA_2:95;
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+FSA = 0;
hence thesis by A1,Th9,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+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = a:=b by A1,A3,SCMFSA_2:30;
x = {} by A2,Th10,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart(a:= a) by Th10;
InsCode(a:= a) = 1 by SCMFSA_2:18;
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+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = AddTo(a,b) by A1,A3,SCMFSA_2:31;
x = {} by A2,Th11,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart AddTo(a,a) by Th11;
InsCode AddTo(a,a) = 2 by SCMFSA_2:19;
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+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = SubFrom(a,b) by A1,A3,SCMFSA_2:32;
x = {} by A2,Th12,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart SubFrom(a,a) by Th12;
InsCode SubFrom(a,a) = 3 by SCMFSA_2:20;
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+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = MultBy(a,b) by A1,A3,SCMFSA_2:33;
x = {} by A2,Th13,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart MultBy(a,a) by Th13;
InsCode MultBy(a,a) = 4 by SCMFSA_2:21;
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+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b such that
A4: I = Divide(a,b) by A1,A3,SCMFSA_2:34;
x = {} by A2,Th14,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart Divide(a,a) by Th14;
InsCode Divide(a,a) = 5 by SCMFSA_2:22;
hence thesis by A5,A1;
end;
theorem Th23:
T = 6 implies dom product" JumpParts T = {1}
proof
set i1 = the Nat;
assume
A1: T = 6;
hereby
let x be object;
InsCode goto i1 = 6;
then
A2: JumpPart 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 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+FSA such that
A4: f = JumpPart I and
A5: InsCode I = T;
consider i1 such that
A6: I = goto i1 by A1,A5,SCMFSA_2:35;
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 Th24:
T = 7 implies dom product" JumpParts T = {1}
proof
set i1 = the Nat,a = the Int-Location;
assume
A1: T = 7;
A2: JumpPart (a =0_goto i1) = <*i1*> by Th15;
hereby
let x be object;
InsCode (a =0_goto i1) = 7 by SCMFSA_2:24;
then
A3: 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 A3,CARD_3:108;
hence x in {1} by A2,FINSEQ_1:2,38;
end;
let x be object;
assume
A4: 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+FSA such that
A5: f = JumpPart I and
A6: InsCode I = T;
consider i1, a such that
A7: I = a =0_goto i1 by A1,A6,SCMFSA_2:36;
f = <*i1*> by A5,A7,Th15;
hence thesis by A4,FINSEQ_1:2,38;
end;
then x in DOM JumpParts T by CARD_3:109;
hence thesis by CARD_3:def 12;
end;
theorem Th25:
T = 8 implies dom product" JumpParts T = {1}
proof
set i1 = the Nat,a = the Int-Location;
assume
A1: T = 8;
A2: JumpPart (a >0_goto i1) = <*i1*> by Th16;
hereby
let x be object;
InsCode (a >0_goto i1) = 8 by SCMFSA_2:25;
then
A3: 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 A3,CARD_3:108;
hence x in {1} by A2,FINSEQ_1:2,38;
end;
let x be object;
assume
A4: 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+FSA such that
A5: f = JumpPart I and
A6: InsCode I = T;
consider i1, a such that
A7: I = a >0_goto i1 by A1,A6,SCMFSA_2:37;
f = <*i1*> by A5,A7,Th16;
hence thesis by A4,FINSEQ_1:2,38;
end;
then x in DOM JumpParts T by CARD_3:109;
hence thesis by CARD_3:def 12;
end;
theorem
T = 9 implies JumpParts T = {{}}
proof
assume
A1: T = 9;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b,f such that
A4: I = b:=(f,a) by A1,A3,SCMFSA_2:38;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location, f = the FinSeq-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart(a:=(f,a));
InsCode(a:=(f,a)) = 9;
hence thesis by A5,A1;
end;
theorem
T = 10 implies JumpParts T = {{}}
proof
assume
A1: T = 10;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,b,f such that
A4: I = (f,a):=b by A1,A3,SCMFSA_2:39;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location, f = the FinSeq-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart((f,a):=a);
InsCode((f,a):=a) = 10;
hence thesis by A5,A1;
end;
theorem
T = 11 implies JumpParts T = {{}}
proof
assume
A1: T = 11;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,f such that
A4: I = a:=len f by A1,A3,SCMFSA_2:40;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location, f = the FinSeq-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart(a:=len f);
InsCode(a:=len f) = 11;
hence thesis by A5,A1;
end;
theorem
T = 12 implies JumpParts T = {{}}
proof
assume
A1: T = 12;
hereby
let x be object;
assume x in JumpParts T;
then consider I being Instruction of SCM+FSA such that
A2: x = JumpPart I and
A3: InsCode I = T;
consider a,f such that
A4: I = f:=<0,...,0>a by A1,A3,SCMFSA_2:41;
x = {} by A2,A4;
hence x in {{}} by TARSKI:def 1;
end;
set a = the Int-Location, f = the FinSeq-Location;
let x be object;
assume x in {{}};
then x = {} by TARSKI:def 1;
then
A5: x = JumpPart(f:=<0,...,0>a);
InsCode(f:=<0,...,0>a) = 12;
hence thesis by A5,A1;
end;
theorem
(product" JumpParts InsCode goto i1).1 = NAT
proof
dom product" JumpParts InsCode goto i1 = {1} by Th23;
then
A1: 1 in dom product" JumpParts InsCode goto i1 by TARSKI:def 1;
hereby
let x be object;
assume x in (product" JumpParts InsCode goto i1).1;
then x in pi(JumpParts InsCode goto i1,1) by A1,CARD_3:def 12;
then consider g being Function such that
A2: g in JumpParts InsCode goto i1 and
A3: x = g.1 by CARD_3:def 6;
consider I being Instruction of SCM+FSA such that
A4: g = JumpPart I and
A5: InsCode I = InsCode goto i1 by A2;
consider i2 such that
A6: I = goto i2 by A5,SCMFSA_2:35;
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 Nat;
A7: <*x*>.1 = x;
A8: InsCode goto i1 = InsCode goto x;
JumpPart goto x = <*x*>;
then <*x*> in JumpParts InsCode goto i1 by A8;
then x in pi(JumpParts InsCode goto i1,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 Th24,SCMFSA_2:24;
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+FSA such that
A4: g = JumpPart I and
A5: InsCode I = InsCode (a =0_goto i1) by A2;
consider i2, b such that
A6: I = b =0_goto i2 by A5,SCMFSA_2:24,36;
g = <*i2*> qua FinSequence by A4,A6,Th15;
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;
A7: <*x*>.1 = x;
InsCode (a =0_goto i1) = 7 by SCMFSA_2:24;
then
A8: InsCode (a =0_goto i1) = InsCode (a =0_goto x) by SCMFSA_2:24;
JumpPart (a =0_goto x) = <*x*> by Th15;
then <*x*> in JumpParts InsCode (a =0_goto i1) by A8;
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;
theorem
(product" JumpParts InsCode (a >0_goto i1)).1 = NAT
proof
dom product" JumpParts InsCode (a >0_goto i1) = {1} by Th25,SCMFSA_2:25;
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+FSA such that
A4: g = JumpPart I and
A5: InsCode I = InsCode (a >0_goto i1) by A2;
consider i2, b such that
A6: I = b >0_goto i2 by A5,SCMFSA_2:25,37;
g = <*i2*> by A4,A6,Th16;
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;
A7: <*x*>.1 = x;
InsCode (a >0_goto i1) = 8 by SCMFSA_2:25;
then
A8: InsCode (a >0_goto i1) = InsCode (a >0_goto x) by SCMFSA_2:25;
JumpPart (a >0_goto x) = <*x*> by Th16;
then <*x*> in JumpParts InsCode (a >0_goto i1) by A8;
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;
Lm1: for i being Instruction of SCM+FSA holds (for l being
Nat holds NIC(i,l)={l+1}) implies JUMP i is
empty
proof
reconsider p=0, q=1 as Nat;
let i be Instruction of SCM+FSA;
assume
A1: for l being Nat holds NIC(i,l)={l+1};
set X = the set of all NIC(i,f) where f is Nat;
reconsider p, q as 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
cluster JUMP halt SCM+FSA -> empty;
coherence;
end;
registration
let a, b;
cluster a:=b -> sequential;
coherence by SCMFSA_2:63;
cluster AddTo(a,b) -> sequential;
coherence
by SCMFSA_2:64;
cluster SubFrom(a,b) -> sequential;
coherence
by SCMFSA_2:65;
cluster MultBy(a,b) -> sequential;
coherence
by SCMFSA_2:66;
cluster Divide(a,b) -> sequential;
coherence
by SCMFSA_2:67;
end;
registration
let a, b;
cluster JUMP (a := b) -> empty;
coherence
proof
for l being Nat holds NIC(a:=b,l)={l + 1}
by AMISTD_1:12;
hence thesis by Lm1;
end;
cluster JUMP AddTo(a, b) -> empty;
coherence
proof
for l being Nat holds NIC(AddTo(a,b),l)={
l + 1 } by AMISTD_1:12;
hence thesis by Lm1;
end;
cluster JUMP SubFrom(a, b) -> empty;
coherence
proof
for l being Nat holds NIC(SubFrom(a,b),l)=
{l + 1} by AMISTD_1:12;
hence thesis by Lm1;
end;
cluster JUMP MultBy(a,b) -> empty;
coherence
proof
for l being Nat holds NIC(MultBy(a,b),l)={
l + 1 } by AMISTD_1:12;
hence thesis by Lm1;
end;
cluster JUMP Divide(a,b) -> empty;
coherence
proof
for l being Nat holds NIC(Divide(a,b),l)={
l + 1 } by AMISTD_1:12;
hence thesis by Lm1;
end;
end;
theorem Th33:
NIC(goto i1, il) = {i1}
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+FSA by MEMSTR_0:def 6;
reconsider n = il1 as Nat;
set I = goto i1;
set t = the State of SCM+FSA,
Q = the Instruction-Sequence of SCM+FSA;
assume
A2: x = i1;
reconsider u = t+*(IC SCM+FSA,il1)
as Element of product the_Values_of SCM+FSA by CARD_3:107;
reconsider P = Q +* (il,I)
as Instruction-Sequence of SCM+FSA;
IC SCM+FSA in dom t by MEMSTR_0:2;
then
A3: IC u = n by FUNCT_7:31;
il in NAT by ORDINAL1:def 12;
then
A4: P/.il = P.il by PBOOLE:143;
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) = i1 by A3,A4,SCMFSA_2:69;
hence x in {IC Exec(goto i1,s)
where s is Element of product the_Values_of SCM+FSA
: IC s = il} by A2,A3,A5,A4;
end;
now
assume x in {IC Exec(goto i1,s)
where s is Element of product the_Values_of SCM+FSA
: IC s = il};
then ex s being Element of product the_Values_of SCM+FSA
st x = IC Exec(goto i1,s) & IC s = il;
hence x = i1 by SCMFSA_2:69;
end;
hence
x in {i1} iff x in {IC Exec(goto i1,s)
where s is Element of product the_Values_of SCM+FSA
: IC s = il} by A1,TARSKI:def 1;
end;
hence thesis by TARSKI:2;
end;
theorem Th34:
JUMP goto i1 = {i1}
proof
set X = the set of all NIC(goto i1, il) ;
now
let x be object;
hereby
set il1 = 1;
A1: NIC(goto i1, il1) in X;
assume x in meet X;
then x in NIC(goto i1, il1) by A1,SETFAM_1:def 1;
hence x in {i1} by Th33;
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, il);
NIC(goto i1, il) = {i1} by Th33;
hence i1 in Y by A4,TARSKI:def 1;
end;
NIC(goto i1, i1) 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 goto i1 -> 1-element;
coherence
proof
JUMP goto i1 = {i1} by Th34;
hence thesis;
end;
end;
theorem Th35:
NIC(a=0_goto i1, il) = {i1, il + 1}
proof
set t = the State of SCM+FSA,
Q = the Instruction-Sequence of SCM+FSA;
hereby
let x be object;
assume x in NIC(a=0_goto i1, il);
then consider s being Element of product the_Values_of SCM+FSA
such that
A1: x = IC Exec(a=0_goto i1,s) and
A2: IC s = il;
per cases;
suppose
s.a = 0;
then x = i1 by A1,SCMFSA_2:70;
hence x in {i1, il + 1} by TARSKI:def 2;
end;
suppose
s.a <> 0;
then x = il + 1 by A1,A2,SCMFSA_2:70;
hence x in {i1, il + 1} by TARSKI:def 2;
end;
end;
let x be object;
set I = a=0_goto i1;
A3: IC SCM+FSA <> a by SCMFSA_2:56;
il in NAT by ORDINAL1:def 12;
then
reconsider il1 = il as Element of Values IC SCM+FSA by MEMSTR_0:def 6;
reconsider u = t+*(IC SCM+FSA,il1)
as Element of product the_Values_of SCM+FSA by CARD_3:107;
reconsider P = Q +* (il,I)
as Instruction-Sequence of SCM+FSA;
reconsider n = il as Nat;
assume
A4: x in {i1, il + 1};
per cases by A4,TARSKI:def 2;
suppose
A5: x = i1;
reconsider v = u+*(a .--> 0)
as Element of product the_Values_of SCM+FSA by CARD_3:107;
A6: IC SCM+FSA in dom t by MEMSTR_0:2;
not IC SCM+FSA in dom (a .--> 0) by A3,TARSKI:def 1;
then
A8: IC v = IC u by FUNCT_4:11
.= n by A6,FUNCT_7:31;
il in NAT by ORDINAL1:def 12;
then
A9: P/.il = P.il by PBOOLE:143;
il in NAT by ORDINAL1:def 12;
then il in dom Q by PARTFUN1:def 2;
then
A10: 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) = i1 by A8,A10,A9,SCMFSA_2:70;
hence thesis by A5,A8,A10,A9;
end;
suppose
A11: x = il + 1;
reconsider v = u+*(a .--> 1)
as Element of product the_Values_of SCM+FSA by CARD_3:107;
A12: IC SCM+FSA in dom t by MEMSTR_0:2;
not IC SCM+FSA in dom (a .--> 1) by A3,TARSKI:def 1;
then
A14: IC v = IC u by FUNCT_4:11
.= n by A12,FUNCT_7:31;
il in NAT by ORDINAL1:def 12;
then
A15: P/.il = P.il by PBOOLE:143;
il in NAT by ORDINAL1:def 12;
then il in dom Q by PARTFUN1:def 2;
then
A16: 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 A14,A16,A15,SCMFSA_2:70;
hence thesis by A11,A14,A16,A15;
end;
end;
theorem Th36:
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 consider il being Nat such that
A2: Y = NIC(a=0_goto i1, il);
NIC(a=0_goto i1, il) = {i1, il + 1} by Th35;
hence i1 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 i1, il2) = {i1, il2 + 1} by Th35;
NIC(a=0_goto i1, il2) in X;
then x in NIC(a=0_goto i1, il2) by A3,SETFAM_1:def 1;
then
A5: x = i1 or x = il2 + 1 by A4,TARSKI:def 2;
A6: NIC(a=0_goto i1, il1) = {i1, il1 + 1} by Th35;
NIC(a=0_goto i1, il1) in X;
then x in NIC(a=0_goto i1, il1) by A3,SETFAM_1:def 1;
then x = i1 or x = il1 + 1 by A6,TARSKI:def 2;
hence x in {i1} by A5,TARSKI:def 1;
end;
assume x in {i1};
then
A7: x = i1 by TARSKI:def 1;
NIC(a=0_goto i1, i1) 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 Th36;
hence thesis;
end;
end;
theorem Th37:
NIC(a>0_goto i1, il) = {i1, il + 1}
proof
set t = the State of SCM+FSA,
Q = the Instruction-Sequence of SCM+FSA;
hereby
let x be object;
assume x in NIC(a>0_goto i1, il);
then consider s being Element of product the_Values_of SCM+FSA
such that
A1: x = IC Exec(a>0_goto i1,s) and
A2: IC s = il;
per cases;
suppose
s.a > 0;
then x = i1 by A1,SCMFSA_2:71;
hence x in {i1, il + 1} by TARSKI:def 2;
end;
suppose
s.a <= 0;
then x = il + 1 by A1,A2,SCMFSA_2:71;
hence x in {i1, il + 1} by TARSKI:def 2;
end;
end;
let x be object;
set I = a>0_goto i1;
A3: IC SCM+FSA <> a by SCMFSA_2:56;
il in NAT by ORDINAL1:def 12;
then
reconsider il1 = il as Element of Values IC SCM+FSA by MEMSTR_0:def 6;
reconsider n = il as Nat;
reconsider u = t+*(IC SCM+FSA,il1)
as Element of product the_Values_of SCM+FSA by CARD_3:107;
reconsider P = Q +* (il,I) as Instruction-Sequence of SCM+FSA;
assume
A4: x in {i1, il + 1};
per cases by A4,TARSKI:def 2;
suppose
A5: x = i1;
reconsider v = u+*(a .--> 1)
as Element of product the_Values_of SCM+FSA by CARD_3:107;
A6: IC SCM+FSA in dom t by MEMSTR_0:2;
not IC SCM+FSA in dom (a .--> 1) by A3,TARSKI:def 1;
then
A8: IC v = IC u by FUNCT_4:11
.= n by A6,FUNCT_7:31;
il in NAT by ORDINAL1:def 12;
then
A9: P/.il = P.il by PBOOLE:143;
il in NAT by ORDINAL1:def 12;
then il in dom Q by PARTFUN1:def 2;
then
A10: 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) = i1 by A8,A10,A9,SCMFSA_2:71;
hence thesis by A5,A8,A10,A9;
end;
suppose
A11: x = il + 1;
reconsider v = u+*(a .--> 0)
as Element of product the_Values_of SCM+FSA by CARD_3:107;
A12: IC SCM+FSA in dom t by MEMSTR_0:2;
not IC SCM+FSA in dom (a .--> 0) by A3,TARSKI:def 1;
then
A14: IC v = IC u by FUNCT_4:11
.= n by A12,FUNCT_7:31;
il in NAT by ORDINAL1:def 12;
then
A15: P/.il = P.il by PBOOLE:143;
il in NAT by ORDINAL1:def 12;
then il in dom Q by PARTFUN1:def 2;
then
A16: 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 A14,A16,A15,SCMFSA_2:71;
hence thesis by A11,A14,A16,A15;
end;
end;
theorem Th38:
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 consider il being Nat such that
A2: Y = NIC(a>0_goto i1, il);
NIC(a>0_goto i1, il) = {i1, il + 1} by Th37;
hence i1 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 i1, il2) = {i1, il2 + 1} by Th37;
NIC(a>0_goto i1, il2) in X;
then x in NIC(a>0_goto i1, il2) by A3,SETFAM_1:def 1;
then
A5: x = i1 or x = il2 + 1 by A4,TARSKI:def 2;
A6: NIC(a>0_goto i1, il1) = {i1, il1 + 1} by Th37;
NIC(a>0_goto i1, il1) in X;
then x in NIC(a>0_goto i1, il1) by A3,SETFAM_1:def 1;
then x = i1 or x = il1 + 1 by A6,TARSKI:def 2;
hence x in {i1} by A5,TARSKI:def 1;
end;
assume x in {i1};
then
A7: x = i1 by TARSKI:def 1;
NIC(a>0_goto i1, i1) 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 Th38;
hence thesis;
end;
end;
registration
let a, b, f;
cluster a:=(f,b) -> sequential;
coherence
by SCMFSA_2:72;
end;
registration
let a, b, f;
cluster JUMP (a:=(f,b)) -> empty;
coherence
proof
for l being Nat holds NIC(a:=(f,b),l)={
l + 1} by AMISTD_1:12;
hence thesis by Lm1;
end;
end;
registration
let a, b, f;
cluster (f,b):=a -> sequential;
coherence
by SCMFSA_2:73;
end;
registration
let a, b, f;
cluster JUMP ((f,b):=a) -> empty;
coherence
proof
for l being Nat holds NIC((f,b):=a,l)={
l + 1} by AMISTD_1:12;
hence thesis by Lm1;
end;
end;
registration
let a, f;
cluster a:=len f -> sequential;
coherence
by SCMFSA_2:74;
end;
registration
let a, f;
cluster JUMP (a:=len f) -> empty;
coherence
proof
for l being Nat holds NIC(a:=len f,l)={
l + 1} by AMISTD_1:12;
hence thesis by Lm1;
end;
end;
registration
let a, f;
cluster f:=<0,...,0>a -> sequential;
coherence
by SCMFSA_2:75;
end;
registration
let a, f;
cluster JUMP (f:=<0,...,0>a) -> empty;
coherence
proof
for l being Nat holds NIC(f:=<0,...,0>a,l)
={l + 1} by AMISTD_1:12;
hence thesis by Lm1;
end;
end;
theorem Th39:
SUCC(il,SCM+FSA) = {il, il + 1}
proof
set X = the set of all
NIC(I, il) \ JUMP I where I is Element of the InstructionsF of
SCM+FSA;
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+FSA such that
A3: Y = NIC(i, il) \ JUMP i by A2;
per cases by SCMFSA_2:93;
suppose
i = [0,{},{}];
then x in {il} \ JUMP halt SCM+FSA
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 i1 st i = goto i1;
then consider i1 such that
A9: i = goto i1;
x in {i1} \ JUMP i by A1,A3,A9,Th33;
then x in {i1} \ {i1} by A9,Th34;
hence x in N by XBOOLE_1:37;
end;
suppose
ex i1,a st i = a=0_goto i1;
then consider i1, a such that
A10: i = a=0_goto i1;
A11: NIC(i, il) = {i1, il + 1} by A10,Th35;
x in NIC(i, il) by A1,A3,XBOOLE_0:def 5;
then
A12: x = i1 or x = il + 1 by A11,TARSKI:def 2;
x in NIC(i, il) \ {i1} by A1,A3,A10,Th36;
then not x in {i1} by XBOOLE_0:def 5;
hence x in N by A12,TARSKI:def 1,def 2;
end;
suppose
ex i1,a st i = a>0_goto i1;
then consider i1, a such that
A13: i = a>0_goto i1;
A14: NIC(i, il) = {i1, il + 1} by A13,Th37;
x in NIC(i, il) by A1,A3,XBOOLE_0:def 5;
then
A15: x = i1 or x = il + 1 by A14,TARSKI:def 2;
x in NIC(i, il) \ {i1} by A1,A3,A13,Th38;
then not x in {i1} by XBOOLE_0:def 5;
hence x in N by A15,TARSKI:def 1,def 2;
end;
suppose
ex a,b,f st i = b:=(f,a);
then consider a, b, f such that
A16: i = b:=(f,a);
x in {il + 1} \ JUMP (b:=(f,a)) by A1,A3,A16,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex a,b,f st i = (f,a):=b;
then consider a, b, f such that
A17: i = (f,a):=b;
x in {il + 1} \ JUMP ((f,a):=b) by A1,A3,A17,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex a,f st i = a:=len f;
then consider a, f such that
A18: i = a:=len f;
x in {il + 1} \ JUMP (a:=len f) by A1,A3,A18,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
suppose
ex a,f st i = f:=<0,...,0>a;
then consider a, f such that
A19: i = f:=<0,...,0>a;
x in {il + 1} \ JUMP (f:=<0,...,0>a) by A1,A3,A19,AMISTD_1:12;
then x = il + 1 by TARSKI:def 1;
hence x in N by TARSKI:def 2;
end;
end;
assume
A20: x in {il, il + 1};
per cases by A20,TARSKI:def 2;
suppose
A21: x = il;
set i = halt SCM+FSA;
NIC(i, il) \ JUMP i = {il} by AMISTD_1:2;
then
A22: {il} in X;
x in {il} by A21,TARSKI:def 1;
hence x in union X by A22,TARSKI:def 4;
end;
suppose
A23: x = il + 1;
set a = the Int-Location;
set i = AddTo(a,a);
NIC(i, il) \ JUMP i = {il + 1} by AMISTD_1:12;
then
A24: {il + 1} in X;
x in {il + 1} by A23,TARSKI:def 1;
hence x in union X by A24,TARSKI:def 4;
end;
end;
hence thesis by TARSKI:2;
end;
theorem Th40:
for k being Nat holds k+1 in SUCC(k,SCM+FSA) &
for j being Nat st j in SUCC(k,SCM+FSA) holds k <= j
proof
let k be Nat;
A1: SUCC(k,SCM+FSA) = {k, k+1} by Th39;
hence k+1 in SUCC(k,SCM+FSA) by TARSKI:def 2;
let j be Nat;
assume
A2: j in SUCC(k,SCM+FSA);
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
cluster SCM+FSA -> standard;
coherence by Th40,AMISTD_1:3;
end;
registration
cluster InsCode halt SCM+FSA -> jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
now
let s be State of SCM+FSA, o be Object of SCM+FSA, I be Instruction of
SCM+FSA;
assume that
A1: InsCode I = InsCode halt SCM+FSA and
o in Data-Locations SCM+FSA;
I = halt SCM+FSA by A1,SCMFSA_2:95;
hence Exec(I, s).o = s.o by EXTPRO_1:def 3;
end;
hence thesis;
end;
end;
registration
cluster halt SCM+FSA -> jump-only;
coherence;
end;
registration
let i1;
cluster InsCode goto i1 -> jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
set S = SCM+FSA;
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 and
A2: o in Data-Locations S;
A3: ex i2 st I = goto i2 by A1,SCMFSA_2:35;
per cases by A2,Th1;
suppose
o is Int-Location;
hence Exec(I, s).o = s.o by A3,SCMFSA_2:69;
end;
suppose
o is FinSeq-Location;
hence Exec(I, s).o = s.o by A3,SCMFSA_2:69;
end;
end;
hence thesis;
end;
end;
registration
let i1;
cluster goto i1 -> jump-only non sequential non ins-loc-free;
coherence
proof
thus InsCode goto i1 is jump-only;
JUMP goto i1 <> {};
hence goto i1 is non sequential by AMISTD_1:13;
thus JumpPart 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+FSA;
coherence
proof
set S = SCM+FSA;
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 S;
A3: ex i2, b st I = b =0_goto i2 by A1,SCMFSA_2:24,36;
per cases by A2,Th1;
suppose
o is Int-Location;
hence Exec(I, s).o = s.o by A3,SCMFSA_2:70;
end;
suppose
o is FinSeq-Location;
hence Exec(I, s).o = s.o by A3,SCMFSA_2:70;
end;
end;
hence thesis;
end;
cluster InsCode (a >0_goto i1) -> jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
set S = SCM+FSA;
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 S;
A6: ex i2, b st I = b >0_goto i2 by A4,SCMFSA_2:25,37;
per cases by A5,Th1;
suppose
o is Int-Location;
hence Exec(I, s).o = s.o by A6,SCMFSA_2:71;
end;
suppose
o is FinSeq-Location;
hence Exec(I, s).o = s.o by A6,SCMFSA_2:71;
end;
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;
dom JumpPart (a =0_goto i1) = dom <*i1*> by Th15
.= {1} by FINSEQ_1:2,38;
hence 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;
dom JumpPart (a >0_goto i1) = dom <*i1*> by Th16
.= {1} by FINSEQ_1:2,38;
hence JumpPart(a >0_goto i1) is not empty;
end;
end;
Lm2: intloc 0 <> intloc 1 by AMI_3:10;
registration
let a, b;
cluster InsCode (a:=b) -> non jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
set w = the State of SCM+FSA;
set t = w+*((intloc 0, intloc 1)-->(0,1));
A1: InsCode (a:=b) = 1 by SCMFSA_2:18
.= InsCode (intloc 0:=intloc 1) by SCMFSA_2:18;
A2: dom ((intloc 0, intloc 1)-->(0,1)) = {intloc 0, intloc 1} by FUNCT_4:62;
then
A3: intloc 1 in dom ((intloc 0, intloc 1)-->(0,1)) by TARSKI:def 2;
intloc 0 in dom ((intloc 0, intloc 1)-->(0,1)) by A2,TARSKI:def 2;
then
A4: t.intloc 0 = (intloc 0, intloc 1)-->(0,1).intloc 0 by FUNCT_4:13
.= 0 by AMI_3:10,FUNCT_4:63;
intloc 0 in Int-Locations by AMI_2:def 16;
then
A5: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
Exec((intloc 0:=intloc 1), t).intloc 0 = t.intloc 1 by SCMFSA_2:63
.= (intloc 0, intloc 1)-->(0,1).intloc 1 by A3,FUNCT_4:13
.= 1 by FUNCT_4:63;
hence thesis by A1,A4,A5;
end;
cluster InsCode AddTo(a,b) -> non jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
set w = the State of SCM+FSA;
set t = w+*((intloc 0, intloc 1)-->(0,1));
A6: InsCode AddTo(a,b) = 2 by SCMFSA_2:19
.= InsCode AddTo(intloc 0, intloc 1) by SCMFSA_2:19;
A7: dom ((intloc 0, intloc 1)-->(0,1)) = {intloc 0, intloc 1} by FUNCT_4:62;
then intloc 0 in dom ((intloc 0, intloc 1)-->(0,1)) by TARSKI:def 2;
then
A8: t.intloc 0 = (intloc 0, intloc 1)-->(0,1).intloc 0 by FUNCT_4:13
.= 0 by AMI_3:10,FUNCT_4:63;
intloc 0 in Int-Locations by AMI_2:def 16;
then
A9: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
intloc 1 in dom ((intloc 0, intloc 1)-->(0,1)) by A7,TARSKI:def 2;
then t.intloc 1 = (intloc 0, intloc 1)-->(0,1).intloc 1 by FUNCT_4:13
.= 1 by FUNCT_4:63;
then Exec(AddTo(intloc 0, intloc 1), t).intloc 0
= (0 qua Nat)+1 by A8,SCMFSA_2:64;
hence thesis by A6,A8,A9;
end;
cluster InsCode SubFrom(a,b) -> non jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
set w = the State of SCM+FSA;
set t = w+*((intloc 0, intloc 1)-->(0,1));
A10: InsCode SubFrom(a,b) = 3 by SCMFSA_2:20
.= InsCode SubFrom(intloc 0, intloc 1) by SCMFSA_2:20;
A11: dom ((intloc 0, intloc 1)-->(0,1)) = {intloc 0, intloc 1} by FUNCT_4:62;
then intloc 0 in dom ((intloc 0, intloc 1)-->(0,1)) by TARSKI:def 2;
then
A12: t.intloc 0 = (intloc 0, intloc 1)-->(0,1).intloc 0 by FUNCT_4:13
.= 0 by AMI_3:10,FUNCT_4:63;
intloc 0 in Int-Locations by AMI_2:def 16;
then
A13: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
intloc 1 in dom ((intloc 0, intloc 1)-->(0,1)) by A11,TARSKI:def 2;
then
A14: t.intloc 1 = (intloc 0, intloc 1)-->(0,1).intloc 1 by FUNCT_4:13
.= 1 by FUNCT_4:63;
Exec(SubFrom(intloc 0, intloc 1), t).intloc 0 = t.intloc 0 - t.intloc
1 by SCMFSA_2:65
.= -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+FSA;
coherence
proof
set w = the State of SCM+FSA;
set t = w+*((intloc 0, intloc 1)-->(1,0));
A15: InsCode MultBy(a,b) = 4 by SCMFSA_2:21
.= InsCode MultBy(intloc 0, intloc 1) by SCMFSA_2:21;
A16: dom ((intloc 0, intloc 1)-->(1,0)) = {intloc 0, intloc 1} by FUNCT_4:62;
then intloc 0 in dom ((intloc 0, intloc 1)-->(1,0)) by TARSKI:def 2;
then
A17: t.intloc 0 = (intloc 0, intloc 1)-->(1,0).intloc 0 by FUNCT_4:13
.= 1 by AMI_3:10,FUNCT_4:63;
intloc 0 in Int-Locations by AMI_2:def 16;
then
A18: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
intloc 1 in dom ((intloc 0, intloc 1)-->(1,0)) by A16,TARSKI:def 2;
then
A19: t.intloc 1 = (intloc 0, intloc 1)-->(1,0).intloc 1 by FUNCT_4:13
.= 0 by FUNCT_4:63;
Exec(MultBy(intloc 0, intloc 1), t).intloc 0 = t.intloc 0 * t.intloc
1 by SCMFSA_2:66
.= 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+FSA;
coherence
proof
set w = the State of SCM+FSA;
set t = w+*((intloc 0, intloc 1)-->(7,3));
A20: InsCode Divide(a,b) = 5 by SCMFSA_2:22
.= InsCode Divide(intloc 0, intloc 1) by SCMFSA_2:22;
A21: dom ((intloc 0, intloc 1)-->(7,3)) = {intloc 0, intloc 1} by FUNCT_4:62;
then intloc 0 in dom ((intloc 0, intloc 1)-->(7,3)) by TARSKI:def 2;
then
A22: t.intloc 0 = (intloc 0, intloc 1)-->(7,3).intloc 0 by FUNCT_4:13
.= 7 by AMI_3:10,FUNCT_4:63;
A23: 7 = 2 * 3 + 1;
intloc 0 in Int-Locations by AMI_2:def 16;
then
A24: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
intloc 1 in dom ((intloc 0, intloc 1)-->(7,3)) by A21,TARSKI:def 2;
then t.intloc 1 = (intloc 0, intloc 1)-->(7,3).intloc 1 by FUNCT_4:13
.= 3 by FUNCT_4:63;
then Exec(Divide(intloc 0, intloc 1), t).intloc 0 = 7 div (3 qua Element
of NAT) by A22,Lm2,SCMFSA_2:67
.= 2 by A23,NAT_D:def 1;
hence thesis by A20,A22,A24;
end;
end;
Lm3: fsloc 0 <> intloc 0 by SCMFSA_2:99;
Lm4: fsloc 0 <> intloc 1 by SCMFSA_2:99;
registration
let a, b, f;
cluster InsCode (b:=(f,a)) -> non jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
Values intloc 1 = INT by SCMFSA_2:11;
then reconsider E = 1 as Element of Values intloc 1 by INT_1:def 1;
Values intloc 0 = INT by SCMFSA_2:11;
then reconsider D = 1 as Element of Values intloc 0 by INT_1:def 1;
reconsider DWA = 2 as Element of INT by INT_1:def 1;
set w = the State of SCM+FSA;
<*DWA*> in INT* by FINSEQ_1:def 11;
then reconsider F = <*2*> as Element of Values fsloc 0 by SCMFSA_2:12;
reconsider t = w+*(fsloc 0 .--> F)+*(intloc 0 .--> D)+*(intloc 1 .--> E)
as State of SCM+FSA;
A1: t.intloc 0 = D by AMI_3:10,BVFUNC14:12;
A2: t.fsloc 0 = F by Lm3,Lm4,FUNCT_7:114;
then dom (t.fsloc 0) = {1} by FINSEQ_1:2,def 8;
then
A3: 1 in dom (t.fsloc 0) by TARSKI:def 1;
consider k being Nat such that
A4: k = |. t.intloc 1 .| and
A5: Exec((intloc 0):=(fsloc 0, intloc 1), t).intloc 0 = (t.fsloc 0)
/. k by SCMFSA_2:72;
intloc 0 in Int-Locations by AMI_2:def 16;
then
A6: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
t.intloc 1 = E by FUNCT_7:94;
then k = 1 by A4,ABSVALUE:def 1;
then
A7: Exec(intloc 0:=(fsloc 0, intloc 1), t).intloc 0 = (t.fsloc 0).1 by A5,A3,
PARTFUN1:def 6
.= 2 by A2;
InsCode (b:=(f,a)) = 9
.= InsCode ((intloc 0):=(fsloc 0, intloc 1));
hence thesis by A1,A7,A6;
end;
cluster InsCode ((f,a):=b) -> non jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
Values intloc 0 = INT by SCMFSA_2:11;
then reconsider D = 1 as Element of Values intloc 0 by INT_1:def 1;
reconsider DWA = 2 as Element of INT by INT_1:def 1;
set w = the State of SCM+FSA;
A8: InsCode ((f,a):=b) = 10
.= InsCode ((fsloc 0, intloc 1):=(intloc 0));
Values intloc 1 = INT by SCMFSA_2:11;
then reconsider E = 1 as Element of Values intloc 1 by INT_1:def 1;
<*DWA*> in INT* by FINSEQ_1:def 11;
then reconsider F = <*2*> as Element of Values fsloc 0 by SCMFSA_2:12;
reconsider t = w+*(fsloc 0 .--> F)+*(intloc 0 .--> D)+*(intloc 1 .--> E)
as State of SCM+FSA;
consider k being Nat such that
A9: k = |. t.intloc 1 .| and
A10: Exec((fsloc 0, intloc 1):=(intloc 0), t).fsloc 0 = (t.fsloc 0) +*
(k,t.intloc 0) by SCMFSA_2:73;
t.intloc 1 = E by FUNCT_7:94;
then
A11: k = 1 by A9,ABSVALUE:def 1;
fsloc 0 in FinSeq-Locations by SCMFSA_2:def 5;
then
A12: fsloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
A13: F <> <*D*> by FINSEQ_1:76;
A14: t.fsloc 0 = F by Lm3,Lm4,FUNCT_7:114;
t.intloc 0 = D by AMI_3:10,BVFUNC14:12;
then Exec((fsloc 0, intloc 1):=intloc 0, t).fsloc 0 = <*D*> by A14,A10,A11,
FUNCT_7:95;
hence thesis by A8,A14,A13,A12;
end;
end;
registration
let a, b, f;
cluster b:=(f,a) -> non jump-only;
coherence;
cluster (f,a):=b -> non jump-only;
coherence;
end;
registration
let a, f;
cluster InsCode (a:=len f) -> non jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
Values intloc 0 = INT by SCMFSA_2:11;
then reconsider D = 3 as Element of Values intloc 0 by INT_1:def 1;
reconsider DWA = 2 as Element of INT by INT_1:def 1;
set w = the State of SCM+FSA;
A1: InsCode (a:=len f) = 11
.= InsCode (intloc 0:=len fsloc 0);
<*DWA*> in INT* by FINSEQ_1:def 11;
then reconsider F = <*2*> as Element of Values fsloc 0 by SCMFSA_2:12;
reconsider t = w+*(fsloc 0 .--> F)+*(intloc 0 .--> D) as State of SCM+FSA;
A2: t.fsloc 0 = F by BVFUNC14:12,SCMFSA_2:99;
intloc 0 in Int-Locations by AMI_2:def 16;
then
A3: intloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
A4: t.intloc 0 = D by FUNCT_7:94;
Exec(intloc 0 :=len fsloc 0, t).intloc 0 = len (t.fsloc 0) by SCMFSA_2:74
.= 1 by A2,FINSEQ_1:39;
hence thesis by A1,A4,A3;
end;
cluster InsCode (f:=<0,...,0>a) -> non jump-only
for InsType of the InstructionsF of SCM+FSA;
coherence
proof
Values intloc 0 = INT by SCMFSA_2:11;
then reconsider D = 1 as Element of Values intloc 0 by INT_1:def 1;
reconsider DWA = 2 as Element of INT by INT_1:def 1;
set w = the State of SCM+FSA;
<*DWA*> in INT* by FINSEQ_1:def 11;
then reconsider F = <*2*> as Element of Values fsloc 0 by SCMFSA_2:12;
reconsider t = w+*(fsloc 0 .--> F)+*(intloc 0 .--> D) as State of SCM+FSA;
A5: t.fsloc 0 = F by BVFUNC14:12,SCMFSA_2:99;
A6: F <> <*0*> by FINSEQ_1:76;
consider k being Nat such that
A7: k = |. t.intloc 0 .| and
A8: Exec(fsloc 0:=<0,...,0>intloc 0, t).fsloc 0 = k |-> 0 by SCMFSA_2:75;
fsloc 0 in FinSeq-Locations by SCMFSA_2:def 5;
then
A9: fsloc 0 in Data-Locations SCM+FSA by SCMFSA_2:100,XBOOLE_0:def 3;
t.intloc 0 = D by FUNCT_7:94;
then k = 1 by A7,ABSVALUE:def 1;
then
A10: Exec(fsloc 0:=<0,...,0>intloc 0, t).fsloc 0 = <*0*> by A8,FINSEQ_2:59;
InsCode (f:=<0,...,0>a) = 12
.= InsCode (fsloc 0:=<0,...,0>intloc 0);
hence thesis by A5,A6,A10,A9;
end;
end;
registration
let a, f;
cluster a:=len f -> non jump-only;
coherence;
cluster f:=<0,...,0>a -> non jump-only;
coherence;
end;
registration
cluster SCM+FSA -> with_explicit_jumps;
coherence
proof
let I be Instruction of SCM+FSA;
thus JUMP I c= rng JumpPart I
proof
let f be object such that
A1: f in JUMP I;
per cases by SCMFSA_2:93;
suppose
I = [0,{},{}];
hence thesis by A1,SCMFSA_2:96;
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 i1 st I = goto i1;
consider i1 such that
A3: I = goto i1 by A2;
rng<*i1*> = {i1} by FINSEQ_1:39;
hence thesis by A1,A3,Th34;
end;
suppose
A4: ex i1,a st I = a=0_goto i1;
consider a, i1 such that
A5: I = a=0_goto i1 by A4;
A6: JumpPart (a=0_goto i1) = <*i1*> by Th15;
rng<*i1*> = {i1} by FINSEQ_1:39;
hence thesis by A1,A5,A6,Th36;
end;
suppose
A7: ex i1,a st I = a>0_goto i1;
consider a, i1 such that
A8: I = a>0_goto i1 by A7;
A9: JumpPart (a>0_goto i1) = <*i1*> by Th16;
rng<*i1*> = {i1} by FINSEQ_1:39;
hence thesis by A1,A8,A9,Th38;
end;
suppose
ex a,b,f st I = b:=(f,a);
hence thesis by A1;
end;
suppose
ex a,b,f st I = (f,a):=b;
hence thesis by A1;
end;
suppose
ex a,f st I = a:=len f;
hence thesis by A1;
end;
suppose
ex a,f st I = f:=<0,...,0>a;
hence thesis by A1;
end;
end;
let f being object;
assume f in rng JumpPart I;
then consider k being object such that
A10: k in dom JumpPart I and
A11: f = (JumpPart I).k by FUNCT_1:def 3;
per cases by SCMFSA_2:93;
suppose
I = [0,{},{}];
then dom JumpPart I = dom {};
hence thesis by A10;
end;
suppose
ex a,b st I = a:=b;
then consider a, b such that
A12: I = a:=b;
k in dom {} by A10,A12,Th10;
hence thesis;
end;
suppose
ex a,b st I = AddTo(a,b);
then consider a, b such that
A13: I = AddTo(a,b);
k in dom {} by A10,A13,Th11;
hence thesis;
end;
suppose
ex a,b st I = SubFrom(a,b);
then consider a, b such that
A14: I = SubFrom(a,b);
k in dom {} by A10,A14,Th12;
hence thesis;
end;
suppose
ex a,b st I = MultBy(a,b);
then consider a, b such that
A15: I = MultBy(a,b);
k in dom {} by A10,A15,Th13;
hence thesis;
end;
suppose
ex a,b st I = Divide(a,b);
then consider a, b such that
A16: I = Divide(a,b);
k in dom {} by A10,A16,Th14;
hence thesis;
end;
suppose
ex i1 st I = goto i1;
then consider i1 such that
A17: I = goto i1;
A18: JumpPart I = <*i1*> by A17;
then k = 1 by A10,FINSEQ_1:90;
then
A19: f = i1 by A18,A11;
JUMP I = {i1} by A17,Th34;
hence thesis by A19,TARSKI:def 1;
end;
suppose
ex i1,a st I = a=0_goto i1;
then consider a, i1 such that
A20: I = a=0_goto i1;
A21: JumpPart I = <*i1*> by A20,Th15;
then k = 1 by A10,FINSEQ_1:90;
then
A22: f = i1 by A21,A11;
JUMP I = {i1} by A20,Th36;
hence thesis by A22,TARSKI:def 1;
end;
suppose
ex i1,a st I = a>0_goto i1;
then consider a, i1 such that
A23: I = a>0_goto i1;
A24: JumpPart I = <*i1*> by A23,Th16;
then k = 1 by A10,FINSEQ_1:90;
then
A25: f = i1 by A24,A11;
JUMP I = {i1} by A23,Th38;
hence thesis by A25,TARSKI:def 1;
end;
suppose
ex a,b,f st I = b:=(f,a);
then consider a, b, f such that
A26: I = b:=(f,a);
k in dom {} by A10,A26;
hence thesis;
end;
suppose
ex a,b,f st I = (f,a):=b;
then consider a, b, f such that
A27: I = (f,a):=b;
k in dom {} by A10,A27;
hence thesis;
end;
suppose
ex a,f st I = a:=len f;
then consider a, f such that
A28: I = a:=len f;
k in dom {} by A10,A28;
hence thesis;
end;
suppose
ex a,f st I = f:=<0,...,0>a;
then consider a, f such that
A29: I = f:=<0,...,0>a;
k in dom {} by A10,A29;
hence thesis;
end;
end;
end;
theorem Th41:
IncAddr(goto i1,k) = goto (i1+ k)
proof
A1: InsCode IncAddr(goto i1,k) = InsCode goto i1 by COMPOS_0:def 9
.= 6
.= InsCode goto (i1+k);
A2: AddressPart IncAddr(goto i1,k) = AddressPart goto i1 by COMPOS_0:def 9
.= {}
.= AddressPart goto (i1+k);
A3: JumpPart IncAddr(goto i1,k) = k + JumpPart goto i1
by COMPOS_0:def 9;
then
A4: dom JumpPart IncAddr(goto i1,k) = dom JumpPart goto i1
by VALUED_1:def 2;
A5: for x being object st x in dom JumpPart goto i1 holds (JumpPart
IncAddr(goto i1,k)).x = (JumpPart goto (i1+k)).x
proof
let x be object;
assume
A6: x in dom JumpPart goto i1;
then x in dom <*i1*>;
then
A7: x = 1 by FINSEQ_1:90;
set f = (JumpPart goto i1).x;
A8: (JumpPart IncAddr(goto i1,k)).x = k+f by A4,A3,A6,VALUED_1:def 2;
thus
(JumpPart IncAddr(goto i1,k)).x =
<*(i1+k)*>.
x by A7,A8
.= (JumpPart goto (i1+k)).x;
end;
dom JumpPart goto (i1+k)
= dom <*(i1+k)*>
.= Seg 1 by FINSEQ_1:def 8
.= dom <*i1*> by FINSEQ_1:def 8
.= dom JumpPart goto i1;
then JumpPart IncAddr(goto i1,k) = JumpPart goto(i1+k) by A4,A5,FUNCT_1:2;
hence thesis by A1,A2,COMPOS_0:1;
end;
theorem Th42:
IncAddr(a=0_goto i1,k) = a=0_goto (i1+k)
proof
A1: InsCode IncAddr(a=0_goto i1,k) = InsCode (a=0_goto i1) by COMPOS_0:def 9
.= 7 by SCMFSA_2:24
.= InsCode (a=0_goto (i1+k)) by SCMFSA_2:24;
A2: a=0_goto i1 = [7, <* i1*>,<*a *>] by Th7;
A3: a=0_goto(i1+k) = [7, <* i1+k*>,<*a *>] by Th7;
A4: AddressPart IncAddr(a=0_goto i1,k)
= AddressPart (a=0_goto i1) by COMPOS_0:def 9
.= <*a*> by A2
.= AddressPart (a=0_goto (i1+k)) by A3;
A5: JumpPart IncAddr(a=0_goto i1,k) = k + JumpPart (a=0_goto i1)
by COMPOS_0:def 9;
then
A6: dom JumpPart IncAddr(a=0_goto i1,k) = dom JumpPart (a=0_goto i1)
by VALUED_1:def 2;
A7: 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
A8: x in dom JumpPart (a=0_goto i1);
then
x in dom <*i1*> by Th15;
then
A9: x = 1 by FINSEQ_1:90;
set f = (JumpPart (a=0_goto i1)).x;
A10: (JumpPart IncAddr(a=0_goto i1,k)).x = k+f by A6,A5,A8,VALUED_1:def 2;
f = <*i1*>.x by Th15
.= i1 by A9;
hence
(JumpPart IncAddr(a=0_goto i1,k)).x =
<*(i1+k)*>.x by A9,A10
.= (JumpPart (a=0_goto (i1+k))).x
by Th15;
end;
dom JumpPart (a=0_goto (i1+k))
= dom <*(i1+k)*> by Th15
.= Seg 1 by FINSEQ_1:38
.= dom <*i1*> by FINSEQ_1:38
.= dom JumpPart (a=0_goto i1) by Th15;
then JumpPart IncAddr(a=0_goto i1,k) = JumpPart (a=0_goto (i1+k))
by A6,A7,FUNCT_1:2;
hence thesis by A1,A4,COMPOS_0:1;
end;
theorem Th43:
IncAddr(a>0_goto i1,k) = a>0_goto (i1+k)
proof
A1: InsCode IncAddr(a>0_goto i1,k) = InsCode (a>0_goto i1) by COMPOS_0:def 9
.= 8 by SCMFSA_2:25
.= InsCode (a>0_goto (i1+k)) by SCMFSA_2:25;
A2: a>0_goto i1 = [8, <* i1*>,<*a *>] by Th8;
A3: a>0_goto(i1+k) = [8, <* i1+k*>,<*a *>] by Th8;
A4: AddressPart IncAddr(a>0_goto i1,k)
= AddressPart (a>0_goto i1) by COMPOS_0:def 9
.= <*a*> by A2
.= AddressPart (a>0_goto (i1+k)) by A3;
A5: JumpPart IncAddr(a>0_goto i1,k) = k + JumpPart (a>0_goto i1)
by COMPOS_0:def 9;
then
A6: dom JumpPart IncAddr(a>0_goto i1,k) = dom JumpPart (a>0_goto i1)
by VALUED_1:def 2;
A7: 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
A8: x in dom JumpPart (a>0_goto i1);
then x in dom <*i1*> by Th16;
then
A9: x = 1 by FINSEQ_1:90;
set f = (JumpPart (a>0_goto i1)).1;
A10: (JumpPart IncAddr(a>0_goto i1,k)).1 = k+f by A9,A6,A5,A8,VALUED_1:def 2;
f = <*i1*>.x by Th16,A9
.= i1 by A9;
hence
(JumpPart IncAddr(a>0_goto i1,k)).x
= <*(i1+k)*>.x by A9,A10
.= (JumpPart (a>0_goto (i1+k))).x by Th16;
end;
dom JumpPart (a>0_goto (i1+k)) =
dom <*(i1+k)*> by Th16
.= Seg 1 by FINSEQ_1:38
.= dom <*i1*> by FINSEQ_1:38
.= dom JumpPart (a>0_goto i1) by Th16;
then JumpPart IncAddr(a>0_goto i1,k) = JumpPart (a>0_goto (i1+k))
by A6,A7,FUNCT_1:2;
hence thesis by A1,A4,COMPOS_0:1;
end;
registration
cluster SCM+FSA -> IC-relocable;
coherence
proof
let I be Instruction of SCM+FSA;
per cases by SCMFSA_2:93;
suppose
I = [0,{},{}];
hence thesis by SCMFSA_2:96;
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 i1 st I = goto i1;
let j,k be Nat, s1 be State of SCM+FSA;
set s2 = IncIC(s1,k);
consider i1 such that
A2: I = goto i1 by A1;
thus IC Exec(IncAddr(I,j),s1) + k
= IC Exec(goto(j+i1),s1) + k by A2,Th41
.= j+i1+k by SCMFSA_2:69
.= IC Exec(goto(j+k+i1),s2) by SCMFSA_2:69
.= IC Exec(IncAddr(I,j+k), s2) by A2,Th41;
end;
suppose
ex i1,a 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+FSA;
set s2 = IncIC(s1,k);
a <> IC SCM+FSA & dom (IC SCM+FSA .--> (IC s1 + k)) = {IC SCM+FSA}
by SCMFSA_2:56;
then not a in dom (IC SCM+FSA .--> (IC s1 + k)) by TARSKI:def 1;
then
A4: s1.a = s2.a by FUNCT_4:11;
per cases;
suppose
A5: s1.a = 0;
thus IC Exec(IncAddr(I,j),s1) + k
= IC Exec(a=0_goto(j+i1),s1) + k by A3,Th42
.= j+i1+k by A5,SCMFSA_2:70
.= IC Exec(a=0_goto(j+k+i1),s2) by A4,A5,SCMFSA_2:70
.= IC Exec(IncAddr(I,j+k), s2) by A3,Th42;
end;
suppose
A6: s1.a <> 0;
A7: IncAddr(I,j) = a=0_goto(i1+j) by A3,Th42;
A8: IncAddr(I,j+k) = a=0_goto(i1+(j+k)) by A3,Th42;
IC SCM+FSA in dom (IC SCM+FSA .--> (IC s1 + k))
by TARSKI:def 1;
then
A9: IC s2 = (IC SCM+FSA .--> (IC s1 + k)).IC SCM+FSA 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,SCMFSA_2:70
.= IC s2 + 1 by A9
.= IC Exec(IncAddr(I,j+k), s2) by A8,A6,A4,SCMFSA_2:70;
end;
end;
suppose
ex i1,a st I = a>0_goto i1;
then consider i1,a such that
A10: I = a>0_goto i1;
let j,k be Nat, s1 be State of SCM+FSA;
set s2 = IncIC(s1,k);
a <> IC SCM+FSA & dom (IC SCM+FSA .--> (IC s1 + k)) = {IC SCM+FSA}
by SCMFSA_2:56;
then not a in dom (IC SCM+FSA .--> (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+i1),s1) + k by A10,Th43
.= j+i1+k by A12,SCMFSA_2:71
.= IC Exec(a>0_goto(j+k+i1),s2) by A11,A12,SCMFSA_2:71
.= IC Exec(IncAddr(I,j+k), s2) by A10,Th43;
end;
suppose
A13: s1.a <= 0;
A14: IncAddr(I,j) = a>0_goto(i1+j) by A10,Th43;
A15: IncAddr(I,j+k) = a>0_goto(i1+(j+k)) by A10,Th43;
IC SCM+FSA in dom (IC SCM+FSA .--> (IC s1 + k))
by TARSKI:def 1;
then
A16: IC s2 = (IC SCM+FSA .--> (IC s1 + k)).IC SCM+FSA 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,SCMFSA_2:71
.= IC s2 + 1 by A16
.= IC Exec(IncAddr(I,j+k), s2) by A15,A13,A11,SCMFSA_2:71;
end;
end;
suppose
ex a,b,f st I = b:=(f,a);
hence thesis;
end;
suppose
ex a,b,f st I = (f,a):=b;
hence thesis;
end;
suppose
ex a,f st I = a:=len f;
hence thesis;
end;
suppose
ex a,f st I = f:=<0,...,0>a;
hence thesis;
end;
end;
end;