:: Modifying addresses of instructions of { \bf SCM_FSA }
:: by Andrzej Trybulec and Yatsuka Nakamura
::
:: Received February 14, 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, AMI_3, SCMFSA_2, AMISTD_2, CARD_1,
GRAPHSP, ARYTM_3, RELAT_1, FUNCT_1, FUNCT_4, XBOOLE_0, FSM_1, ARYTM_1,
INT_1, COMPLEX1, PARTFUN1, FINSEQ_1, FINSEQ_2, NAT_1, COMPOS_1;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, ORDINAL1, NUMBERS,
CARD_3, XXREAL_0, XCMPLX_0, NAT_1, NAT_D, VALUED_1, INT_1, INT_2,
RELAT_1, FUNCT_1, PARTFUN1, FUNCT_2, FUNCT_4, FUNCOP_1, FUNCT_7,
FINSEQ_1, FINSEQ_2, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1,
AMI_3, SCMFSA_2, AMISTD_2, AMISTD_5;
constructors DOMAIN_1, XXREAL_0, AMI_3, SCMFSA_2, NAT_D, RELSET_1, VALUED_1,
AMISTD_2, AMISTD_5, PBOOLE, FUNCT_7, MEMSTR_0, FINSEQ_2;
registrations XBOOLE_0, ORDINAL1, RELSET_1, XREAL_0, INT_1, SCMFSA_2, AMI_3,
SCMFSA10, AMISTD_2, VALUED_0, EXTPRO_1, MEMSTR_0, FINSEQ_1, COMPOS_0,
XTUPLE_0, NAT_1;
requirements NUMERALS, REAL, SUBSET;
definitions FUNCT_1, AMISTD_5, COMPOS_0;
equalities SCMFSA_2, MEMSTR_0;
expansions COMPOS_0;
theorems SCMFSA_2, ENUMSET1, TARSKI, SCMFSA_3, VALUED_1, AMISTD_2, SCMFSA10,
FINSEQ_1, ORDINAL1, EXTPRO_1, MEMSTR_0, COMPOS_0;
begin :: Incrementing addresses
reserve L, j, k, l, m, n, p, q for Nat,
A for Data-Location,
I for Instruction of SCM;
registration
let a,b be Int-Location;
cluster a:=b -> ins-loc-free;
coherence
proof
a := b = [1,{},<*a,b*>] by SCMFSA10:2;
hence JumpPart(a:=b) is empty;
end;
cluster AddTo(a,b) -> ins-loc-free;
coherence
proof
AddTo(a,b) = [2,{},<*a,b*>] by SCMFSA10:3;
hence JumpPart AddTo(a,b) is empty;
end;
cluster SubFrom(a,b) -> ins-loc-free;
coherence
proof
SubFrom(a,b) = [3,{},<*a,b*>] by SCMFSA10:4;
hence JumpPart SubFrom(a,b) is empty;
end;
cluster MultBy(a,b) -> ins-loc-free;
coherence
proof
MultBy(a,b) = [4,{},<*a,b*>] by SCMFSA10:5;
hence JumpPart MultBy(a,b) is empty;
end;
cluster Divide(a,b) -> ins-loc-free;
coherence
proof
Divide(a,b) = [5,{},<*a,b*>] by SCMFSA10:6;
hence JumpPart Divide(a,b) is empty;
end;
end;
theorem Th1:
for k,loc being Nat
holds IncAddr(goto loc,k) = goto (loc + k) by SCMFSA10:41;
theorem Th2:
for k,loc being Nat, a being Int-Location
holds IncAddr(a=0_goto loc,k) = a=0_goto (loc + k)
proof
let k,loc be Nat, a be Int-Location;
A1: a=0_goto loc = [7,<* loc *>,<*a*>] by SCMFSA10:7;
A2: a=0_goto (loc + k) = [7,<* loc + k *>,<*a*>] by SCMFSA10:7;
A3: InsCode IncAddr(a=0_goto loc,k) = InsCode(a=0_goto loc) by COMPOS_0:def 9
.= 7 by A1
.= InsCode(a=0_goto(loc + k)) by A2;
A4: AddressPart IncAddr(a=0_goto loc,k) = AddressPart(a=0_goto loc)
by COMPOS_0:def 9
.= <*a*> by A1
.= AddressPart(a=0_goto (loc + k)) by A2;
A5: JumpPart IncAddr(a=0_goto loc,k) = k + JumpPart(a=0_goto loc)
by COMPOS_0:def 9;
JumpPart IncAddr(a=0_goto loc,k) = JumpPart(a=0_goto (loc + k))
proof
thus
A6: dom JumpPart IncAddr(a=0_goto loc,k)
= dom JumpPart(a=0_goto (loc + k)) by A3,COMPOS_0:def 5;
A7: JumpPart(a=0_goto loc) = <*loc*> by A1;
A8: JumpPart(a=0_goto (loc+k)) = <*loc+k*> by A2;
let x be object;
assume
A9: x in dom JumpPart IncAddr(a=0_goto loc,k);
dom <*loc+k*> = {1} by FINSEQ_1:2,38;
then
A10: x = 1 by A9,A6,A8,TARSKI:def 1;
thus (JumpPart IncAddr(a=0_goto loc,k)).x
= k + (JumpPart(a=0_goto loc)).x by A5,A9,VALUED_1:def 2
.= loc + k by A7,A10
.= (JumpPart(a=0_goto(loc + k))).x by A8,A10;
end;
hence thesis by A3,A4,COMPOS_0:1;
end;
theorem Th3:
for k,loc being Nat, a being Int-Location
holds IncAddr(a>0_goto loc,k) = a>0_goto (loc + k)
proof
let k,loc be Nat, a be Int-Location;
A1: a>0_goto loc = [8,<* loc *>,<*a*>] by SCMFSA10:8;
A2: a>0_goto (loc + k) = [8,<* loc + k *>,<*a*>] by SCMFSA10:8;
A3: InsCode IncAddr(a>0_goto loc,k) = InsCode(a>0_goto loc) by COMPOS_0:def 9
.= 8 by A1
.= InsCode(a>0_goto(loc + k)) by A2;
A4: AddressPart IncAddr(a>0_goto loc,k) = AddressPart(a>0_goto loc)
by COMPOS_0:def 9
.= <*a*> by A1
.= AddressPart(a>0_goto (loc + k)) by A2;
A5: JumpPart IncAddr(a>0_goto loc,k) = k + JumpPart(a>0_goto loc)
by COMPOS_0:def 9;
JumpPart IncAddr(a>0_goto loc,k) = JumpPart(a>0_goto (loc + k))
proof
thus
A6: dom JumpPart IncAddr(a>0_goto loc,k)
= dom JumpPart(a>0_goto (loc + k)) by A3,COMPOS_0:def 5;
A7: JumpPart(a>0_goto loc) = <*loc*> by A1;
A8: JumpPart(a>0_goto (loc+k)) = <*loc+k*> by A2;
let x be object;
assume
A9: x in dom JumpPart IncAddr(a>0_goto loc,k);
dom <*loc+k*> = {1} by FINSEQ_1:2,38;
then
A10: x = 1 by A9,A6,A8,TARSKI:def 1;
thus (JumpPart IncAddr(a>0_goto loc,k)).x
= k + (JumpPart(a>0_goto loc)).x by A5,A9,VALUED_1:def 2
.= loc + k by A7,A10
.= (JumpPart(a>0_goto(loc + k))).x by A8,A10;
end;
hence thesis by A3,A4,COMPOS_0:1;
end;
registration
let a,b be Int-Location; let f be FinSeq-Location;
cluster b:=(f,a) -> ins-loc-free;
coherence;
cluster (f,a):=b -> ins-loc-free;
coherence;
end;
registration
let a be Int-Location; let f be FinSeq-Location;
cluster a:=len f -> ins-loc-free;
coherence;
cluster f:=<0,...,0>a -> ins-loc-free;
coherence;
end;
reserve i for Instruction of SCM+FSA;
begin :: Incrementing Addresses in a finite partial state
registration
cluster SCM+FSA -> relocable;
coherence
proof let INS be Instruction of SCM+FSA, j,k be Nat;
let s be State of SCM+FSA;
A1: IC IncIC(Exec(IncAddr(INS,j),s),k)
= IC Exec(IncAddr(INS,j),s) + k by MEMSTR_0:53
.= IC Exec(IncAddr(INS,j+k),IncIC(s,k)) by AMISTD_2:def 3;
InsCode INS = 0 or ... or InsCode INS = 12 by SCMFSA_2:16;
then per cases;
suppose InsCode INS = 0;
then
A2: INS = halt SCM+FSA by SCMFSA_2:95;
then
A3: IncAddr(INS,j) = halt SCM+FSA by COMPOS_0:4;
Exec(IncAddr(INS,j+k),IncIC(s,k))
= Exec(INS,IncIC(s,k)) by A2,COMPOS_0:4
.= IncIC(s,k) by A2,EXTPRO_1:def 3
.= IncIC(Exec(IncAddr(INS,j),s),k) by A3,EXTPRO_1:def 3;
hence thesis;
end;
suppose InsCode INS = 1;
then consider da,db being Int-Location such that
A4: INS = da := db by SCMFSA_2:30;
A5: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= Exec(INS,IncIC(s,k)).f by A4,COMPOS_0:4
.= IncIC(s,k).f by A4,SCMFSA_2:63
.= s.f by SCMFSA_3:4
.= Exec(INS, s).f by A4,SCMFSA_2:63
.= Exec(IncAddr(INS,j), s).f by A4,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now
let d be Int-Location;
per cases;
suppose
A6: da = d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A4,COMPOS_0:4
.= IncIC(s,k).db by A4,A6,SCMFSA_2:63
.= s.db by SCMFSA_3:3
.= Exec(INS, s).d by A4,A6,SCMFSA_2:63
.= Exec(IncAddr(INS,j), s).d by A4,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
suppose
A7: da <> d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A4,COMPOS_0:4
.= IncIC(s,k).d by A4,A7,SCMFSA_2:63
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A4,A7,SCMFSA_2:63
.= Exec(IncAddr(INS,j), s).d by A4,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
end;
hence thesis by A5,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 2;
then consider da,db being Int-Location such that
A8: INS = AddTo(da, db) by SCMFSA_2:31;
A9: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= Exec(INS,IncIC(s,k)).f by A8,COMPOS_0:4
.= IncIC(s,k).f by A8,SCMFSA_2:64
.= s.f by SCMFSA_3:4
.= Exec(INS, s).f by A8,SCMFSA_2:64
.= Exec(IncAddr(INS,j), s).f by A8,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now let d be Int-Location;
per cases;
suppose
A10: da = d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A8,COMPOS_0:4
.= IncIC(s,k).da + IncIC(s,k).db by A10,A8,SCMFSA_2:64
.= s.da + IncIC(s,k).db by SCMFSA_3:3
.= s.da + s.db by SCMFSA_3:3
.= Exec(INS, s).d by A8,A10,SCMFSA_2:64
.= Exec(IncAddr(INS,j), s).d by A8,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
suppose
A11: da <> d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A8,COMPOS_0:4
.= IncIC(s,k).d by A8,A11,SCMFSA_2:64
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A8,A11,SCMFSA_2:64
.= Exec(IncAddr(INS,j), s).d by A8,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
end;
hence thesis by A9,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 3;
then consider da,db being Int-Location such that
A12: INS = SubFrom(da, db) by SCMFSA_2:32;
A13: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= Exec(INS,IncIC(s,k)).f by A12,COMPOS_0:4
.= IncIC(s,k).f by A12,SCMFSA_2:65
.= s.f by SCMFSA_3:4
.= Exec(INS, s).f by A12,SCMFSA_2:65
.= Exec(IncAddr(INS,j), s).f by A12,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now let d be Int-Location;
per cases;
suppose
A14: da = d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A12,COMPOS_0:4
.= IncIC(s,k).da - IncIC(s,k).db by A14,A12,SCMFSA_2:65
.= s.da - IncIC(s,k).db by SCMFSA_3:3
.= s.da - s.db by SCMFSA_3:3
.= Exec(INS, s).d by A12,A14,SCMFSA_2:65
.= Exec(IncAddr(INS,j), s).d by A12,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
suppose
A15: da <> d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A12,COMPOS_0:4
.= IncIC(s,k).d by A12,A15,SCMFSA_2:65
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A12,A15,SCMFSA_2:65
.= Exec(IncAddr(INS,j), s).d by A12,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
end;
hence thesis by A13,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 4;
then consider da,db being Int-Location such that
A16: INS = MultBy(da, db) by SCMFSA_2:33;
A17: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= Exec(INS,IncIC(s,k)).f by A16,COMPOS_0:4
.= IncIC(s,k).f by A16,SCMFSA_2:66
.= s.f by SCMFSA_3:4
.= Exec(INS, s).f by A16,SCMFSA_2:66
.= Exec(IncAddr(INS,j), s).f by A16,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now let d be Int-Location;
per cases;
suppose
A18: da = d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A16,COMPOS_0:4
.= IncIC(s,k).da * IncIC(s,k).db by A18,A16,SCMFSA_2:66
.= s.da * IncIC(s,k).db by SCMFSA_3:3
.= s.da * s.db by SCMFSA_3:3
.= Exec(INS, s).d by A16,A18,SCMFSA_2:66
.= Exec(IncAddr(INS,j), s).d by A16,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
suppose
A19: da <> d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A16,COMPOS_0:4
.= IncIC(s,k).d by A16,A19,SCMFSA_2:66
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A16,A19,SCMFSA_2:66
.= Exec(IncAddr(INS,j), s).d by A16,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
end;
hence thesis by A17,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 5;
then consider da,db being Int-Location such that
A20: INS = Divide(da, db) by SCMFSA_2:34;
A21: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= Exec(INS,IncIC(s,k)).f by A20,COMPOS_0:4
.= IncIC(s,k).f by A20,SCMFSA_2:67
.= s.f by SCMFSA_3:4
.= Exec(INS, s).f by A20,SCMFSA_2:67
.= Exec(IncAddr(INS,j), s).f by A20,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now
let d be Int-Location;
per cases;
suppose
A22: da <> db;
hereby
per cases;
suppose
A23: da = d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
.= IncIC(s,k).da div IncIC(s,k).db by A22,A23,A20,SCMFSA_2:67
.= s.da div IncIC(s,k).db by SCMFSA_3:3
.= s.da div s.db by SCMFSA_3:3
.= Exec(INS, s).d by A20,A22,A23,SCMFSA_2:67
.= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
suppose
A24: db = d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
.= IncIC(s,k).da mod IncIC(s,k).db by A24,A20,SCMFSA_2:67
.= s.da mod IncIC(s,k).db by SCMFSA_3:3
.= s.da mod s.db by SCMFSA_3:3
.= Exec(INS, s).d by A20,A24,SCMFSA_2:67
.= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
suppose
A25: da <> d & db <> d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
.= IncIC(s,k).d by A20,A25,SCMFSA_2:67
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A20,A25,SCMFSA_2:67
.= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
end;
end;
suppose
A26: da = db;
per cases;
suppose
A27: da = d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
.= IncIC(s,k).da mod IncIC(s,k).db by A26,A27,A20,SCMFSA_2:67
.= s.da mod IncIC(s,k).db by SCMFSA_3:3
.= s.da mod s.db by SCMFSA_3:3
.= Exec(INS, s).d by A20,A26,A27,SCMFSA_2:67
.= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
suppose
A28: da <> d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A20,COMPOS_0:4
.= IncIC(s,k).d by A20,A26,A28,SCMFSA_2:67
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A20,A26,A28,SCMFSA_2:67
.= Exec(IncAddr(INS,j), s).d by A20,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
end;
end;
hence thesis by A21,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 6;
then consider loc being Nat such that
A29: INS = goto loc by SCMFSA_2:35;
A30: IncAddr(INS, j+k) = goto (loc + (j+k)) by A29,Th1;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
A31: IncAddr(INS,jj) = goto (loc + jj) by A29,Th1;
A32: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= IncIC(s,k).f by A30,SCMFSA_2:69
.= s.f by SCMFSA_3:4
.= Exec(IncAddr(INS,j), s).f by A31,SCMFSA_2:69
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now let d be Int-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= IncIC(s,k).d by A30,SCMFSA_2:69
.= s.d by SCMFSA_3:3
.= Exec(IncAddr(INS,j), s).d by A31,SCMFSA_2:69
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
hence thesis by A32,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 7;
then consider loc being Nat, da being Int-Location such that
A33: INS = da=0_goto loc by SCMFSA_2:36;
A34: IncAddr(INS, j+k) = da=0_goto (loc + (j+k)) by A33,Th2;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
A35: IncAddr(INS,jj) = da=0_goto (loc + jj) by A33,Th2;
A36: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= IncIC(s,k).f by A34,SCMFSA_2:70
.= s.f by SCMFSA_3:4
.= Exec(IncAddr(INS,j), s).f by A35,SCMFSA_2:70
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now let d be Int-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= IncIC(s,k).d by A34,SCMFSA_2:70
.= s.d by SCMFSA_3:3
.= Exec(IncAddr(INS,j), s).d by A35,SCMFSA_2:70
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
hence thesis by A1,A36,SCMFSA_2:104;
end;
suppose InsCode INS = 8;
then consider loc being Nat, da being Int-Location such that
A37: INS = da>0_goto loc by SCMFSA_2:37;
A38: IncAddr(INS, j+k) = da>0_goto (loc + (j+k)) by A37,Th3;
reconsider jj=j as Element of NAT by ORDINAL1:def 12;
A39: IncAddr(INS, jj) = da>0_goto (loc + jj) by A37,Th3;
A40: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= IncIC(s,k).f by A38,SCMFSA_2:71
.= s.f by SCMFSA_3:4
.= Exec(IncAddr(INS,j), s).f by A39,SCMFSA_2:71
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now let d be Int-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= IncIC(s,k).d by A38,SCMFSA_2:71
.= s.d by SCMFSA_3:3
.= Exec(IncAddr(INS,j), s).d by A39,SCMFSA_2:71
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
hence thesis by A40,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 9;
then consider db,da being Int-Location, f being FinSeq-Location such that
A41: INS = da :=(f, db) by SCMFSA_2:38;
A42: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= Exec(INS,IncIC(s,k)).f by A41,COMPOS_0:4
.= IncIC(s,k).f by A41,SCMFSA_2:72
.= s.f by SCMFSA_3:4
.= Exec(INS, s).f by A41,SCMFSA_2:72
.= Exec(IncAddr(INS,j), s).f by A41,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now let d be Int-Location;
per cases;
suppose
A43: da = d;
consider m being Nat such that
A44: m = |.s.db.| and
A45: Exec(INS, s).da = (s.f)/.m by A41,SCMFSA_2:72;
A46: ex m1 being Nat st
m1 = |.IncIC(s,k).db.| &
Exec(INS,IncIC(s,k)).da = (IncIC(s,k).f)/.m1 by A41,SCMFSA_2:72;
A47: (IncIC(s,k)).db = s.db by SCMFSA_3:3;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A41,COMPOS_0:4
.= (s.f)/.m by A44,A46,A43,A47,SCMFSA_3:4
.= IncIC(Exec(INS, s),k).d by A45,A43,SCMFSA_3:3
.= IncIC(Exec(IncAddr(INS,j),s),k).d by A41,COMPOS_0:4;
end;
suppose
A48: da <> d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A41,COMPOS_0:4
.= IncIC(s,k).d by A41,A48,SCMFSA_2:72
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A41,A48,SCMFSA_2:72
.= Exec(IncAddr(INS,j), s).d by A41,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
end;
hence thesis by A42,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 10;
then consider db,da being Int-Location, f being FinSeq-Location such that
A49: INS = (f, db):=da by SCMFSA_2:39;
A50: now let g be FinSeq-Location;
consider m being Nat such that
A51: m = |.s.db.| and
A52: Exec(INS, s).f = s.f+*(m,s.da) by A49,SCMFSA_2:73;
A53: ex m1 being Nat
st m1 = |.IncIC(s,k).db.| &
Exec(INS,IncIC(s,k)).f = IncIC(s,k).f +*(m1,IncIC(s,k).da)
by A49,SCMFSA_2:73;
per cases;
suppose
A54: f = g;
A55: IncIC(s,k).f = s.f & IncIC(s,k).db = s.db by SCMFSA_3:3,4;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).g
= Exec(INS, IncIC(s,k)).g by A49,COMPOS_0:4
.= s.f+*(m,s.da) by A51,A53,A54,A55,SCMFSA_3:3
.= IncIC(Exec(INS, s),k).g by A52,A54,SCMFSA_3:4
.= IncIC(Exec(IncAddr(INS,j),s),k).g by A49,COMPOS_0:4;
end;
suppose
A56: f <> g;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).g
= Exec(INS,IncIC(s,k)).g by A49,COMPOS_0:4
.= IncIC(s,k).g by A49,A56,SCMFSA_2:73
.= s.g by SCMFSA_3:4
.= Exec(INS, s).g by A49,A56,SCMFSA_2:73
.= Exec(IncAddr(INS,j), s).g by A49,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).g by SCMFSA_3:4;
end;
end;
now let d be Int-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A49,COMPOS_0:4
.= IncIC(s,k).d by A49,SCMFSA_2:73
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A49,SCMFSA_2:73
.= Exec(IncAddr(INS,j), s).d by A49,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
hence thesis by A50,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 11;
then consider da being Int-Location, f being FinSeq-Location such that
A57: INS = da :=len f by SCMFSA_2:40;
A58: now let f be FinSeq-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).f
= Exec(INS,IncIC(s,k)).f by A57,COMPOS_0:4
.= IncIC(s,k).f by A57,SCMFSA_2:74
.= s.f by SCMFSA_3:4
.= Exec(INS, s).f by A57,SCMFSA_2:74
.= Exec(IncAddr(INS,j), s).f by A57,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).f by SCMFSA_3:4;
end;
now let d be Int-Location;
per cases;
suppose
A59: da = d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A57,COMPOS_0:4
.= len(IncIC(s,k).f) by A59,A57,SCMFSA_2:74
.= len(s.f) by SCMFSA_3:4
.= Exec(INS, s).d by A57,A59,SCMFSA_2:74
.= IncIC(Exec(INS, s),k).d by SCMFSA_3:3
.= IncIC(Exec(IncAddr(INS,j),s),k).d by A57,COMPOS_0:4;
end;
suppose
A60: da <> d;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A57,COMPOS_0:4
.= IncIC(s,k).d by A57,A60,SCMFSA_2:74
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A57,A60,SCMFSA_2:74
.= Exec(IncAddr(INS,j), s).d by A57,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
end;
hence thesis by A58,A1,SCMFSA_2:104;
end;
suppose InsCode INS = 12;
then consider da being Int-Location, f being FinSeq-Location such that
A61: INS = f:=<0,...,0>da by SCMFSA_2:41;
A62: now let g be FinSeq-Location;
A63: (ex m being Nat
st m = |.s.da.| & Exec(INS, s ).f = m|-> 0 ) &
ex m being Nat st m = |.IncIC(s,k).da.|
& Exec (INS,IncIC(s,k)).f = m |-> 0 by A61,SCMFSA_2:75;
per cases;
suppose
A64: f = g;
A65: IncIC(s,k).da = s.da by SCMFSA_3:3;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).g
= Exec(INS, IncIC(s,k)).g by A61,COMPOS_0:4
.= IncIC(Exec(INS, s),k).g by A63,A64,A65,SCMFSA_3:4
.= IncIC(Exec(IncAddr(INS,j),s),k).g by A61,COMPOS_0:4;
end;
suppose
A66: f <> g;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).g
= Exec(INS,IncIC(s,k)).g by A61,COMPOS_0:4
.= IncIC(s,k).g by A61,A66,SCMFSA_2:75
.= s.g by SCMFSA_3:4
.= Exec(INS, s).g by A61,A66,SCMFSA_2:75
.= Exec(IncAddr(INS,j), s).g by A61,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).g by SCMFSA_3:4;
end;
end;
now let d be Int-Location;
thus Exec(IncAddr(INS,j+k),IncIC(s,k)).d
= Exec(INS,IncIC(s,k)).d by A61,COMPOS_0:4
.= IncIC(s,k).d by A61,SCMFSA_2:75
.= s.d by SCMFSA_3:3
.= Exec(INS, s).d by A61,SCMFSA_2:75
.= Exec(IncAddr(INS,j), s).d by A61,COMPOS_0:4
.= IncIC(Exec(IncAddr(INS,j),s),k).d by SCMFSA_3:3;
end;
hence thesis by A62,A1,SCMFSA_2:104;
end;
end;
end;
theorem
not InsCode i in {6,7,8} implies IncAddr(i,k) = i
proof
assume not InsCode i in {6,7,8};
then
A1: InsCode i <> 6 & InsCode i <> 7 & InsCode i <> 8 by ENUMSET1:def 1;
InsCode i = 0 or ... or InsCode i = 12 by SCMFSA_2:16;
then per cases by A1;
suppose InsCode i = 0;
then i = halt SCM+FSA by SCMFSA_2:95;
hence thesis by COMPOS_0:4;
end;
suppose
InsCode i = 1;
then consider da,db being Int-Location such that
A2: i = da := db by SCMFSA_2:30;
thus thesis by A2,COMPOS_0:4;
end;
suppose
InsCode i = 2;
then consider da,db being Int-Location such that
A3: i = AddTo(da, db) by SCMFSA_2:31;
thus thesis by A3,COMPOS_0:4;
end;
suppose
InsCode i = 3;
then consider da,db being Int-Location such that
A4: i = SubFrom(da, db) by SCMFSA_2:32;
thus thesis by A4,COMPOS_0:4;
end;
suppose
InsCode i = 4;
then consider da,db being Int-Location such that
A5: i = MultBy(da, db) by SCMFSA_2:33;
thus thesis by A5,COMPOS_0:4;
end;
suppose
InsCode i = 5;
then consider da,db being Int-Location such that
A6: i = Divide(da, db) by SCMFSA_2:34;
thus thesis by A6,COMPOS_0:4;
end;
suppose
InsCode i = 9;
then consider db,da being Int-Location, f being FinSeq-Location such that
A7: i = da :=(f, db) by SCMFSA_2:38;
thus thesis by A7,COMPOS_0:4;
end;
suppose
InsCode i = 10;
then consider db,da being Int-Location, f being FinSeq-Location such that
A8: i = (f, db):=da by SCMFSA_2:39;
thus thesis by A8,COMPOS_0:4;
end;
suppose
InsCode i = 11;
then consider da being Int-Location, f being FinSeq-Location such that
A9: i = da :=len f by SCMFSA_2:40;
thus thesis by A9,COMPOS_0:4;
end;
suppose
InsCode i = 12;
then consider da being Int-Location, f being FinSeq-Location such that
A10: i = f:=<0,...,0>da by SCMFSA_2:41;
thus thesis by A10,COMPOS_0:4;
end;
end;