:: On the compositions of macro instructions
:: by Andrzej Trybulec , Yatsuka Nakamura and Noriko Asamoto
::
:: Received June 20, 1996
:: Copyright (c) 1996-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, SUBSET_1, AMI_1, SCMFSA_2, EXTPRO_1, FUNCT_4, AMI_3,
FUNCOP_1, RELAT_1, FUNCT_1, TARSKI, XBOOLE_0, CARD_1, CAT_1, NAT_1,
ARYTM_3, XXREAL_0, AMISTD_2, VALUED_1, FSM_1, GRAPHSP, ARYTM_1, INT_1,
COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, SCMFSA6A, RELOC, MEMSTR_0,
SCMPDS_4, TURING_1, AMISTD_1, FRECHET, COMPOS_1, SCMPDS_5;
notations TARSKI, XBOOLE_0, SUBSET_1, CARD_1, ORDINAL1, NUMBERS, XCMPLX_0,
COMPLEX1, NAT_1, INT_1, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FINSEQ_1,
FINSEQ_2, FUNCT_4, DOMAIN_1, VALUED_1, AFINSQ_1, NAT_D, STRUCT_0,
MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, FUNCT_7, SCMFSA_2, AMISTD_1,
AMISTD_2, FUNCOP_1, XXREAL_0, SCMFSA_M;
constructors WELLORD2, DOMAIN_1, XXREAL_0, INT_2, AMISTD_2, SCMFSA_2,
RELSET_1, VALUED_1, AMI_3, PRE_POLY, AMISTD_1, FUNCT_7, MEMSTR_0,
SCMFSA_1, SCMFSA_M, NAT_D, COMPOS_2, AFINSQ_1;
registrations XBOOLE_0, FUNCT_1, ORDINAL1, RELSET_1, FUNCOP_1, FINSET_1,
XREAL_0, INT_1, SCMFSA_2, FUNCT_4, RELAT_1, VALUED_1, SCMFSA10, AMISTD_2,
COMPOS_1, EXTPRO_1, AMI_3, COMPOS_0, NAT_1, AMISTD_1, COMPOS_2, AFINSQ_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions AFINSQ_1, AMISTD_1;
equalities FUNCOP_1, COMPOS_1, FUNCT_4, MEMSTR_0;
expansions COMPOS_1;
theorems FUNCT_2, RELAT_1, FUNCT_7, FUNCT_4, FUNCT_1, ZFMISC_1, FUNCOP_1,
TARSKI, NAT_1, SCMFSA_4, SCMFSA_2, CARD_1, CARD_2, ENUMSET1, GRFUNC_1,
RELSET_1, XBOOLE_0, XBOOLE_1, VALUED_1, AFINSQ_1, COMPOS_1, EXTPRO_1,
COMPOS_0, SCMFSA_M, PARTFUN1, AMISTD_1, SCMFSA10;
begin
reserve l, m, n for Nat,
i,j,k for Instruction of SCM+FSA,
I,J,K for Program of SCM+FSA;
::$CD
definition
let P be preProgram of SCM+FSA;
func Directed P -> preProgram of SCM+FSA equals
P +~ (halt SCM+FSA,goto card P);
coherence;
projectivity by FUNCT_4:127;
end;
registration
let I be Program of SCM+FSA;
cluster Directed I -> initial non empty;
coherence
proof
thus Directed I is initial
proof let m,n be Nat such that
A1: n in dom Directed I and
A2: m < n;
n in dom I by A1,FUNCT_4:99;
then m in dom I by A2,AFINSQ_1:def 12;
hence thesis by FUNCT_4:99;
end;
thus Directed I is non empty;
end;
end;
theorem
not halt SCM+FSA in rng Directed I by FUNCT_4:100;
theorem
Reloc(Directed I, m) = ((id the InstructionsF of
SCM+FSA) +* (halt SCM+FSA .--> goto (m + card I)))* Reloc(I, m)
proof
rng(halt SCM+FSA .--> goto (card I)) = {goto (card I)} by FUNCOP_1:8;
then
A1: rng((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto (
card I))) c= rng(id the InstructionsF of SCM+FSA) \/ {goto (card I)} by
FUNCT_4:17;
A2: rng(id the InstructionsF of SCM+FSA) \/ {goto (card I)} = the
InstructionsF of SCM+FSA by ZFMISC_1:40;
dom(halt SCM+FSA .--> goto (card I)) = {halt SCM+FSA};
then
dom((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto (
card I))) = dom(id the InstructionsF of SCM+FSA) \/ {halt SCM+FSA} by
FUNCT_4:def 1
.= the InstructionsF of SCM+FSA by ZFMISC_1:40;
then reconsider
f = (id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto
card I) as Function of the InstructionsF of SCM+FSA, the InstructionsF of
SCM+FSA by A1,A2,FUNCT_2:def 1,RELSET_1:4;
A3: IncAddr(goto card I,m) = goto (m + card I) by SCMFSA_4:1;
dom id the InstructionsF of SCM+FSA = the InstructionsF of SCM+FSA;
then
A4: f = (id the InstructionsF of SCM+FSA) +* (halt SCM+FSA, goto card
I) by FUNCT_7:def 3;
A5: rng I c= the InstructionsF of SCM+FSA by RELAT_1:def 19;
A6: Reloc(Directed I,m) = IncAddr(Shift(Directed I,m),m)
by COMPOS_1:34;
A7: Reloc(I,m) = IncAddr(Shift(I,m),m) by COMPOS_1:34;
Directed I = f*I by A4,A5,FUNCT_7:116;
hence Reloc(Directed I, m)
= IncAddr(f*Shift(I,m),m) by A6,VALUED_1:22
.= ((id the InstructionsF of SCM+FSA) +* (halt SCM+FSA .--> goto (m
+ card I)))* Reloc(I, m) by A3,A7,COMPOS_1:47;
end;
reserve a,b for Int-Location,
f for FinSeq-Location,
s,s1,s2 for State of SCM+FSA;
set q = (intloc 0) .--> 1;
set f = the_Values_of SCM+FSA;
theorem Th3:
InsCode i in {0,6,7,8} or Exec(i,s).IC SCM+FSA = IC s + 1
proof
assume
A1: not InsCode i in {0,6,7,8};
then
A2: InsCode i <> 0 & InsCode i <> 6 by ENUMSET1:def 2;
A3: InsCode i <> 7 & InsCode i <> 8 by A1,ENUMSET1:def 2;
InsCode i = 0 or ... or InsCode i = 12 by SCMFSA_2:16;
then per cases by A2,A3;
suppose
InsCode i = 1;
then ex a,b st i = a:=b by SCMFSA_2:30;
hence thesis by SCMFSA_2:63;
end;
suppose
InsCode i = 2;
then ex a,b st i = AddTo(a,b) by SCMFSA_2:31;
hence thesis by SCMFSA_2:64;
end;
suppose
InsCode i = 3;
then ex a,b st i = SubFrom(a,b) by SCMFSA_2:32;
hence thesis by SCMFSA_2:65;
end;
suppose
InsCode i = 4;
then ex a,b st i = MultBy(a,b) by SCMFSA_2:33;
hence thesis by SCMFSA_2:66;
end;
suppose
InsCode i = 5;
then ex a,b st i = Divide(a,b) by SCMFSA_2:34;
hence thesis by SCMFSA_2:67;
end;
suppose
InsCode i = 9;
then ex a,b,f st i = b:=(f,a) by SCMFSA_2:38;
hence thesis by SCMFSA_2:72;
end;
suppose
InsCode i = 10;
then ex a,b,f st i = (f,a):=b by SCMFSA_2:39;
hence thesis by SCMFSA_2:73;
end;
suppose
InsCode i = 11;
then ex a,f st i = a:=len f by SCMFSA_2:40;
hence thesis by SCMFSA_2:74;
end;
suppose
InsCode i = 12;
then ex a,f st i = f:=<0,...,0>a by SCMFSA_2:41;
hence thesis by SCMFSA_2:75;
end;
end;
::$CT 4
theorem
for s1,s2 being State of SCM+FSA, n being Nat, i being
Instruction of SCM+FSA holds IC s1 + n = IC s2 & DataPart s1 = DataPart s2
implies IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) & DataPart Exec(i,s1) =
DataPart Exec(IncAddr(i,n),s2)
proof
set D = Data-Locations SCM+FSA;
let s1,s2 be State of SCM+FSA;
let n be Nat;
let i be Instruction of SCM+FSA;
assume that
A1: IC s1 + n = IC s2 and
A2: DataPart s1 = DataPart s2;
reconsider k1 = IC s1 as Element of NAT;
A3: IC s1 + 1 + n = (k1 + 1) + n
.= IC s2 + 1 by A1;
A4: now
set I = InsCode i;
assume that
A5: I < 6 or 8 < I and
A6: I <> 0;
not(I = 6 or ... or I = 8) by A5;
then not I in {6,7,8} by ENUMSET1:def 1;
then
A7: IncAddr(i,n) = i by SCMFSA_4:4;
not(I = 0 or (I = 6 or ... or I = 8)) by A5,A6;
then
A8: not I in {0,6,7,8} by ENUMSET1:def 2;
then IC Exec(i,s1) = IC s1 + 1 by Th3;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A3,A8,A7,Th3;
end;
InsCode i = 0 or ... or InsCode i = 12 by SCMFSA_2:16;
then per cases;
suppose
InsCode i = 0;
then
A9: i = halt SCM+FSA by SCMFSA_2:95;
then Exec(i,s1) = s1 & Exec(i,s2) = s2 by EXTPRO_1:def 3;
hence thesis by A1,A2,A9,COMPOS_0:4;
end;
suppose
A10: InsCode i = 1;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider da, db being Int-Location such that
A11: i = da := db by A10,SCMFSA_2:30;
A12: IncAddr(i,n) = i by A11,COMPOS_0:4;
A13: now
let c be Int-Location;
per cases;
suppose
A14: c = da;
hence Exec(i,s1).c = s1.db by A11,SCMFSA_2:63
.= s2.db by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A11,A12,A14,SCMFSA_2:63;
end;
suppose
A15: c <> da;
hence Exec(i,s1).c = s1.c by A11,SCMFSA_2:63
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A11,A12,A15,SCMFSA_2:63;
end;
end;
now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A11,SCMFSA_2:63
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A11,A12,SCMFSA_2:63;
end;
hence thesis by A13,SCMFSA_M:2;
end;
suppose
A16: InsCode i = 2;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider da, db being Int-Location such that
A17: i = AddTo(da, db) by A16,SCMFSA_2:31;
A18: IncAddr(i,n) = i by A17,COMPOS_0:4;
A19: now
let c be Int-Location;
per cases;
suppose
A20: c = da;
s1.da = s2.da & s1.db = s2.db by A2,SCMFSA_M:2;
hence Exec(i,s1).c = s2.da + s2.db by A17,A20,SCMFSA_2:64
.= Exec(IncAddr(i,n),s2).c by A17,A18,A20,SCMFSA_2:64;
end;
suppose
A21: c <> da;
hence Exec(i,s1).c = s1.c by A17,SCMFSA_2:64
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A17,A18,A21,SCMFSA_2:64;
end;
end;
now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A17,SCMFSA_2:64
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A17,A18,SCMFSA_2:64;
end;
hence thesis by A19,SCMFSA_M:2;
end;
suppose
A22: InsCode i = 3;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider da, db being Int-Location such that
A23: i = SubFrom(da, db) by A22,SCMFSA_2:32;
A24: IncAddr(i,n) = i by A23,COMPOS_0:4;
A25: now
let c be Int-Location;
per cases;
suppose
A26: c = da;
s1.da = s2.da & s1.db = s2.db by A2,SCMFSA_M:2;
hence Exec(i,s1).c = s2.da - s2.db by A23,A26,SCMFSA_2:65
.= Exec(IncAddr(i,n),s2).c by A23,A24,A26,SCMFSA_2:65;
end;
suppose
A27: c <> da;
hence Exec(i,s1).c = s1.c by A23,SCMFSA_2:65
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A23,A24,A27,SCMFSA_2:65;
end;
end;
now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A23,SCMFSA_2:65
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A23,A24,SCMFSA_2:65;
end;
hence thesis by A25,SCMFSA_M:2;
end;
suppose
A28: InsCode i = 4;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider da, db being Int-Location such that
A29: i = MultBy(da, db) by A28,SCMFSA_2:33;
A30: IncAddr(i,n) = i by A29,COMPOS_0:4;
A31: now
let c be Int-Location;
per cases;
suppose
A32: c = da;
s1.da = s2.da & s1.db = s2.db by A2,SCMFSA_M:2;
hence Exec(i,s1).c = s2.da * s2.db by A29,A32,SCMFSA_2:66
.= Exec(IncAddr(i,n),s2).c by A29,A30,A32,SCMFSA_2:66;
end;
suppose
A33: c <> da;
hence Exec(i,s1).c = s1.c by A29,SCMFSA_2:66
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A29,A30,A33,SCMFSA_2:66;
end;
end;
now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A29,SCMFSA_2:66
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A29,A30,SCMFSA_2:66;
end;
hence thesis by A31,SCMFSA_M:2;
end;
suppose
A34: InsCode i = 5;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider da, db being Int-Location such that
A35: i = Divide(da, db) by A34,SCMFSA_2:34;
A36: IncAddr(i,n) = i by A35,COMPOS_0:4;
A37: now
let c be Int-Location;
per cases;
suppose
A38: c = db;
s1.da = s2.da & s1.db = s2.db by A2,SCMFSA_M:2;
hence Exec(i,s1).c = s2.da mod s2.db by A35,A38,SCMFSA_2:67
.= Exec(IncAddr(i,n),s2).c by A35,A36,A38,SCMFSA_2:67;
end;
suppose
A39: c = da & c <> db;
s1.da = s2.da & s1.db = s2.db by A2,SCMFSA_M:2;
hence Exec(i,s1).c = s2.da div s2.db by A35,A39,SCMFSA_2:67
.= Exec(IncAddr(i,n),s2).c by A35,A36,A39,SCMFSA_2:67;
end;
suppose
A40: c <> da & c <> db;
hence Exec(i,s1).c = s1.c by A35,SCMFSA_2:67
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A35,A36,A40,SCMFSA_2:67;
end;
end;
now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A35,SCMFSA_2:67
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A35,A36,SCMFSA_2:67;
end;
hence thesis by A37,SCMFSA_M:2;
end;
suppose
InsCode i = 6;
then consider loc being Nat such that
A41: i = goto loc by SCMFSA_2:35;
A42: IncAddr(i,n) = goto (loc + n) by A41,SCMFSA_4:1;
A43: now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A41,SCMFSA_2:69
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A42,SCMFSA_2:69;
end;
IC Exec(i,s1) = loc by A41,SCMFSA_2:69;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A42,SCMFSA_2:69;
now
let c be Int-Location;
thus Exec(i,s1).c = s1.c by A41,SCMFSA_2:69
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A42,SCMFSA_2:69;
end;
hence thesis by A43,SCMFSA_M:2;
end;
suppose
InsCode i = 7;
then consider
loc being Nat, da being Int-Location
such that
A44: i = da=0_goto loc by SCMFSA_2:36;
A45: IncAddr(i,n) = da=0_goto (loc + n) by A44,SCMFSA_4:2;
A46: now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A44,SCMFSA_2:70
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A45,SCMFSA_2:70;
end;
hereby
per cases;
suppose
s1.da = 0;
then s2.da = 0 & IC Exec(i,s1) = loc by A2,A44,SCMFSA_2:70,SCMFSA_M:2;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A45,SCMFSA_2:70;
end;
suppose
s1.da <> 0;
then s2.da <> 0 & IC Exec(i,s1) = IC s1 + 1
by A2,A44,SCMFSA_2:70,SCMFSA_M:2;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A3,A45,
SCMFSA_2:70;
end;
end;
now
let c be Int-Location;
thus Exec(i,s1).c = s1.c by A44,SCMFSA_2:70
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A45,SCMFSA_2:70;
end;
hence thesis by A46,SCMFSA_M:2;
end;
suppose
InsCode i = 8;
then consider
loc being Nat, da being Int-Location
such that
A47: i = da>0_goto loc by SCMFSA_2:37;
A48: IncAddr(i,n) = da>0_goto (loc + n) by A47,SCMFSA_4:3;
A49: now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A47,SCMFSA_2:71
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A48,SCMFSA_2:71;
end;
hereby
per cases;
suppose
s1.da > 0;
then s2.da > 0 & IC Exec(i,s1) = loc by A2,A47,SCMFSA_2:71,SCMFSA_M:2;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A48,SCMFSA_2:71;
end;
suppose
s1.da <= 0;
then s2.da <= 0 & IC Exec(i,s1) = IC s1 + 1
by A2,A47,SCMFSA_2:71,SCMFSA_M:2;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2)
by A3,A48,SCMFSA_2:71;
end;
end;
now
let c be Int-Location;
thus Exec(i,s1).c = s1.c by A47,SCMFSA_2:71
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A48,SCMFSA_2:71;
end;
hence thesis by A49,SCMFSA_M:2;
end;
suppose
A50: InsCode i = 9;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider db, da being Int-Location, f being FinSeq-Location such that
A51: i = da := (f,db) by A50,SCMFSA_2:38;
A52: IncAddr(i,n) = i by A51,COMPOS_0:4;
A53: now
let c be Int-Location;
per cases;
suppose
A54: c = da;
then consider m being Nat such that
A55: m = |.s1.db.| and
A56: Exec(da:=(f,db), s1).c = (s1.f)/.m by SCMFSA_2:72;
A57: s1.f = s2.f by A2,SCMFSA_M:2;
consider m2 being Nat such that
A58: m2 = |.s2.db.| and
A59: Exec(da:=(f,db), s2).c = (s2.f)/.m2 by A54,SCMFSA_2:72;
m = m2 by A2,A55,A58,SCMFSA_M:2;
hence Exec(i,s1).c = Exec(IncAddr(i,n),s2).c by A51,A56,A59,A57,
COMPOS_0:4;
end;
suppose
A60: c <> da;
hence Exec(i,s1).c = s1.c by A51,SCMFSA_2:72
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A51,A52,A60,SCMFSA_2:72;
end;
end;
now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A51,SCMFSA_2:72
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A51,A52,SCMFSA_2:72;
end;
hence thesis by A53,SCMFSA_M:2;
end;
suppose
A61: InsCode i = 10;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider db, da being Int-Location, f being FinSeq-Location such that
A62: i = (f,db):=da by A61,SCMFSA_2:39;
A63: IncAddr(i,n) = i by A62,COMPOS_0:4;
A64: now
let g be FinSeq-Location;
per cases;
suppose
A65: g = f;
A66: s1.da = s2.da & s1.f = s2.f by A2,SCMFSA_M:2;
consider m2 being Nat such that
A67: m2 = |.s2.db.| and
A68: Exec((f,db):=da, s2).f = s2.f+*(m2,s2.da) by SCMFSA_2:73;
consider m1 being Nat such that
A69: m1 = |.s1.db.| and
A70: Exec((f,db):=da, s1).f = s1.f+*(m1,s1.da) by SCMFSA_2:73;
m1 = m2 by A2,A69,A67,SCMFSA_M:2;
hence Exec(i,s1).g = Exec(IncAddr(i,n),s2).g by A62,A65,A70,A68,A66,
COMPOS_0:4;
end;
suppose
A71: g <> f;
hence Exec(i,s1).g = s1.g by A62,SCMFSA_2:73
.= s2.g by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).g by A62,A63,A71,SCMFSA_2:73;
end;
end;
now
let c be Int-Location;
thus Exec(i,s1).c = s1.c by A62,SCMFSA_2:73
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A62,A63,SCMFSA_2:73;
end;
hence thesis by A64,SCMFSA_M:2;
end;
suppose
A72: InsCode i = 11;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider da being Int-Location, f being FinSeq-Location such that
A73: i = da :=len f by A72,SCMFSA_2:40;
A74: IncAddr(i,n) = i by A73,COMPOS_0:4;
A75: now
let c be Int-Location;
per cases;
suppose
A76: c = da;
hence Exec(i,s1).c = len(s1.f) by A73,SCMFSA_2:74
.= len(s2.f) by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A73,A74,A76,SCMFSA_2:74;
end;
suppose
A77: c <> da;
hence Exec(i,s1).c = s1.c by A73,SCMFSA_2:74
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A73,A74,A77,SCMFSA_2:74;
end;
end;
now
let f be FinSeq-Location;
thus Exec(i,s1).f = s1.f by A73,SCMFSA_2:74
.= s2.f by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).f by A73,A74,SCMFSA_2:74;
end;
hence thesis by A75,SCMFSA_M:2;
end;
suppose
A78: InsCode i = 12;
hence IC Exec(i,s1) + n = IC Exec(IncAddr(i,n),s2) by A4;
consider da being Int-Location, f being FinSeq-Location such that
A79: i = f:=<0,...,0>da by A78,SCMFSA_2:41;
A80: IncAddr(i,n) = i by A79,COMPOS_0:4;
A81: now
let g be FinSeq-Location;
per cases;
suppose
A82: g = f;
(ex m1 being Nat st m1 = |.s1.da.| & Exec(f
:=<0,...,0>da, s1).f = m1 |-> 0 )& ex m2 being Nat st m2 = |.s2.da
.| & Exec(f :=<0,...,0>da, s2).f = m2 |-> 0 by SCMFSA_2:75;
hence Exec(i,s1).g = Exec(IncAddr(i,n),s2).g
by A2,A79,A80,A82,SCMFSA_M:2;
end;
suppose
A83: g <> f;
hence Exec(i,s1).g = s1.g by A79,SCMFSA_2:75
.= s2.g by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).g by A79,A80,A83,SCMFSA_2:75;
end;
end;
now
let c be Int-Location;
thus Exec(i,s1).c = s1.c by A79,SCMFSA_2:75
.= s2.c by A2,SCMFSA_M:2
.= Exec(IncAddr(i,n),s2).c by A79,A80,SCMFSA_2:75;
end;
hence thesis by A81,SCMFSA_M:2;
end;
end;
::$CT 6
begin :: The composition of macroinstructions
definition
::$CD
let I,J be Program of SCM+FSA;
func I ";" J -> Program of SCM+FSA equals
stop Directed I ';' J;
coherence;
end;
registration
let I be Program of SCM+FSA, J be halt-ending Program of SCM+FSA;
cluster I ";" J -> halt-ending;
coherence;
end;
registration
let P be preProgram of SCM+FSA;
cluster Directed P -> halt-free;
correctness by FUNCT_4:100;
end;
registration
cluster halt-free for Program of SCM+FSA;
existence
proof
take Directed the Program of SCM+FSA;
thus thesis;
end;
end;
registration
let I be Program of SCM+FSA, J be unique-halt Program of SCM+FSA;
cluster I ";" J -> unique-halt;
coherence;
end;
Lm1:
for I being preProgram of SCM+FSA
holds card Directed I = card I
proof
let I be preProgram of SCM+FSA;
thus card Directed I = card dom Directed I by CARD_1:62
.= card dom I by FUNCT_4:99
.= card I by CARD_1:62;
end;
Lm2:
for I being Program of SCM+FSA
holds card stop Directed I = card stop I
proof let I be Program of SCM+FSA;
thus card stop Directed I = card Directed I + 1 by COMPOS_1:72
.= card I + 1 by Lm1
.= card stop I by COMPOS_1:72;
end;
theorem Th5:
for I,J being Program of SCM+FSA, l being Nat
st l in dom I & I.l <> halt SCM+FSA holds (I ";" J).l = I.l
proof
let I,J be Program of SCM+FSA, l be Nat such
that
A1: l in dom I and
A2: I.l <> halt SCM+FSA;
Reloc(J,card I) = IncAddr(Shift(J,card I),card I) by COMPOS_1:34;
then
A3: dom Reloc(J, card I) = dom Shift(J,card I) by COMPOS_1:def 21;
A4: card stop I -' 1 = card I by COMPOS_1:71;
A5: card stop Directed I = card stop I by Lm2;
now
assume l in dom(Reloc(J, card I));
then l in { m+card I where m is Nat: m in dom J } by A3,VALUED_1:def 12;
then consider m being Nat such that
A6: l = m+card I and
m in dom J;
m + card I < card I by A1,A6,AFINSQ_1:66;
hence contradiction by NAT_1:11;
end;
hence (I ";" J).l = (Directed I).l by FUNCT_4:11,A4,A5
.= I.l by A2,FUNCT_4:105;
end;
theorem
for I,J being Program of SCM+FSA holds Directed I c= I ";" J
proof
let I,J be Program of SCM+FSA;
A1: card stop I -' 1 = card I by COMPOS_1:71;
A2: card stop Directed I = card stop I by Lm2;
A3: now
let x be object;
assume x in dom Directed I;
then
A4: x in dom I by FUNCT_4:99;
dom I misses dom Reloc(J,card I) by COMPOS_1:48;
then not x in dom Reloc(J,card I) by A4,XBOOLE_0:3;
hence (Directed I).x = (I ";" J).x by FUNCT_4:11,A1,A2;
end;
dom (I ";" J) = dom Directed I \/ dom Reloc(J,card I) by FUNCT_4:def 1,A1,A2;
then dom Directed I c= dom (I ";" J) by XBOOLE_1:7;
hence thesis by A3,GRFUNC_1:2;
end;
theorem Th7:
for I,J being Program of SCM+FSA holds dom I c= dom (I ";" J)
proof
let I,J be Program of SCM+FSA;
A1: card stop I -' 1 = card I by COMPOS_1:71;
card stop Directed I = card stop I by Lm2;
then dom (I ";" J) = dom Directed I \/ dom Reloc(J,card I)
by FUNCT_4:def 1,A1
.= dom I \/ dom Reloc(J,card I) by FUNCT_4:99;
hence thesis by XBOOLE_1:7;
end;
theorem
for I,J being Program of SCM+FSA holds I +* (I ";" J) = (I ";" J)
proof
let I,J be Program of SCM+FSA;
A1: for x be object st x in dom (I ";" J)
holds (I +* (I ";" J)).x = (I ";" J).x by FUNCT_4:13;
dom (I +* (I ";" J)) = dom I \/ dom (I ";" J) by FUNCT_4:def 1
.= dom (I ";" J) by Th7,XBOOLE_1:12;
hence thesis by A1,FUNCT_1:2;
end;
begin :: The compostion of instruction and macroinstructions
definition
let i, J;
func i ";" J -> Program of SCM+FSA equals
Macro i ";" J;
correctness;
end;
definition
let I, j;
func I ";" j -> Program of SCM+FSA equals
I ";" Macro j;
correctness;
end;
definition
let i,j;
func i ";" j -> Program of SCM+FSA equals
Macro i ";" Macro j;
correctness;
end;
registration
cluster sequential for Instruction of SCM+FSA;
existence
proof take intloc 0:= intloc 0; thus thesis; end;
end;
registration
cluster sequential -> No-StopCode for Instruction of SCM+FSA;
coherence
proof let i be Instruction of SCM+FSA such that
A1: i is sequential;
reconsider i as Element of the InstructionsF of SCM+FSA;
i <> halt SCM+FSA by A1;
then i is No-StopCode by COMPOS_0:def 12;
hence thesis;
end;
end;
registration let i,j be sequential Instruction of SCM+FSA;
cluster i ";" j -> halt-ending unique-halt;
coherence;
end;
registration
let I be MacroInstruction of SCM+FSA,
j be sequential Instruction of SCM+FSA;
cluster I ";" j -> halt-ending unique-halt;
coherence;
end;
registration
let i be sequential Instruction of SCM+FSA,
J be MacroInstruction of SCM+FSA;
cluster i ";" J -> halt-ending unique-halt;
coherence;
end;
theorem
i ";" j = Macro i ";" j;
theorem
i ";" j = i ";" Macro j;
theorem Th11:
card(I ";" J) = card I + card J
proof
A1: card dom(I ";" J) = card(I ";" J) & card dom I = card I;
A2: card stop Directed I = card stop I by Lm2;
card stop I -' 1 = card I by COMPOS_1:71;
then
A3: dom(I ";" J) = dom Directed I \/ dom Reloc(J, card I) by FUNCT_4:def 1,A2
.= dom I \/ dom Reloc(J, card I) by FUNCT_4:99;
card dom Reloc(J, card I) = card Reloc(J, card I) by CARD_1:62
.= card J by COMPOS_1:49
.= card dom J;
hence thesis by A1,A3,CARD_2:40,COMPOS_1:48;
end;
theorem
for I being preProgram of SCM+FSA
holds I is halt-free implies Directed I = I
by FUNCT_4:103;
theorem Th13:
for I being preProgram of SCM+FSA, k being Element of NAT holds
Reloc(Directed I,k) = Reloc(I,k) +~ (halt SCM+FSA,goto(card I + k))
proof
let I be preProgram of SCM+FSA;
let k be Element of NAT;
A1: dom Reloc(I,k) = {m + k where m is Nat: m in dom I} by COMPOS_1:33;
A2: dom Directed I = dom I by FUNCT_4:99;
A3: dom Reloc(Directed I,k) = {m + k where m is Nat: m in dom I}
by A2,COMPOS_1:33;
A4: now
let x be object;
assume
A5: x in {m + k where m is Nat: m in dom I};
then consider n being Nat such that
A6: x = n + k and
A7: n in dom I;
dom Directed I = dom I by FUNCT_4:99;
then reconsider i = (Directed I). n as Instruction of SCM+FSA by A7,
FUNCT_1:106;
reconsider i0 = I. n as Instruction of SCM+FSA by A7,FUNCT_1:106;
A8: now
per cases;
suppose
A9: i0 = halt SCM+FSA;
then
A10: i = goto card I by A7,FUNCT_4:106;
A11: (Reloc(I,k)).x
= IncAddr(i0,k) by A6,A7,COMPOS_1:35
.= halt SCM+FSA by A9,COMPOS_0:4;
then (Reloc(I,k)).x in {halt SCM+FSA} by TARSKI:def 1;
then (Reloc(I,k)).x in dom (halt SCM+FSA .--> goto
(card I + k));
then x in dom ((halt SCM+FSA .--> goto (card I + k))*
Reloc(I,k)) by A1,A5,FUNCT_1:11;
hence (Reloc(I,k) +~ (halt SCM+FSA,goto(card I + k))).x =
((halt SCM+FSA .--> goto (card I + k))* Reloc(I,k)).x by FUNCT_4:13
.= (halt SCM+FSA .--> goto (card I + k)). ((
Reloc(I,k)).x) by A1,A5,FUNCT_1:13
.= goto (card I + k) by A11,FUNCOP_1:72
.= IncAddr(i,k) by A10,SCMFSA_4:1;
end;
suppose
A12: i0 <> halt SCM+FSA;
A13: (Reloc(I,k)).x = IncAddr(i0,k) by A6,A7,COMPOS_1:35;
A14: InsCode halt SCM+FSA = 0 by COMPOS_1:70;
InsCode i0 <> 0 by A12,SCMFSA_2:95;
then IncAddr(i0,k) <> halt SCM+FSA by A14,COMPOS_0:def 9;
then not (Reloc(I,k)).x in {halt SCM+FSA} by A13,TARSKI:def 1;
then
not (Reloc(I,k)).x in dom (halt SCM+FSA .--> goto
(card I + k));
then not x in dom ((halt SCM+FSA .--> goto (card I + k)) *
Reloc(I,k)) by FUNCT_1:11;
hence (Reloc(I,k) +~ (halt SCM+FSA,goto(card I + k))).x =
(Reloc(I,k)).x by FUNCT_4:11
.= IncAddr(i,k) by A12,A13,FUNCT_4:105;
end;
end;
thus (Reloc(Directed I,k)).x
= (Reloc(I,k) +~ (halt SCM+FSA,goto(card I + k))).x
by A8,A2,A6,A7,COMPOS_1:35;
end;
dom(Reloc(I,k) +~ (halt SCM+FSA,goto(card I + k))) =
{m + k where m is Nat:
m in dom I} by A1,FUNCT_4:99;
hence thesis by A3,A4,FUNCT_1:2;
end;
theorem Th14:
for I,J being Program of SCM+FSA holds Directed (I ";" J) = I ";" Directed J
proof
let I,J be Program of SCM+FSA;
A1: card stop I -' 1 = card I by COMPOS_1:71;
A2: card stop Directed I = card stop I by Lm2;
hence I ";" Directed J
= Directed I +*
(Reloc(J,card I) +~ (halt SCM+FSA,goto(card J + card I))) by Th13,A1
.= Directed I +*
(Reloc(J,card I) +~ (halt SCM+FSA,goto(card(I ";" J)))) by Th11
.= Directed I+~(halt SCM+FSA,goto card (I ";" J))+*
(Reloc(J,card I)+~(halt SCM+FSA,goto card (I ";" J))) by FUNCT_4:127
.= Directed (I ";" J) by FUNCT_7:117,A1,A2;
end;
theorem Th15:
I ";" J ";" K = I ";" (J ";" K)
proof
A1: card stop I -' 1 = card I by COMPOS_1:71;
A2: card stop Directed I = card stop I by Lm2;
A3: card stop Directed(I ";" J) = card stop(I ";" J) by Lm2;
A4: card stop(I ";" J) -' 1 = card(I ";" J) by COMPOS_1:71;
A5: card stop Directed J = card stop J by Lm2;
card stop J -' 1 = card J by COMPOS_1:71;
then
A6: Reloc(J ";" K, card I)
= Reloc(Directed J, card I) +* Reloc(Reloc(K, card J), card I)
by COMPOS_1:42,A5
.= Reloc(Directed J, card I) +* Reloc(K,card J + card I) by COMPOS_1:43;
thus I ";" J ";" K
= (I ";" Directed J) +* Reloc(K, card (I ";" J)) by Th14,A4,A3
.= Directed I +* (Reloc(Directed J, card I) +*
Reloc(K, card (I ";" J))) by FUNCT_4:14,A1,A2
.= I ";" (J ";" K) by A6,Th11,A1,A2;
end;
theorem
I ";" J ";" k = I ";" (J ";" k) by Th15;
theorem
I ";" j ";" K = I ";" (j ";" K) by Th15;
theorem
I ";" j ";" k = I ";" (j ";" k) by Th15;
theorem
i ";" J ";" K = i ";" (J ";" K) by Th15;
theorem
i ";" J ";" k = i ";" (J ";" k) by Th15;
theorem
i ";" j ";" K = i ";" (j ";" K) by Th15;
theorem
i ";" j ";" k = i ";" (j ";" k) by Th15;
theorem
card(i ";" J) = card J + 2
proof
thus card(i ";" J) = card Macro i + card J by Th11
.= card J + 2 by COMPOS_1:56;
end;
theorem
card(I ";" j) = card I + 2
proof
thus card(I ";" j) = card Macro j + card I by Th11
.= card I + 2 by COMPOS_1:56;
end;
theorem
card(i ";" j) = 4
proof
thus card(i ";" j) = card Macro i + card Macro j by Th11
.= card Macro i + 2 by COMPOS_1:56
.= 2 + 2 by COMPOS_1:56
.= 4;
end;
theorem
for I being preProgram of SCM+FSA
holds card Directed I = card I by Lm1;
theorem Th27:
for I being Program of SCM+FSA
holds card stop Directed I = card stop I by Lm2;
theorem
Reloc(J,card I) c= I ";" J
proof
I ";" J
= CutLastLoc stop Directed I +* Reloc(J,card stop I -' 1) by Th27
.= CutLastLoc stop Directed I +* Reloc(J,card I) by COMPOS_1:71;
hence thesis by FUNCT_4:25;
end;
theorem
dom(I ";" J) = dom I \/ dom Reloc(J, card I)
proof
I ";" J
= CutLastLoc stop Directed I +* Reloc(J,card stop I -' 1) by Th27
.= Directed I +* Reloc(J,card I) by COMPOS_1:71;
hence dom(I ";" J) = dom Directed I \/ dom Reloc(J, card I) by FUNCT_4:def 1
.= dom I \/ dom Reloc(J, card I) by FUNCT_4:99;
end;
theorem
n in dom Reloc(J,card I)
implies (I ";" J).n = Reloc(J,card I).n
proof assume
A1: n in dom Reloc(J,card I);
I ";" J
= CutLastLoc stop Directed I +* Reloc(J,card stop I -' 1) by Th27
.= Directed I +* Reloc(J,card I) by COMPOS_1:71;
hence (I ";" J).n = Reloc(J,card I).n by A1,FUNCT_4:13;
end;
begin :: closedness
registration let I be really-closed Program of SCM+FSA;
cluster stop Directed I -> really-closed;
coherence
proof set F = stop Directed I;
let l be Nat such that
A1: l in dom F;
A2: card Directed I = card I by FUNCT_4:99;
then
A3: dom F = dom I \/ {card I} by AFINSQ_1:89;
A4: dom Directed I = dom I by FUNCT_4:99;
per cases;
suppose l = card I;
then F/.l = F.card Directed I by A2,A1,PARTFUN1:def 6
.= halt SCM+FSA by COMPOS_1:64;
then NIC(F/.l,l) = {l} by AMISTD_1:2;
hence NIC (F/.l, l) c= dom F by A1,ZFMISC_1:31;
end;
suppose l <> card I;
then not l in {card I} by TARSKI:def 1;
then
A5: l in dom I by A3,A1,XBOOLE_0:def 3;
A6: F/.l = F.l by PARTFUN1:def 6,A1
.= (Directed I).l by A4,A5,AFINSQ_1:def 3;
A7: dom I c= dom F by A3,XBOOLE_1:7;
card I in {card I} by TARSKI:def 1;
then
A8: card I in dom F by A3,XBOOLE_0:def 3;
per cases;
suppose I.l = halt SCM+FSA;
then (Directed I).l = goto card I by A5,FUNCT_4:106;
then F/.l = goto card I by A6;
then NIC(F/.l,l) = {card I} by SCMFSA10:33;
hence NIC (F/.l, l) c= dom F by ZFMISC_1:31,A8;
end;
suppose I.l <> halt SCM+FSA;
then
A9: (Directed I).l = I.l by FUNCT_4:105
.= I/.l by A5,PARTFUN1:def 6;
NIC (I/.l, l) c= dom I by A5,AMISTD_1:def 9;
then NIC (I/.l, l) c= dom F by A7,XBOOLE_1:1;
hence NIC (F/.l, l) c= dom F by A6,A9;
end;
end;
end;
end;
registration let I,J be really-closed Program of SCM+FSA;
cluster I ";" J -> really-closed;
coherence;
end;
theorem
for I,J being MacroInstruction of SCM+FSA, n being Nat
st n < LastLoc I holds (I ";" J).n = I.n
proof
let I,J be MacroInstruction of SCM+FSA, l be Nat such that
A1: l < LastLoc I;
LastLoc I in dom I by VALUED_1:30;
then
A2: l in dom I by A1,AFINSQ_1:def 12;
then I.l <> halt SCM+FSA by A1,COMPOS_1:def 15;
hence thesis by A2,Th5;
end;