:: The { \bf SCM_FSA } computer
:: by Andrzej Trybulec , Yatsuka Nakamura and Piotr Rudnicki
::
:: Received February 7, 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, STRUCT_0, AMI_1, RELAT_1, SCMFSA_1, FUNCT_7, XBOOLE_0,
TARSKI, AMI_3, ZFMISC_1, SUBSET_1, CARD_1, CAT_1, ARYTM_1, ARYTM_3,
NAT_1, FINSET_1, FUNCT_1, AMI_2, XXREAL_0, FINSEQ_1, GRAPHSP, FSM_1,
FUNCT_4, FUNCOP_1, INT_1, CARD_3, COMPLEX1, PARTFUN1, FINSEQ_2, GLIB_000,
SCMFSA_2, RECDEF_2, GOBRD13, MEMSTR_0, AMISTD_4, SCMPDS_5;
notations TARSKI, XBOOLE_0, ENUMSET1, ZFMISC_1, XTUPLE_0, XFAMILY, SUBSET_1,
ORDINAL1, XCMPLX_0, XXREAL_0, INT_1, NAT_1, RELAT_1, MCART_1, CARD_1,
CARD_3, INT_2, FINSEQ_1, FUNCOP_1, STRUCT_0, FUNCT_1, RELSET_1, PARTFUN1,
FUNCT_2, FINSET_1, FUNCT_4, FINSEQ_2, FUNCT_7, RECDEF_2, NUMBERS,
MEMSTR_0, COMPOS_0, COMPOS_1, AMISTD_4, EXTPRO_1, SCM_INST, SCMFSA_I,
AMI_2, AMI_3, SCMFSA_1;
constructors WELLORD2, DOMAIN_1, REAL_1, FINSEQ_4, AMI_3, SCMFSA_1, RELSET_1,
PRE_POLY, FUNCT_7, NAT_D, AMISTD_4, XTUPLE_0, XFAMILY;
registrations RELAT_1, FUNCT_1, ORDINAL1, FUNCOP_1, XREAL_0, NAT_1, INT_1,
CARD_3, STRUCT_0, AMI_3, SCMFSA_1, FINSET_1, CARD_2, RELSET_1, EXTPRO_1,
MEMSTR_0, COMPOS_0, SCM_INST, SCMFSA_I, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions TARSKI, EXTPRO_1, WELLORD2, XBOOLE_0, FUNCT_1, AMISTD_4;
equalities TARSKI, EXTPRO_1, COMPOS_1, XBOOLE_0, AMI_2, AMI_3, STRUCT_0,
SCMFSA_1, FUNCOP_1, MEMSTR_0, COMPOS_0, SCM_INST, SCMFSA_I;
expansions EXTPRO_1, AMI_2, FUNCT_1, MEMSTR_0, COMPOS_0;
theorems SCMFSA_1, TARSKI, INT_1, RELAT_1, AMI_5, FUNCT_2, FUNCT_4, CARD_3,
FUNCOP_1, FUNCT_1, AMI_3, NAT_1, CARD_1, AMI_2, FUNCT_7, ZFMISC_1,
ORDINAL1, XBOOLE_0, XBOOLE_1, XREAL_1, XXREAL_0, NUMBERS, FINSET_1,
PARTFUN1, MEMSTR_0, SCMFSA_I, SCM_INST, XTUPLE_0, SUBSET_1;
schemes FUNCT_2;
begin :: The SCM+FSA Computer
reserve J,J1,K for Element of Segm 13,
b,b1,b2,c,c1,c2 for Element of SCM+FSA-Data-Loc,
f,f1,f2 for Element of SCM+FSA-Data*-Loc;
definition
func SCM+FSA -> strict AMI-Struct over Segm 3 equals
AMI-Struct(# SCM+FSA-Memory,In (NAT,SCM+FSA-Memory),
SCM+FSA-Instr,
SCM+FSA-OK,SCM*-VAL,SCM+FSA-Exec#);
coherence;
end;
registration
cluster SCM+FSA -> non empty with_non-empty_values;
coherence;
end;
registration
cluster SCM+FSA -> with_non_trivial_Instructions;
coherence
proof
A1: [0,{},{}] in SCM+FSA-Instr by SCMFSA_I:3;
[6,<*0*>,{}] in SCM-Instr by SCM_INST:2;
then
A2: [6,<*0*>,{}] in SCM+FSA-Instr by SCMFSA_I:1;
[0,{},{}] <> [6,<*0*>,{}] by XTUPLE_0:3;
hence the InstructionsF of SCM+FSA is non trivial by A1,A2,ZFMISC_1:def 10;
end;
end;
theorem Th1:
IC SCM+FSA = NAT by SCMFSA_1:5,SUBSET_1:def 8;
begin :: The Memory Structure
reserve k for Nat,
J,K,L for Element of Segm 13,
O,P,R for Element of Segm 9;
notation
synonym Int-Locations↑ for SCM+FSA-Data-Loc;
end;
definition
redefine func Int-Locations -> Subset of SCM+FSA; :: redefines Int-Locations (SCMFSA_2, synonym) → SCM+FSA-Data-Loc (SCMFSA_1, synonym) → SCM-Data-Loc (SCM_INST, definition)
coherence
proof
Int-Locations = SCM+FSA-Data-Loc;
hence thesis;
end;
::$CD
func FinSeq-Locations -> Subset of SCM+FSA equals
SCM+FSA-Data*-Loc;
coherence;
end;
registration
cluster Int-like for Object of SCM+FSA;
existence
proof
reconsider x = the Element of SCM+FSA-Data-Loc as Object of SCM+FSA;
take x;
thus thesis;
end;
end;
definition
mode Int-Location is Int-like Object of SCM+FSA;
::$CD
mode FinSeq-Location -> Object of SCM+FSA means
:Def3:
it in SCM+FSA-Data*-Loc;
existence
proof
set x =the Element of SCM+FSA-Data*-Loc;
reconsider x as Object of SCM+FSA;
take x;
thus thesis;
end;
end;
reserve da for Int-Location,
fa for FinSeq-Location,
x,y for set;
::$CT 5
definition
let k be Nat;
func intloc k -> Int-Location equals
dl.k;
coherence
proof
A1: Int-Locations = SCM+FSA-Data-Loc;
dl.k in SCM-Data-Loc by AMI_2:def 16;
hence thesis by A1;
end;
func fsloc k -> FinSeq-Location equals
-(k+1);
coherence
proof
-(k+1) < -0 by XREAL_1:24;
then -(k+1) in INT & not -(k+1) in NAT by INT_1:def 1;
then -(k+1) in SCM+FSA-Data*-Loc by XBOOLE_0:def 5;
hence thesis by Def3;
end;
end;
theorem
for k1,k2 being Nat st k1 <> k2 holds fsloc k1 <> fsloc k2;
theorem
for dl being Int-Location ex i being Nat st dl = intloc i
proof
let dl be Int-Location;
dl in SCM-Data-Loc by AMI_2:def 16;
then reconsider D = dl as Data-Location;
consider i being Nat such that
A1: D = dl.i by AMI_5:1;
take i;
thus thesis by A1;
end;
theorem Th4:
for fl being FinSeq-Location ex i being Nat st fl =
fsloc i
proof
let fl be FinSeq-Location;
A1: fl in SCM+FSA-Data*-Loc by Def3;
then consider k being Nat such that
A2: fl = k or fl = -k by INT_1:def 1;
k <> 0 by A1,A2,XBOOLE_0:def 5;
then consider i being Nat such that
A3: k = i+1 by NAT_1:6;
reconsider i as Nat;
take i;
thus thesis by A1,A2,A3,XBOOLE_0:def 5;
end;
registration
cluster FinSeq-Locations -> infinite;
coherence
proof
deffunc U(Nat) = fsloc $1;
consider f being sequence of the carrier of SCM+FSA such that
A1: for k being Element of NAT holds f.k = U(k) from FUNCT_2:sch 4;
NAT, FinSeq-Locations are_equipotent
proof
take f;
thus f is one-to-one
proof
let x1,x2 be object such that
A2: x1 in dom f & x2 in dom f and
A3: f.x1 = f.x2;
reconsider k1 = x1,k2 = x2 as Element of NAT by A2;
fsloc k1 = f.k1 by A1
.= fsloc k2 by A1,A3;
hence thesis;
end;
thus dom f = NAT by FUNCT_2:def 1;
thus rng f c= FinSeq-Locations
proof
let y be object;
assume y in rng f;
then consider x be object such that
A4: x in dom f and
A5: y = f.x by FUNCT_1:def 3;
reconsider x as Element of NAT by A4;
y = fsloc x by A1,A5;
hence thesis by Def3;
end;
thus FinSeq-Locations c= rng f
proof
let y be object;
assume y in FinSeq-Locations;
then y is FinSeq-Location by Def3;
then consider i being Nat such that
A6: y = fsloc i by Th4;
reconsider i as Element of NAT by ORDINAL1:def 12;
i in NAT;
then
A7: i in dom f by FUNCT_2:def 1;
y = f.i by A1,A6;
hence thesis by A7,FUNCT_1:def 3;
end;
end;
hence thesis by CARD_1:38;
end;
end;
theorem Th5:
for I being Int-Location holds I is Data-Location
proof
let I be Int-Location;
I in SCM-Data-Loc by AMI_2:def 16;
hence thesis;
end;
theorem Th6:
for l being Int-Location holds Values l = INT
proof
let l be Int-Location;
l in SCM-Data-Loc by AMI_2:def 16;
hence thesis by SCMFSA_1:10;
end;
theorem Th7:
for l being FinSeq-Location holds Values l = INT*
proof
let l be FinSeq-Location;
l in SCM+FSA-Data*-Loc by Def3;
hence thesis by SCMFSA_1:11;
end;
reserve la,lb for Nat,
La for Nat,
i for Instruction of SCM+FSA,
I for Instruction of SCM,
l for Nat,
LA,LB for Nat,
dA,dB,dC,dD for Element of SCM+FSA-Data-Loc,
DA,DB,DC for Element of SCM-Data-Loc,
fA,fB,fC for Element of SCM+FSA-Data*-Loc,
f,g for FinSeq-Location,
A,B for Data-Location,
a,b,c,db for Int-Location;
begin :: The Instruction Structure
::$CT 2
theorem Th8:
for I being Instruction of SCM+FSA st InsCode I <= 8 holds
I is Instruction of SCM
proof
let I be Instruction of SCM+FSA;
assume
A1: InsCode I <= 8;
now
assume I in { [K,{},<*dC,fB*>] : K in {11,12} };
then consider K,dC,fB such that
A2: I = [K,{},<*dC,fB*>] and
A3: K in {11,12};
A4: I`1_3 = K by A2;
K = 12 or K = 11 by A3,TARSKI:def 2;
hence contradiction by A1,A4;
end;
then
A5: I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc
: L in {9,10} }
by XBOOLE_0:def 3;
now
assume I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc
: L in {9,10} };
then consider L be Element of Segm 13,
dA,dB be Element of SCM+FSA-Data-Loc,fA be Element of SCM+FSA-Data*-Loc
such that
A6: I = [L,{},<*dB,fA,dA*>] and
A7: L in {9,10};
A8: I`1_3 = L by A6;
L = 9 or L = 10 by A7,TARSKI:def 2;
hence contradiction by A1,A8;
end;
hence thesis by A5,XBOOLE_0:def 3;
end;
theorem Th9:
for I being Instruction of SCM+FSA holds InsCode I <= 12
proof
let I be Instruction of SCM+FSA;
A1: I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc
: L in {9,10} }
or I in { [K,{},<*dC,fB*>] : K in {11,12} }
by XBOOLE_0:def 3;
per cases by A1,XBOOLE_0:def 3;
suppose
I in SCM-Instr;
then reconsider i = I as Instruction of SCM;
InsCode i <= 8 by AMI_5:5;
hence thesis by XXREAL_0:2;
end;
suppose
I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc:
L in {9,10} };
then consider L be Element of Segm 13,
dA,dB be Element of SCM+FSA-Data-Loc,fA be Element of SCM+FSA-Data*-Loc
such that
A2: I = [L,{},<*dB,fA,dA*>] and
A3: L in {9,10};
A4: I`1_3 = L by A2;
L = 9 or L = 10 by A3,TARSKI:def 2;
hence thesis by A4;
end;
suppose
I in { [K,{},<*dC,fB*>] : K in {11,12} };
then consider K,dC,fB such that
A5: I = [K,{},<*dC,fB*>] and
A6: K in {11,12};
A7: I`1_3 = K by A5;
K=11 or K=12 by A6,TARSKI:def 2;
hence thesis by A7;
end;
end;
theorem Th10:
for I being Instruction of SCM holds I is Instruction of SCM+FSA
proof
let I be Instruction of SCM;
I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc
: L in {9,10} }
by XBOOLE_0:def 3;
hence thesis by XBOOLE_0:def 3;
end;
definition
let a,b;
func a := b -> Instruction of SCM+FSA means
:Def6:
ex A,B st a = A & b = B & it = A:=B;
existence
proof
reconsider A = a, B = b as Data-Location by Th5;
reconsider i = A:=B as Instruction of SCM+FSA by Th10;
take i,A,B;
thus thesis;
end;
correctness;
func AddTo(a,b) -> Instruction of SCM+FSA means
:Def7:
ex A,B st a = A & b = B & it = AddTo(A,B);
existence
proof
reconsider A = a, B = b as Data-Location by Th5;
reconsider i = AddTo(A,B) as Instruction of SCM+FSA by Th10;
take i,A,B;
thus thesis;
end;
correctness;
func SubFrom(a,b) -> Instruction of SCM+FSA means
:Def8:
ex A,B st a = A & b = B & it = SubFrom(A,B);
existence
proof
reconsider A = a, B = b as Data-Location by Th5;
reconsider i = SubFrom(A,B) as Instruction of SCM+FSA by Th10;
take i,A,B;
thus thesis;
end;
correctness;
func MultBy(a,b) -> Instruction of SCM+FSA means
:Def9:
ex A,B st a = A & b = B & it = MultBy(A,B);
existence
proof
reconsider A = a, B = b as Data-Location by Th5;
reconsider i = MultBy(A,B) as Instruction of SCM+FSA by Th10;
take i,A,B;
thus thesis;
end;
correctness;
func Divide(a,b) -> Instruction of SCM+FSA means
:Def10:
ex A,B st a = A & b = B & it = Divide(A,B);
existence
proof
reconsider A = a, B = b as Data-Location by Th5;
reconsider i = Divide(A,B) as Instruction of SCM+FSA by Th10;
take i,A,B;
thus thesis;
end;
correctness;
end;
definition
let la be Nat;
func goto la -> Instruction of SCM+FSA equals
SCM-goto la;
coherence by Th10;
let a;
func a=0_goto la -> Instruction of SCM+FSA means
:Def12:
ex A st a = A & it = A=0_goto la;
existence
proof
reconsider A = a as Data-Location by Th5;
reconsider i = A=0_goto la as Instruction of SCM+FSA by Th10;
take i,A;
thus thesis;
end;
correctness;
func a>0_goto la -> Instruction of SCM+FSA means
:Def13:
ex A st a = A & it = A>0_goto la;
existence
proof
reconsider A = a as Data-Location by Th5;
reconsider i = A>0_goto la as Instruction of SCM+FSA by Th10;
take i,A;
thus thesis;
end;
correctness;
end;
definition
let c,i be Int-Location;
let a be FinSeq-Location;
func c:=(a,i) -> Instruction of SCM+FSA equals
[9,{},<*c,a,i*>];
coherence
proof
reconsider A=a as Element of SCM+FSA-Data*-Loc by Def3;
reconsider C=c, I=i as Element of SCM-Data-Loc by AMI_2:def 16;
9 in {9,10} by TARSKI:def 2;
then [9,{},<*C,A,I*>] in SCM+FSA-Instr by SCMFSA_I:4;
hence thesis;
end;
func (a,i):=c -> Instruction of SCM+FSA equals
[10,{},<*c,a,i*>];
coherence
proof
reconsider A=a as Element of SCM+FSA-Data*-Loc by Def3;
reconsider C=c, I=i as Element of SCM-Data-Loc by AMI_2:def 16;
10 in {9,10} by TARSKI:def 2;
then [10,{},<*C,A,I*>] in SCM+FSA-Instr by SCMFSA_I:4;
hence thesis;
end;
end;
definition
let i be Int-Location;
let a be FinSeq-Location;
func i:=len a -> Instruction of SCM+FSA equals
[11,{},<*i,a*>];
coherence
proof
reconsider A=a as Element of SCM+FSA-Data*-Loc by Def3;
reconsider I=i as Element of SCM-Data-Loc by AMI_2:def 16;
11 in {11,12} by TARSKI:def 2;
then [11,{},<*I,A*>] in SCM+FSA-Instr by SCMFSA_I:5;
hence thesis;
end;
func a:=<0,...,0>i -> Instruction of SCM+FSA equals
[12,{},<*i,a*>];
coherence
proof
reconsider A=a as Element of SCM+FSA-Data*-Loc by Def3;
reconsider I=i as Element of SCM-Data-Loc by AMI_2:def 16;
12 in {11,12} by TARSKI:def 2;
then [12,{},<*I,A*>] in SCM+FSA-Instr by SCMFSA_I:5;
hence thesis;
end;
end;
theorem
InsCode (a:=b) = 1
proof
ex A,B st a = A & b = B & a:=b = A:=B by Def6;
hence thesis;
end;
theorem
InsCode (AddTo(a,b)) = 2
proof
ex A,B st a = A & b = B & AddTo(a,b) = AddTo(A,B) by Def7;
hence thesis;
end;
theorem
InsCode (SubFrom(a,b)) = 3
proof
ex A,B st a = A & b = B & SubFrom(a,b) = SubFrom(A,B) by Def8;
hence thesis;
end;
theorem
InsCode (MultBy(a,b)) = 4
proof
ex A,B st a = A & b = B & MultBy(a,b) = MultBy(A,B) by Def9;
hence thesis;
end;
theorem
InsCode (Divide(a,b)) = 5
proof
ex A,B st a = A & b = B & Divide(a,b) = Divide(A,B) by Def10;
hence thesis;
end;
theorem
InsCode (goto lb) = 6;
theorem
InsCode (a=0_goto lb) = 7
proof
ex A st a= A & a=0_goto lb = A=0_goto lb by Def12;
hence thesis;
end;
theorem
InsCode (a>0_goto lb) = 8
proof
ex A st a= A & a>0_goto lb = A>0_goto lb by Def13;
hence thesis;
end;
theorem
InsCode (c:=(fa,a)) = 9;
theorem
InsCode ((fa,a):=c) = 10;
theorem
InsCode (a:=len fa) = 11;
theorem
InsCode (fa:=<0,...,0>a) = 12;
theorem Th23:
for ins being Instruction of SCM+FSA st InsCode ins = 1 holds ex
da,db st ins = da:=db
proof
let ins be Instruction of SCM+FSA;
assume
A1: InsCode ins = 1;
then reconsider I = ins as Instruction of SCM by Th8;
consider A,B such that
A2: I = A:=B by A1,AMI_5:8;
A3: Int-Locations = SCM+FSA-Data-Loc;
A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;
then reconsider da = A, db = B as Int-Location by A3;
take da,db;
thus thesis by A2,Def6;
end;
theorem Th24:
for ins being Instruction of SCM+FSA st InsCode ins = 2 holds ex
da,db st ins = AddTo(da,db)
proof
let ins be Instruction of SCM+FSA;
assume
A1: InsCode ins = 2;
then reconsider I = ins as Instruction of SCM by Th8;
consider A,B such that
A2: I = AddTo(A,B) by A1,AMI_5:9;
A3: Int-Locations = SCM+FSA-Data-Loc;
A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;
then reconsider da = A, db = B as Int-Location by A3;
take da,db;
thus thesis by A2,Def7;
end;
theorem Th25:
for ins being Instruction of SCM+FSA st InsCode ins = 3 holds ex
da,db st ins = SubFrom(da,db)
proof
let ins be Instruction of SCM+FSA;
assume
A1: InsCode ins = 3;
then reconsider I = ins as Instruction of SCM by Th8;
consider A,B such that
A2: I = SubFrom(A,B) by A1,AMI_5:10;
A3: Int-Locations = SCM+FSA-Data-Loc;
A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;
then reconsider da = A, db = B as Int-Location by A3;
take da,db;
thus thesis by A2,Def8;
end;
theorem Th26:
for ins being Instruction of SCM+FSA st InsCode ins = 4 holds ex
da,db st ins = MultBy(da,db)
proof
let ins be Instruction of SCM+FSA;
assume
A1: InsCode ins = 4;
then reconsider I = ins as Instruction of SCM by Th8;
consider A,B such that
A2: I = MultBy(A,B) by A1,AMI_5:11;
A3: Int-Locations = SCM+FSA-Data-Loc;
A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;
then reconsider da = A, db = B as Int-Location by A3;
take da,db;
thus thesis by A2,Def9;
end;
theorem Th27:
for ins being Instruction of SCM+FSA st InsCode ins = 5 holds ex
da,db st ins = Divide(da,db)
proof
let ins be Instruction of SCM+FSA;
assume
A1: InsCode ins = 5;
then reconsider I = ins as Instruction of SCM by Th8;
consider A,B such that
A2: I = Divide(A,B) by A1,AMI_5:12;
A3: Int-Locations = SCM+FSA-Data-Loc;
A in SCM-Data-Loc & B in SCM-Data-Loc by AMI_2:def 16;
then reconsider da = A, db = B as Int-Location by A3;
take da,db;
thus thesis by A2,Def10;
end;
theorem Th28:
for ins being Instruction of SCM+FSA st InsCode ins = 6 holds ex
lb st ins = goto lb
proof
let ins be Instruction of SCM+FSA;
assume
A1: InsCode ins = 6;
then reconsider I = ins as Instruction of SCM by Th8;
consider La being Nat such that
A2: I = SCM-goto La by A1,AMI_5:13;
take La;
thus thesis by A2;
end;
theorem Th29:
for ins being Instruction of SCM+FSA st InsCode ins = 7 holds ex
lb,da st ins = da=0_goto lb
proof
let ins be Instruction of SCM+FSA;
assume
A1: InsCode ins = 7;
then reconsider I = ins as Instruction of SCM by Th8;
consider La being Nat, A such that
A2: I = A=0_goto La by A1,AMI_5:14;
A3: Int-Locations = SCM+FSA-Data-Loc;
A in SCM-Data-Loc by AMI_2:def 16;
then reconsider da = A as Int-Location by A3;
take La,da;
thus thesis by A2,Def12;
end;
theorem Th30:
for ins being Instruction of SCM+FSA st InsCode ins = 8 holds ex
lb,da st ins = da>0_goto lb
proof
let ins be Instruction of SCM+FSA;
assume
A1: InsCode ins = 8;
then reconsider I = ins as Instruction of SCM by Th8;
consider La being Nat,A such that
A2: I = A>0_goto La by A1,AMI_5:15;
A3: Int-Locations = SCM+FSA-Data-Loc;
A in SCM-Data-Loc by AMI_2:def 16;
then reconsider da = A as Int-Location by A3;
take La,da;
thus thesis by A2,Def13;
end;
theorem Th31:
for ins being Instruction of SCM+FSA st InsCode ins = 9 holds ex
a,b,fa st ins = b:=(fa,a)
proof
let ins be Instruction of SCM+FSA such that
A1: InsCode ins = 9;
A2: now
assume ins in { [K,{},<*dC,fB*>] : K in {11,12} };
then consider K,dC,fB such that
A3: ins = [K,{},<*dC,fB*>] and
A4: K in {11,12};
K = 11 or K = 12 by A4,TARSKI:def 2;
hence contradiction by A1,A3;
end;
ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc
: L in {9,10} } or
ins in { [K,{},<*dC,fB*>] : K in {11,12} }
by XBOOLE_0:def 3;
then ins in SCM-Instr or ins in { [L,{},<*dB,fA,dA*>] : L in {9,10} } by A2,
XBOOLE_0:def 3;
then consider L be Element of Segm 13,
dA,dB be Element of SCM+FSA-Data-Loc,fA be Element of SCM+FSA-Data*-Loc
such that
A5: ins = [L,{},<*dB,fA,dA*>] and
L in {9,10} by A1,AMI_5:5;
reconsider f=fA as FinSeq-Location by Def3;
reconsider c = dB, b = dA as Int-Location by AMI_2:def 16;
take b,c,f;
thus thesis by A1,A5;
end;
theorem Th32:
for ins being Instruction of SCM+FSA st InsCode ins = 10 holds
ex a,b,fa st ins = (fa,a):=b
proof
let ins be Instruction of SCM+FSA such that
A1: InsCode ins = 10;
A2: now
assume ins in { [K,{},<*dC,fB*>] : K in {11,12} };
then consider K,dC,fB such that
A3: ins = [K,{},<*dC,fB*>] and
A4: K in {11,12};
K = 11 or K = 12 by A4,TARSKI:def 2;
hence contradiction by A1,A3;
end;
ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc:
L in {9,10} } or
ins in { [K,{},<*dC,fB*>] : K in {11,12} } by XBOOLE_0:def 3;
then ins in SCM-Instr or ins in { [L,{},<*dB,fA,dA*>] : L in {9,10} } by A2,
XBOOLE_0:def 3;
then consider L be Element of Segm 13,
dA,dB be Element of SCM+FSA-Data-Loc,fA be Element of SCM+FSA-Data*-Loc
such that
A5: ins = [L,{},<*dB,fA,dA*>] and
L in {9,10} by A1,AMI_5:5;
reconsider f=fA as FinSeq-Location by Def3;
reconsider c = dB, b = dA as Int-Location by AMI_2:def 16;
take b,c,f;
thus thesis by A1,A5;
end;
theorem Th33:
for ins being Instruction of SCM+FSA st InsCode ins = 11 holds
ex a,fa st ins = a:=len fa
proof
let ins be Instruction of SCM+FSA such that
A1: InsCode ins = 11;
A2: now
assume ins in { [L,{},<*dB,fA,dA*>] : L in {9,10} };
then consider K be Element of Segm 13,
dA,dB be Element of SCM+FSA-Data-Loc,fA be Element of SCM+FSA-Data*-Loc
such that
A3: ins = [K,{},<*dB,fA,dA*>] and
A4: K in {9,10};
ins`1_3 = K by A3;
hence contradiction by A1,A4,TARSKI:def 2;
end;
A5: ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc :
L in {9,10} } or
ins in { [K,{},<*dC,fB*>] : K in {11,12} } by XBOOLE_0:def 3;
not ins in SCM-Instr by A1,AMI_5:5;
then consider K,dB,fA such that
A6: ins = [K,{},<*dB,fA*>] and
K in {11,12} by A5,A2,XBOOLE_0:def 3;
reconsider f=fA as FinSeq-Location by Def3;
reconsider c = dB as Int-Location by AMI_2:def 16;
take c,f;
thus thesis by A1,A6;
end;
theorem Th34:
for ins being Instruction of SCM+FSA st InsCode ins = 12 holds
ex a,fa st ins = fa:=<0,...,0>a
proof
let ins be Instruction of SCM+FSA such that
A1: InsCode ins = 12;
A2: now
assume ins in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc:
L in {9,10} };
then consider K be Element of Segm 13,
dA,dB be Element of SCM+FSA-Data-Loc,fA be Element of SCM+FSA-Data*-Loc
such that
A3: ins = [K,{},<*dB,fA,dA*>] and
A4: K in {9,10};
ins`1_3 = K by A3;
hence contradiction by A1,A4,TARSKI:def 2;
end;
A5: ins in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc :
L in {9,10} } or
ins in { [K,{},<*dC,fB*>] : K in {11,12} } by XBOOLE_0:def 3;
not ins in SCM-Instr by A1,AMI_5:5;
then consider K,dB,fA such that
A6: ins = [K,{},<*dB,fA*>] and
K in {11,12} by A5,A2,XBOOLE_0:def 3;
reconsider f=fA as FinSeq-Location by Def3;
reconsider c = dB as Int-Location by AMI_2:def 16;
take c,f;
thus thesis by A1,A6;
end;
begin :: Relationship to {\bf SCM}
reserve S for State of SCM,
s,s1 for State of SCM+FSA;
theorem
for s being State of SCM+FSA, d being Int-Location holds d in dom s
proof
let s be State of SCM+FSA, d be Int-Location;
dom s = the carrier of SCM+FSA by PARTFUN1:def 2;
hence thesis;
end;
theorem
f in dom s
proof
dom s = SCM+FSA-Memory by PARTFUN1:def 2;
hence thesis;
end;
theorem Th37:
not f in dom S
proof
f in SCM+FSA-Data*-Loc by Def3;
hence thesis by SCMFSA_1:30,XBOOLE_0:3;
end;
theorem Th38:
for s being State of SCM+FSA holds Int-Locations c= dom s
proof
let s be State of SCM+FSA;
dom s = the carrier of SCM+FSA by PARTFUN1:def 2;
hence thesis;
end;
theorem Th39:
for s being State of SCM+FSA holds FinSeq-Locations c= dom s
proof
let s be State of SCM+FSA;
dom s = the carrier of SCM+FSA by PARTFUN1:def 2;
hence thesis;
end;
theorem
for s being State of SCM+FSA holds dom (s|Int-Locations) =
Int-Locations
proof
let s be State of SCM+FSA;
Int-Locations c= dom s by Th38;
hence thesis by RELAT_1:62;
end;
theorem
for s being State of SCM+FSA holds dom (s|FinSeq-Locations) =
FinSeq-Locations
proof
let s be State of SCM+FSA;
FinSeq-Locations c= dom s by Th39;
hence thesis by RELAT_1:62;
end;
theorem Th42:
for s being State of SCM+FSA, i being Instruction of SCM
holds s|SCM-Memory is State of SCM
proof
let s be State of SCM+FSA, i be Instruction of SCM;
reconsider s as SCM+FSA-State by CARD_3:107;
s|SCM-Memory is SCM-State by SCMFSA_1:17;
then s|SCM-Memory is State of SCM by AMI_3:29;
hence thesis;
end;
theorem
for s being State of SCM+FSA, s9 being State of SCM
holds s +* s9 is State of SCM+FSA
proof
let s be State of SCM+FSA, s9 being State of SCM;
reconsider s as SCM+FSA-State by CARD_3:107;
reconsider s9 as SCM-State by CARD_3:107;
s +* s9 is SCM+FSA-State by SCMFSA_1:18;
then s +* s9 is State of SCM+FSA;
hence thesis;
end;
theorem Th44:
for i being Instruction of SCM, ii being Instruction of SCM+FSA,
s being State of SCM, ss being State of SCM+FSA st i = ii & s = ss|SCM-Memory
holds Exec(ii,ss) = ss +* Exec(i,s)
proof
let i be Instruction of SCM, ii be Instruction of SCM+FSA, s be State of SCM
, ss be State of SCM+FSA such that
A1: i = ii and
A2: s = ss|SCM-Memory;
reconsider SS = ss as SCM+FSA-State by CARD_3:107;
reconsider II = ii as Element of SCM+FSA-Instr;
InsCode II <= 8 by A1,AMI_5:5;
then consider I being Element of SCM-Instr, S being SCM-State such that
A3: I = II & S = SS|SCM-Memory and
A4: SCM+FSA-Exec-Res(II,SS) = SS +* SCM-Exec-Res(I,S) by SCMFSA_1:def 16;
Exec(i,s) = SCM-Exec-Res(I,S) by A1,A2,A3,AMI_2:def 15;
hence thesis by A4,SCMFSA_1:def 17;
end;
registration
let s be State of SCM+FSA, d be Int-Location;
cluster s.d -> integer;
coherence
proof
reconsider D = d as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider S = s as SCM+FSA-State by CARD_3:107;
S.D = s.d;
hence thesis;
end;
end;
definition
let s be State of SCM+FSA, d be FinSeq-Location;
redefine func s.d -> FinSequence of INT; :: redefines . (FUNCT_1, definition)
coherence
proof
reconsider D = d as Element of SCM+FSA-Data*-Loc by Def3;
reconsider S = s as SCM+FSA-State by CARD_3:107;
S.D = s.d;
hence thesis;
end;
end;
theorem Th45:
S = s|SCM-Memory implies s = s +* S by FUNCT_4:75;
theorem Th46:
s1 = s +* S implies s1.IC SCM+FSA = S.IC SCM
proof
A1: dom S = SCM-Memory by PARTFUN1:def 2;
assume s1 = s +* S;
hence s1.IC SCM+FSA
= S.IC SCM by A1,Th1,AMI_3:1,FUNCT_4:13;
end;
theorem Th47:
s1 = s +* S & A = a implies S.A = s1.a
proof
assume that
A1: s1 = s +* S and
A2: A = a;
dom S = SCM-Memory by PARTFUN1:def 2;
hence s1.a = S.A by A1,A2,FUNCT_4:13;
end;
theorem Th48:
S = s|SCM-Memory & A = a implies S.A = s.a
proof
assume S = s|SCM-Memory;
then s = s +* S by Th45;
hence thesis by Th47;
end;
registration
cluster SCM+FSA -> IC-Ins-separated;
coherence
by SCMFSA_1:5,SCMFSA_1:9,SUBSET_1:def 8;
end;
theorem Th49:
for dl being Int-Location holds dl <> IC SCM+FSA
by AMI_2:def 16,Th1,FINSET_1:15;
theorem Th50:
for dl being FinSeq-Location holds dl <> IC SCM+FSA
proof
let dl be FinSeq-Location;
now assume NAT in INT \ NAT;
then
A1: NAT in NAT \/ [:{0},NAT:] by NUMBERS:def 4,XBOOLE_0:def 5;
per cases by A1,XBOOLE_0:def 3;
suppose NAT in NAT;
hence contradiction;
end;
suppose NAT in [:{0},NAT:];
hence contradiction by FINSET_1:15;
end;
end;
hence thesis by Def3,Th1;
end;
theorem
for il being Int-Location, dl being FinSeq-Location holds il <> dl
proof
let il be Int-Location, dl be FinSeq-Location;
Values dl = INT* by Th7;
hence thesis by Th6,FUNCT_7:16;
end;
theorem
for il being Nat, dl being Int-Location
holds il <> dl
proof
let il be Nat, dl be Int-Location;
dl in [:{1},NAT:] by AMI_2:def 16;
then ex x,y being object st x in {1} & y in NAT & dl = [x,y] by ZFMISC_1:84;
hence il <> dl;
end;
theorem
for il being Nat, dl being FinSeq-Location
holds il <> dl
proof
let il be Nat, dl be FinSeq-Location;
A1: dl in INT \ NAT by Def3;
A2: il in NAT by ORDINAL1:def 12;
NAT misses INT \ NAT by XBOOLE_1:79;
hence thesis by A1,A2,XBOOLE_0:3;
end;
theorem
for s1,s2 being State of SCM+FSA st IC s1 = IC s2 &
(for a being Int-Location holds s1.a = s2.a) &
(for f being FinSeq-Location holds s1.f = s2.f)
holds s1 = s2
proof
let s1,s2 be State of SCM+FSA such that
A1: IC(s1) = IC(s2) and
A2: for a being Int-Location holds s1.a = s2.a and
A3: for f being FinSeq-Location holds s1.f = s2.f;
s1 in product(SCM*-VAL*SCM+FSA-OK) by CARD_3:107;
then consider g1 being Function such that
A4: s1 = g1 and
A5: dom g1 = dom(SCM*-VAL*SCM+FSA-OK) and
for x being object st x in dom(SCM*-VAL*SCM+FSA-OK)
holds g1.x in (SCM*-VAL*SCM+FSA-OK).x by CARD_3:def 5;
s2 in product(SCM*-VAL*SCM+FSA-OK) by CARD_3:107;
then consider g2 being Function such that
A6: s2 = g2 and
A7: dom g2 = dom(SCM*-VAL*SCM+FSA-OK) and
for x being object st x in dom(SCM*-VAL*SCM+FSA-OK)
holds g2.x in (SCM*-VAL*SCM+FSA-OK).x by CARD_3:def 5;
A8: now
let x be object;
assume x in SCM+FSA-Memory;
then x in {IC SCM+FSA} \/ SCM-Data-Loc \/ SCM+FSA-Data*-Loc by Th1;
then
A9: x in {IC SCM+FSA} \/ SCM-Data-Loc or x in SCM+FSA-Data*-Loc
by XBOOLE_0:def 3;
A10: Int-Locations = SCM+FSA-Data-Loc;
per cases by A9,XBOOLE_0:def 3;
suppose
x in {IC SCM+FSA};
then x = IC SCM+FSA by TARSKI:def 1;
hence g1.x = g2.x by A1,A4,A6;
end;
suppose
x in SCM-Data-Loc;
then x is Int-Location by A10,AMI_2:def 16;
hence g1.x = g2.x by A2,A4,A6;
end;
suppose
x in SCM+FSA-Data*-Loc;
then x is FinSeq-Location by Def3;
hence g1.x = g2.x by A3,A4,A6;
end;
end;
thus thesis by A4,A5,A6,A7,A8;
end;
theorem Th55:
S = s|SCM-Memory implies IC s = IC S
proof
assume S = s|SCM-Memory;
then s = s +* S by Th45;
hence thesis by Th46;
end;
begin :: Users guide
theorem Th56:
Exec(a:=b, s).IC SCM+FSA = IC s + 1 & Exec(a:=b, s).a = s.b & (
for c st c <> a holds Exec(a:=b, s).c = s.c) & for f holds Exec(a:=b, s).f = s.
f
proof
consider A,B such that
A1: a = A and
A2: b = B and
A3: a:=b = A:=B by Def6;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A4: Exec(a:=b, s)=s +* Exec(A:=B, S) by A3,Th44;
hence Exec(a:=b, s).IC SCM+FSA = Exec(A:=B, S).IC SCM by Th46
.= IC S + 1 by AMI_3:2
.= IC s + 1 by Th55;
thus Exec(a:=b, s).a = Exec(A:=B, S).A by A1,A4,Th47
.= S.B by AMI_3:2
.= s.b by A2,Th48;
hereby
let c such that
A5: c <> a;
reconsider C = c as Data-Location by Th5;
thus Exec(a:=b, s).c = Exec(A:=B, S).C by A4,Th47
.= S.C by A1,A5,AMI_3:2
.= s.c by Th48;
end;
let f;
A6: not f in dom Exec(A:=B, S) by Th37;
thus Exec(a:=b, s).f
= s.f by A4,A6,FUNCT_4:11;
end;
theorem Th57:
Exec(AddTo(a,b), s).IC SCM+FSA = IC s + 1 & Exec(AddTo(a,b), s)
.a = s.a + s.b & (for c st c <> a holds Exec(AddTo(a,b), s).c = s.c) & for f
holds Exec(AddTo(a,b), s).f = s.f
proof
consider A,B such that
A1: a = A and
A2: b = B and
A3: AddTo(a,b) = AddTo(A,B) by Def7;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A4: Exec(AddTo(a,b), s)=s +* Exec(AddTo(A,B), S) by A3,Th44;
hence Exec(AddTo(a,b), s).IC SCM+FSA = Exec(AddTo(A,B), S).IC SCM by Th46
.= IC S + 1 by AMI_3:3
.= IC s + 1 by Th55;
thus Exec(AddTo(a,b), s).a = Exec(AddTo(A,B), S).A by A1,A4,Th47
.= S.A + S.B by AMI_3:3
.= S.A + s.b by A2,Th48
.= s.a + s.b by A1,Th48;
hereby
let c such that
A5: c <> a;
reconsider C = c as Data-Location by Th5;
thus Exec(AddTo(a,b), s).c = Exec(AddTo(A,B), S).C by A4,Th47
.= S.C by A1,A5,AMI_3:3
.= s.c by Th48;
end;
let f;
A6: not f in dom Exec(AddTo(A,B), S) by Th37;
thus Exec(AddTo(a,b), s).f
= s.f by A4,A6,FUNCT_4:11;
end;
theorem Th58:
Exec(SubFrom(a,b), s).IC SCM+FSA = IC s + 1 & Exec(SubFrom(a,b)
, s).a = s.a - s.b & (for c st c <> a holds Exec(SubFrom(a,b), s).c = s.c) &
for f holds Exec(SubFrom(a,b), s).f = s.f
proof
consider A,B such that
A1: a = A and
A2: b = B and
A3: SubFrom(a,b) = SubFrom(A,B) by Def8;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A4: Exec(SubFrom(a,b), s)=s +* Exec(SubFrom(A,B), S) by A3,Th44;
hence Exec(SubFrom(a,b), s).IC SCM+FSA = Exec(SubFrom(A,B), S).IC SCM by Th46
.= IC S + 1 by AMI_3:4
.= IC s + 1 by Th55;
thus Exec(SubFrom(a,b), s).a = Exec(SubFrom(A,B), S).A by A1,A4,Th47
.= S.A - S.B by AMI_3:4
.= S.A - s.b by A2,Th48
.= s.a - s.b by A1,Th48;
hereby
let c such that
A5: c <> a;
reconsider C = c as Data-Location by Th5;
thus Exec(SubFrom(a,b), s).c = Exec(SubFrom(A,B), S).C by A4,Th47
.= S.C by A1,A5,AMI_3:4
.= s.c by Th48;
end;
let f;
A6: not f in dom Exec(SubFrom(A,B), S) by Th37;
thus Exec(SubFrom(a,b), s).f
= s.f by A4,A6,FUNCT_4:11;
end;
theorem Th59:
Exec(MultBy(a,b), s).IC SCM+FSA = IC s + 1 & Exec(MultBy(a,b),
s).a = s.a * s.b & (for c st c <> a holds Exec(MultBy(a,b), s).c = s.c) & for f
holds Exec(MultBy(a,b), s).f = s.f
proof
consider A,B such that
A1: a = A and
A2: b = B and
A3: MultBy(a,b) = MultBy(A,B) by Def9;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A4: Exec(MultBy(a,b), s)=s +* Exec(MultBy(A,B), S) by A3,Th44;
hence Exec(MultBy(a,b), s).IC SCM+FSA = Exec(MultBy(A,B), S).IC SCM by Th46
.= IC S + 1 by AMI_3:5
.= IC s + 1 by Th55;
thus Exec(MultBy(a,b), s).a = Exec(MultBy(A,B), S).A by A1,A4,Th47
.= S.A * S.B by AMI_3:5
.= S.A * s.b by A2,Th48
.= s.a * s.b by A1,Th48;
hereby
let c such that
A5: c <> a;
reconsider C = c as Data-Location by Th5;
thus Exec(MultBy(a,b), s).c = Exec(MultBy(A,B), S).C by A4,Th47
.= S.C by A1,A5,AMI_3:5
.= s.c by Th48;
end;
let f;
A6: not f in dom Exec(MultBy(A,B), S) by Th37;
thus Exec(MultBy(a,b), s).f
= s.f by A4,A6,FUNCT_4:11;
end;
theorem Th60:
Exec(Divide(a,b), s).IC SCM+FSA = IC s + 1 & (a <> b implies
Exec(Divide(a,b), s).a = s.a div s.b) & Exec(Divide(a,b), s).b = s.a mod s.b &
(for c st c <> a & c <> b holds Exec(Divide(a,b), s).c = s.c) & for f holds
Exec(Divide(a,b), s).f = s.f
proof
consider A,B such that
A1: a = A and
A2: b = B and
A3: Divide(a,b) = Divide(A,B) by Def10;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A4: Exec(Divide(a,b), s)=s +* Exec(Divide(A,B), S) by A3,Th44;
hence Exec(Divide(a,b), s).IC SCM+FSA = Exec(Divide(A,B), S).IC SCM by Th46
.= IC S + 1 by AMI_3:6
.= IC s + 1 by Th55;
hereby
assume
A5: a <> b;
thus Exec(Divide(a,b), s).a = Exec(Divide(A,B), S).A by A1,A4,Th47
.= S.A div S.B by A1,A2,A5,AMI_3:6
.= S.A div s.b by A2,Th48
.= s.a div s.b by A1,Th48;
end;
thus Exec(Divide(a,b), s).b = Exec(Divide(A,B), S).B by A2,A4,Th47
.= S.A mod S.B by AMI_3:6
.= S.A mod s.b by A2,Th48
.= s.a mod s.b by A1,Th48;
hereby
let c such that
A6: c <> a & c <> b;
reconsider C = c as Data-Location by Th5;
thus Exec(Divide(a,b), s).c = Exec(Divide(A,B), S).C by A4,Th47
.= S.C by A1,A2,A6,AMI_3:6
.= s.c by Th48;
end;
let f;
A7: not f in dom Exec(Divide(A,B), S) by Th37;
thus Exec(Divide(a,b), s).f
= s.f by A4,A7,FUNCT_4:11;
end;
theorem
Exec(Divide(a,a), s).IC SCM+FSA = IC s + 1 & Exec(Divide(a,a), s).a =
s.a mod s.a & (for c st c <> a holds Exec(Divide(a,a), s).c = s.c) & for f
holds Exec(Divide(a,a), s).f = s.f
proof
consider A,B such that
A1: a = A and
A2: a = B & Divide(a,a) = Divide(A,B) by Def10;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A3: Exec(Divide(a,a), s)=s +* Exec(Divide(A,A), S) by A1,A2,Th44;
hence Exec(Divide(a,a), s).IC SCM+FSA = Exec(Divide(A,A), S).IC SCM by Th46
.= IC S + 1 by AMI_3:6
.= IC s + 1 by Th55;
thus Exec(Divide(a,a), s).a = Exec(Divide(A,A), S).A by A1,A3,Th47
.= S.A mod S.A by AMI_3:6
.= S.A mod s.a by A1,Th48
.= s.a mod s.a by A1,Th48;
hereby
let c such that
A4: c <> a;
reconsider C = c as Data-Location by Th5;
thus Exec(Divide(a,a), s).c = Exec(Divide(A,A), S).C by A3,Th47
.= S.C by A1,A4,AMI_3:6
.= s.c by Th48;
end;
let f;
A5: not f in dom Exec(Divide(A,A), S) by Th37;
thus Exec(Divide(a,a), s).f
= s.f by A3,A5,FUNCT_4:11;
end;
theorem Th62:
Exec(goto l, s).IC SCM+FSA = l & (for c holds Exec(goto l, s).c
= s.c) & for f holds Exec(goto l, s).f = s.f
proof
consider La such that
A1: l = La and
A2: goto l = SCM-goto La;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A3: Exec(goto l, s)=s +* Exec(SCM-goto La, S) by A2,Th44;
hence Exec(goto l, s).IC SCM+FSA = Exec(SCM-goto La, S).IC SCM by Th46
.= l by A1,AMI_3:7;
hereby
let c;
reconsider C = c as Data-Location by Th5;
thus Exec(goto l, s).c = Exec(SCM-goto La, S).C by A3,Th47
.= S.C by AMI_3:7
.= s.c by Th48;
end;
let f;
A4: not f in dom Exec(SCM-goto La, S) by Th37;
thus Exec(goto l, s).f
= s.f by A3,A4,FUNCT_4:11;
end;
theorem Th63:
(s.a = 0 implies Exec(a =0_goto l, s).IC SCM+FSA = l) & (s.a <>
0 implies Exec(a=0_goto l, s).IC SCM+FSA = IC s + 1) & (for c holds Exec(a
=0_goto l, s).c = s.c) & for f holds Exec(a=0_goto l, s).f = s.f
proof
consider A such that
A1: a = A and
A2: a =0_goto l = A =0_goto l by Def12;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A3: Exec(a =0_goto l, s)=s +* Exec(A =0_goto l, S) by A2,Th44;
hereby
assume s.a = 0;
then
A4: S.A = 0 by A1,Th48;
thus Exec(a =0_goto l, s).IC SCM+FSA = Exec(A =0_goto l, S).IC SCM by A3
,Th46
.= l by A4,AMI_3:8;
end;
hereby
assume s.a <> 0;
then
A5: S.A <> 0 by A1,Th48;
thus Exec(a =0_goto l, s).IC SCM+FSA = Exec(A =0_goto l, S).IC SCM by A3
,Th46
.= IC S + 1 by A5,AMI_3:8
.= IC s + 1 by Th55;
end;
hereby
let c;
reconsider C = c as Data-Location by Th5;
thus Exec(a =0_goto l, s).c = Exec(A =0_goto l, S).C by A3,Th47
.= S.C by AMI_3:8
.= s.c by Th48;
end;
let f;
A6: not f in dom Exec(A =0_goto l, S) by Th37;
thus Exec(a =0_goto l, s).f
= s.f by A3,A6,FUNCT_4:11;
end;
theorem Th64:
(s.a > 0 implies Exec(a >0_goto l, s).IC SCM+FSA = l) & (s.a <=
0 implies Exec(a>0_goto l, s).IC SCM+FSA = IC s + 1) & (for c holds Exec(a
>0_goto l, s).c = s.c) & for f holds Exec(a>0_goto l, s).f = s.f
proof
consider A such that
A1: a = A and
A2: a >0_goto l = A >0_goto l by Def13;
reconsider S = s|SCM-Memory as State of SCM by Th42;
A3: Exec(a >0_goto l, s)=s +* Exec(A >0_goto l, S) by A2,Th44;
hereby
assume s.a > 0;
then
A4: S.A > 0 by A1,Th48;
thus Exec(a >0_goto l, s).IC SCM+FSA = Exec(A >0_goto l, S).IC SCM by A3
,Th46
.= l by A4,AMI_3:9;
end;
hereby
assume s.a <= 0;
then
A5: S.A <= 0 by A1,Th48;
thus Exec(a >0_goto l, s).IC SCM+FSA = Exec(A >0_goto l, S).IC SCM by A3
,Th46
.= IC S + 1 by A5,AMI_3:9
.= IC s + 1 by Th55;
end;
hereby
let c;
reconsider C = c as Data-Location by Th5;
thus Exec(a >0_goto l, s).c = Exec(A >0_goto l, S).C by A3,Th47
.= S.C by AMI_3:9
.= s.c by Th48;
end;
let f;
A6: not f in dom Exec(A >0_goto l, S) by Th37;
thus Exec(a >0_goto l, s).f
= s.f by A3,A6,FUNCT_4:11;
end;
theorem Th65:
Exec(c:=(g,a), s).IC SCM+FSA = IC s + 1 & (ex k st k = |.s.a.|
& Exec(c:=(g,a), s).c = (s.g)/.k) & (for b st b <> c holds Exec(c:=(g,a), s).b
= s.b) & for f holds Exec(c:=(g,a), s).f = s.f
proof
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;
reconsider mk = a, ml = c as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = c:=(g,a) as Element of SCM+FSA-Instr;
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider J = 9 as Element of Segm 13 by NAT_1:44;
InsCode I = 9;
then consider i being Integer, k being Nat such that
A1: k = |.S.(I int_addr2).| and
A2: i = (S.(I coll_addr1))/.k and
A3: SCM+FSA-Exec-Res(I,S) = SCM+FSA-Chg(SCM+FSA-Chg(S,I int_addr1,i),
IC S + 1) by SCMFSA_1:def 16;
set S1 = SCM+FSA-Chg(S,I int_addr1,i);
A4: Exec(c:=(g,a), s) = (SCM+FSA-Chg(S1, IC S + 1)) by A3,SCMFSA_1:def 17;
hence Exec(c:=(g,a), s).IC SCM+FSA = IC s + 1 by Th1,SCMFSA_1:19;
A5: I = [J,{},<*ml,p,mk*>] & I`3_3 = <*ml,p,mk*>;
then
A6: I int_addr1 = ml by SCMFSA_I:def 3;
A7: I coll_addr1 = p by A5,SCMFSA_I:def 5;
hereby
reconsider k as Nat;
take k;
thus k = |.s.a.| by A5,A1,SCMFSA_I:def 4;
thus Exec(c:=(g,a), s).c = S1.ml by A4,SCMFSA_1:20
.= (s.g)/.k by A2,A6,A7,SCMFSA_1:24;
end;
hereby
let b;
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
assume
A8: b <> c;
thus Exec(c:=(g,a), s).b = S1.mn by A4,SCMFSA_1:20
.= s.b by A6,A8,SCMFSA_1:25;
end;
let f;
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;
thus Exec(c:=(g,a), s).f = S1.q by A4,SCMFSA_1:21
.= s.f by SCMFSA_1:26;
end;
theorem Th66:
Exec((g,a):=c, s).IC SCM+FSA = IC s + 1 & (ex k st k = |.s.a.|
& Exec((g,a):=c, s).g = s.g+*(k,s.c)) & (for b holds Exec((g,a):=c, s).b = s.b)
& for f st f <> g holds Exec((g,a):=c, s).f = s.f
proof
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;
reconsider mk = a, ml = c as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = (g,a):=c as Element of SCM+FSA-Instr;
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider J = 10 as Element of Segm 13 by NAT_1:44;
InsCode I = 10;
then consider F being FinSequence of INT,k being Nat such that
A1: k = |.S.(I int_addr2).| and
A2: F = S.(I coll_addr1)+*(k,S.(I int_addr1)) and
A3: SCM+FSA-Exec-Res(I,S)=SCM+FSA-Chg(SCM+FSA-Chg(S,I coll_addr1,F),
IC S + 1) by SCMFSA_1:def 16;
set S1 = SCM+FSA-Chg(S,I coll_addr1,F);
A4: Exec((g,a):=c, s) = (SCM+FSA-Chg(S1, IC S + 1)) by A3,SCMFSA_1:def 17;
hence Exec((g,a):=c, s).IC SCM+FSA = IC s + 1 by Th1,SCMFSA_1:19;
A5: I = [J,{},<*ml,p,mk*>] & I`3_3 = <*ml,p,mk*>;
then
A6: I coll_addr1 = p by SCMFSA_I:def 5;
A7: I int_addr1 = ml by A5,SCMFSA_I:def 3;
hereby
reconsider k as Nat;
take k;
thus k = |.s.a.| by A5,A1,SCMFSA_I:def 4;
thus Exec((g,a):=c, s).g = S1.p by A4,SCMFSA_1:21
.= s.g+*(k,s.c) by A2,A7,A6,SCMFSA_1:27;
end;
hereby
let b;
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
thus Exec((g,a):=c, s).b = S1.mn by A4,SCMFSA_1:20
.= s.b by SCMFSA_1:29;
end;
let f such that
A8: f <> g;
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;
thus Exec((g,a):=c, s).f = S1.q by A4,SCMFSA_1:21
.= s.f by A6,A8,SCMFSA_1:28;
end;
theorem Th67:
Exec(c:=len g, s).IC SCM+FSA = IC s + 1 & Exec(c:=len g, s).c
= len(s.g) & (for b st b <> c holds Exec(c:=len g, s).b = s.b) & for f holds
Exec(c:=len g, s).f = s.f
proof
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;
reconsider I = c:=len g as Element of SCM+FSA-Instr;
set S1 = SCM+FSA-Chg(S,I int_addr3,len(S.(I coll_addr2)));
reconsider J = 11 as Element of Segm 13 by NAT_1:44;
reconsider ml = c as Element of SCM-Data-Loc by AMI_2:def 16;
A1: InsCode I = 11;
A2: Exec(c:=len g, s) = SCM+FSA-Exec-Res(I,S) by SCMFSA_1:def 17
.= (SCM+FSA-Chg(S1, IC S + 1)) by A1,SCMFSA_1:def 16;
hence Exec(c:=len g, s).IC SCM+FSA = IC s + 1 by Th1,SCMFSA_1:19;
A3: I = [J,{},<*ml,p*>] & I`3_3 = <*ml,p*>;
then
A4: I int_addr3 = ml by SCMFSA_I:def 7;
A5: I coll_addr2 = p by A3,SCMFSA_I:def 8;
thus Exec(c:=len g, s).c = S1.ml by A2,SCMFSA_1:20
.= len(s.g) by A4,A5,SCMFSA_1:24;
hereby
let b;
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
assume
A6: b <> c;
thus Exec(c:=len g, s).b = S1.mn by A2,SCMFSA_1:20
.= s.b by A4,A6,SCMFSA_1:25;
end;
let f;
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;
thus Exec(c:=len g, s).f = S1.q by A2,SCMFSA_1:21
.= s.f by SCMFSA_1:26;
end;
theorem Th68:
Exec(g:=<0,...,0>c, s).IC SCM+FSA = IC s + 1 & (ex k st k =
|.s.c.| & Exec(g:=<0,...,0>c, s).g = k |-> 0) & (for b holds Exec(g:=<0,...,0>
c, s).b = s.b) & for f st f <> g holds Exec(g:=<0,...,0>c, s).f = s.f
proof
reconsider p = g as Element of SCM+FSA-Data*-Loc by Def3;
reconsider ml = c as Element of SCM-Data-Loc by AMI_2:def 16;
reconsider I = g:=<0,...,0>c as Element of SCM+FSA-Instr;
reconsider S = s as SCM+FSA-State by CARD_3:107;
reconsider J = 12 as Element of Segm 13 by NAT_1:44;
InsCode I = 12;
then consider F being FinSequence of INT,k being Nat such that
A1: k = |.S.(I int_addr3).| and
A2: F = k |-> 0 and
A3: SCM+FSA-Exec-Res(I,S) = SCM+FSA-Chg(SCM+FSA-Chg(S,I coll_addr2,F),
IC S + 1) by SCMFSA_1:def 16;
set S1 = SCM+FSA-Chg(S,I coll_addr2,F);
A4: Exec(g:=<0,...,0>c, s) = SCM+FSA-Chg(S1, IC S + 1) by A3,SCMFSA_1:def 17;
hence Exec(g:=<0,...,0>c, s).IC SCM+FSA = IC s + 1 by Th1,SCMFSA_1:19;
A5: I = [J,{},<*ml,p*>] & I`3_3 = <*ml,p*>;
then
A6: I coll_addr2 = p by SCMFSA_I:def 8;
hereby
reconsider k as Nat;
take k;
thus k = |.s.c.| by A5,A1,SCMFSA_I:def 7;
thus Exec(g:=<0,...,0>c, s).g = S1.p by A4,SCMFSA_1:21
.= k|->0 by A2,A6,SCMFSA_1:27;
end;
hereby
let b;
reconsider mn = b as Element of SCM-Data-Loc by AMI_2:def 16;
thus Exec(g:=<0,...,0>c, s).b = S1.mn by A4,SCMFSA_1:20
.= s.b by SCMFSA_1:29;
end;
let f such that
A7: f <> g;
reconsider q = f as Element of SCM+FSA-Data*-Loc by Def3;
thus Exec(g:=<0,...,0>c, s).f = S1.q by A4,SCMFSA_1:21
.= s.f by A6,A7,SCMFSA_1:28;
end;
begin :: Halt Instruction
theorem
for S being SCM+FSA-State st S = s holds IC s = IC S by SCMFSA_1:5
,SUBSET_1:def 8;
theorem Th70:
for i being Instruction of SCM, I being Instruction of SCM+FSA
st i = I & i is halting holds I is halting
proof
let i be Instruction of SCM, I be Instruction of SCM+FSA such that
A1: i = I;
assume
A2: i is halting;
let S be State of SCM+FSA;
reconsider s = (S|SCM-Memory) as State of SCM by Th42;
thus Exec(I,S) = S +* Exec(i,s) by A1,Th44
.= S +* s by A2
.= S by Th45;
end;
theorem Th71:
for I being Instruction of SCM+FSA st ex s st Exec(I,s).IC
SCM+FSA = IC s + 1 holds I is non halting
proof
let I be Instruction of SCM+FSA;
given s such that
A1: Exec(I,s).IC SCM+FSA = IC s + 1;
reconsider T = s as SCM+FSA-State by CARD_3:107;
IC T = T.NAT;
then reconsider w = T.NAT as Nat;
assume I is halting;
then
A2: Exec(I,s).IC SCM+FSA = T.NAT by Th1;
Exec(I,s).IC SCM+FSA = w+1 by A1,SCMFSA_1:5,SUBSET_1:def 8;
hence contradiction by A2;
end;
registration let a,b;
set s =the State of SCM+FSA;
cluster a := b -> non halting;
coherence
proof
IC Exec(a:=b, s) = IC s + 1 by Th56;
hence thesis by Th71;
end;
cluster AddTo(a,b) -> non halting;
coherence
proof
IC Exec(AddTo(a,b), s) = IC s + 1 by Th57;
hence thesis by Th71;
end;
cluster SubFrom(a,b) -> non halting;
coherence
proof
IC Exec(SubFrom(a,b), s) = IC s + 1 by Th58;
hence thesis by Th71;
end;
cluster MultBy(a,b) -> non halting;
coherence
proof
IC Exec(MultBy(a,b), s) = IC s + 1 by Th59;
hence thesis by Th71;
end;
cluster Divide(a,b) -> non halting;
coherence
proof
IC Exec(Divide(a,b), s) = IC s + 1 by Th60;
hence thesis by Th71;
end;
end;
theorem
a := b is non halting;
theorem
AddTo(a,b) is non halting;
theorem
SubFrom(a,b) is non halting;
theorem
MultBy(a,b) is non halting;
theorem
Divide(a,b) is non halting;
registration let la;
cluster goto la -> non halting;
coherence
proof
set f = the_Values_of SCM+FSA;
set s =the SCM+FSA-State;
assume
A1: goto la is halting;
reconsider a3 = la as Nat;
set t = s +* (NAT.--> (a3+1));
NAT in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then
A2: t.NAT = (NAT.--> (a3+1)).NAT by FUNCT_4:13
.= (a3+1) by FUNCOP_1:72;
A3: for x being object st x in dom f holds t.x in f.x
proof
let x be object such that
A4: x in dom f;
per cases;
suppose
x = NAT;
hence thesis by A2,SCMFSA_1:9;
end;
suppose
x <> NAT;
then not x in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then t.x = s.x by FUNCT_4:11;
hence thesis by A4,CARD_3:9;
end;
end;
A5: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5,ZFMISC_1:31;
A6: dom t = dom s \/ dom (NAT.--> (a3+1)) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ dom (NAT.--> (a3+1)) by SCMFSA_1:33
.= SCM+FSA-Memory \/ {NAT}
.= SCM+FSA-Memory by A5,XBOOLE_1:12;
dom f = SCM+FSA-Memory by SCMFSA_1:32;
then reconsider t as State of SCM+FSA
by A6,A3,FUNCT_1:def 14,PARTFUN1:def 2,RELAT_1:def 18;
reconsider w = t as SCM+FSA-State by CARD_3:107;
NAT in dom (NAT .--> la) by TARSKI:def 1;
then
A7: (w +* (NAT .--> la)).NAT = (NAT .--> la).NAT by FUNCT_4:13
.= la by FUNCOP_1:72;
(w +* (NAT .--> la)).NAT = SCM+FSA-Chg(w,a3).NAT
.= a3 by SCMFSA_1:19
.= Exec(goto la,t).NAT by Th1,Th62
.= t.NAT by A1;
hence contradiction by A2,A7;
end;
end;
theorem
goto la is non halting;
registration let a,la;
set f = the_Values_of SCM+FSA;
set s =the SCM+FSA-State;
cluster a=0_goto la -> non halting;
coherence
proof
reconsider a3 = la as Nat;
set t = s +* (NAT.--> (a3+1));
A1: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5,ZFMISC_1:31;
A2: dom t = dom s \/ dom (NAT.--> (a3+1)) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ dom (NAT.--> (a3+1)) by SCMFSA_1:33
.= SCM+FSA-Memory \/ {NAT}
.= SCM+FSA-Memory by A1,XBOOLE_1:12;
assume
A3: a=0_goto la is halting;
NAT in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then
A4: t.NAT = (NAT.--> (a3+1)).NAT by FUNCT_4:13
.= (a3+1) by FUNCOP_1:72;
A5: for x being object st x in dom f holds t.x in f.x
proof
let x be object such that
A6: x in dom f;
per cases;
suppose
x = NAT;
hence thesis by A4,SCMFSA_1:9;
end;
suppose
x <> NAT;
then not x in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then t.x = s.x by FUNCT_4:11;
hence thesis by A6,CARD_3:9;
end;
end;
dom f = SCM+FSA-Memory by SCMFSA_1:32;
then reconsider t as State of SCM+FSA
by A2,A5,FUNCT_1:def 14,PARTFUN1:def 2,RELAT_1:def 18;
reconsider w = t as SCM+FSA-State by CARD_3:107;
NAT in dom (NAT .--> la) by TARSKI:def 1;
then
A7: (w +* (NAT .--> la)).NAT = (NAT .--> la).NAT by FUNCT_4:13
.= la by FUNCOP_1:72;
per cases;
suppose
A8: t.a <> 0;
IC w = w.NAT;
then reconsider e = w.NAT as Nat;
IC t = IC w by SCMFSA_1:5,SUBSET_1:def 8;
then
A9: Exec(a=0_goto la,t).IC SCM+FSA = e+1 by A8,Th63;
Exec(a=0_goto la,t).IC SCM+FSA = w.NAT by A3,Th1;
hence contradiction by A9;
end;
suppose
A10: t.a = 0;
(w +* (NAT .--> la)).NAT = (SCM+FSA-Chg(w,a3)).NAT
.= a3 by SCMFSA_1:19
.= Exec(a=0_goto la,t).NAT by A10,Th1,Th63
.= t.NAT by A3;
hence contradiction by A4,A7;
end;
end;
cluster a>0_goto la -> non halting;
coherence
proof
reconsider a3 = la as Nat;
set t = s +* (NAT.--> (a3+1));
A11: {NAT} c= SCM+FSA-Memory by SCMFSA_1:5,ZFMISC_1:31;
A12: dom t = dom s \/ dom (NAT.--> (a3+1)) by FUNCT_4:def 1
.= SCM+FSA-Memory \/ dom (NAT.--> (a3+1)) by SCMFSA_1:33
.= SCM+FSA-Memory \/ {NAT}
.= SCM+FSA-Memory by A11,XBOOLE_1:12;
assume
A13: a>0_goto la is halting;
NAT in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then
A14: t.NAT = (NAT.--> (a3+1)).NAT by FUNCT_4:13
.= (a3+1) by FUNCOP_1:72;
A15: for x being object st x in dom f holds t.x in f.x
proof
let x be object such that
A16: x in dom f;
per cases;
suppose
x = NAT;
hence thesis by A14,SCMFSA_1:9;
end;
suppose
x <> NAT;
then not x in dom (NAT.--> (a3+1)) by TARSKI:def 1;
then t.x = s.x by FUNCT_4:11;
hence thesis by A16,CARD_3:9;
end;
end;
dom f = SCM+FSA-Memory by SCMFSA_1:32;
then reconsider t as State of SCM+FSA
by A12,A15,FUNCT_1:def 14,PARTFUN1:def 2,RELAT_1:def 18;
reconsider w = t as SCM+FSA-State by CARD_3:107;
NAT in dom (NAT .--> la) by TARSKI:def 1;
then
A17: (w +* (NAT .--> la)).NAT = (NAT .--> la).NAT by FUNCT_4:13
.= la by FUNCOP_1:72;
per cases;
suppose
A18: t.a <= 0;
IC w = w.NAT;
then reconsider e = w.NAT as Nat;
IC t = IC w by SCMFSA_1:5,SUBSET_1:def 8;
then
A19: Exec(a>0_goto la,t).IC SCM+FSA = e+1 by A18,Th64;
Exec(a>0_goto la,t).IC SCM+FSA = w.NAT by A13,Th1;
hence contradiction by A19;
end;
suppose
A20: t.a > 0;
(w +* (NAT .--> la)).NAT = (SCM+FSA-Chg(w,a3)).NAT
.= a3 by SCMFSA_1:19
.= Exec(a>0_goto la,t).NAT by A20,Th1,Th64
.= t.NAT by A13;
hence contradiction by A14,A17;
end;
end;
end;
theorem
a=0_goto la is non halting;
theorem
a>0_goto la is non halting;
registration let c,f,a;
set s =the State of SCM+FSA;
cluster c:=(f,a) -> non halting;
coherence
proof
Exec(c:=(f,a), s).IC SCM+FSA = IC s + 1 by Th65;
hence thesis by Th71;
end;
cluster (f,a):=c -> non halting;
coherence
proof
Exec((f,a):=c, s).IC SCM+FSA = IC s + 1 by Th66;
hence thesis by Th71;
end;
end;
theorem
c:=(f,a) is non halting;
theorem
(f,a):=c is non halting;
registration let c,f;
set s =the State of SCM+FSA;
cluster c:=len f -> non halting;
coherence
proof
Exec(c:=len f, s).IC SCM+FSA = IC s + 1 by Th67;
hence thesis by Th71;
end;
cluster f:=<0,...,0>c -> non halting;
coherence
proof
Exec(f:=<0,...,0>c, s).IC SCM+FSA = IC s + 1 by Th68;
hence thesis by Th71;
end;
end;
theorem
c:=len f is non halting;
theorem
f:=<0,...,0>c is non halting;
theorem
for I being Instruction of SCM+FSA
st I = [0,{},{}] holds I is halting by Th70,AMI_3:26;
theorem Th85:
for I be Instruction of SCM+FSA st InsCode I = 0 holds I = [0,{},{}]
proof
let I be Instruction of SCM+FSA such that
A1: InsCode I = 0;
A2: now
assume I in { [R,{},<*DA,DC*>] : R in { 1,2,3,4,5} };
then ex R,DA,DC st I = [R,{},<*DA,DC*>] & R in { 1,2,3,4,5};
hence contradiction by A1;
end;
A3: now
assume I in { [O,<*LA*>,{}] : O = 6 };
then ex O,LA st I = [O,<*LA*>,{}] & O = 6;
hence contradiction by A1;
end;
A4: now
assume I in { [P,<*LB*>,<*DB*>] : P in { 7,8 } };
then ex P,LB,DB st I = [P,<*LB*>,<*DB*>] & P in { 7,8 };
hence contradiction by A1;
end;
A5: now
assume I in { [K,{},<*dC,fB*>] : K in {11,12} };
then ex K,dC,fB st I = [K,{},<*dC,fB*>] & K in {11,12};
hence contradiction by A1;
end;
A6: I in SCM-Instr \/ { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc:
L in {9,10} }
by A5,XBOOLE_0:def 3;
now
assume I in { [L,{},<*dB,fA,dA*>] where L is Element of Segm 13,
dA,dB is Element of SCM+FSA-Data-Loc,fA is Element of SCM+FSA-Data*-Loc
: L in {9,10} };
then ex L be Element of Segm 13,
dA,dB be Element of SCM+FSA-Data-Loc,fA be Element of SCM+FSA-Data*-Loc
st I = [L,{},<*dB,fA,dA*>] & L in {9,10};
hence contradiction by A1;
end;
then I in SCM-Instr by A6,XBOOLE_0:def 3;
then
I in { [SCM-Halt,{},{}] } \/ { [O,<*LA*>,{}] : O = 6 }
\/ { [P,<*LB*>,<*DB*>] : P in { 7,8 } } by A2,XBOOLE_0:def 3;
then I in { [SCM-Halt,{},{}] } \/ { [O,<*LA*>,{}] : O = 6 }
by A4,XBOOLE_0:def 3;
then I in { [SCM-Halt,{},{}] } by A3,XBOOLE_0:def 3;
hence thesis by TARSKI:def 1;
end;
theorem Th86:
for I being set holds I is Instruction of SCM+FSA iff
I = [0,{},{}]
or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b))
or (ex a,b st I = SubFrom(a,b)) or
(ex a,b st I = MultBy(a,b)) or (ex a,b st I = Divide(a,b)) or
(ex la st I = goto la) or (ex lb,da st I = da=0_goto lb) or
(ex lb,da st I = da>0_goto lb) or (ex b,a,fa st I = a:=(fa,b)) or
(ex a,b,fa st I = (fa,a):=b) or
(ex a,f st I = a:=len f) or ex a,f st I = f:=<0,...,0>a
proof
let I be set;
thus I is Instruction of SCM+FSA implies
I = [0,{},{}]
or (ex a,b st I = a:=b) or (ex a,b st I = AddTo(a,b))
or (ex a,b st I = SubFrom(a,b)) or
(ex a,b st I = MultBy(a,b)) or (ex a,b st I = Divide(a,b)) or
(ex la st I = goto la) or (ex lb,da st I = da=0_goto lb) or
(ex lb,da st I = da>0_goto lb) or (ex b,a,fa st I = a:=(fa,b)) or
(ex a,b,fa st I = (fa,a):=b) or
(ex a,f st I = a:=len f) or ex a,f st I = f:=<0,...,0>a
proof
assume I is Instruction of SCM+FSA;
then reconsider J = I as Instruction of SCM+FSA;
set n = InsCode J;
n = 0 or ... or n = 12 by Th9;
hence thesis by Th23,Th24,Th25,Th26,Th27,Th28,Th29,Th30,Th31,Th32,Th33,Th34
,Th85;
end;
thus thesis by SCMFSA_I:3;
end;
Lm1: for W being Instruction of SCM+FSA st W is halting holds W = [0,{},{}]
proof
set I = [0,{},{}];
let W be Instruction of SCM+FSA such that
A1: W is halting;
assume
A2: I <> W;
per cases by Th86;
suppose
W = [0,{},{}];
hence thesis by A2;
end;
suppose
ex a,b st W = a:=b;
hence thesis by A1;
end;
suppose
ex a,b st W = AddTo(a,b);
hence thesis by A1;
end;
suppose
ex a,b st W = SubFrom(a,b);
hence thesis by A1;
end;
suppose
ex a,b st W = MultBy(a,b);
hence thesis by A1;
end;
suppose
ex a,b st W = Divide(a,b);
hence thesis by A1;
end;
suppose
ex la st W = goto la;
hence thesis by A1;
end;
suppose
ex lb,da st W = da=0_goto lb;
hence thesis by A1;
end;
suppose
ex lb,da st W = da>0_goto lb;
hence thesis by A1;
end;
suppose
ex b,a,fa st W = a:=(fa,b);
hence thesis by A1;
end;
suppose
ex a,b,fa st W = (fa,a):=b;
hence thesis by A1;
end;
suppose
ex a,f st W = a:=len f;
hence thesis by A1;
end;
suppose
ex a,f st W = f:=<0,...,0>a;
hence thesis by A1;
end;
end;
registration
cluster SCM+FSA -> halting;
coherence
by Th70,AMI_3:26;
end;
theorem Th87:
for I being Instruction of SCM+FSA st I is halting holds I = halt SCM+FSA
by Lm1;
theorem
for I being Instruction of SCM+FSA st InsCode I = 0 holds I =
halt SCM+FSA by Th85;
theorem Th89:
halt SCM = halt SCM+FSA;
::$CT
theorem
for i being Instruction of SCM, I being Instruction of SCM+FSA st i =
I & i is non halting holds I is non halting by Th87,Th89;
theorem
for i,j being Nat holds fsloc i <> intloc j
proof
let i,j be Nat;
fsloc i in FinSeq-Locations by Def3;
hence thesis by SCMFSA_1:30,XBOOLE_0:3;
end;
theorem Th92:
Data-Locations SCM+FSA = Int-Locations \/ FinSeq-Locations
proof
now
assume NAT in FinSeq-Locations;
then
A1: NAT in NAT \/ [:{0},NAT:] \ {[0,0]} by NUMBERS:def 4;
not NAT in NAT;
then NAT in [:{0},NAT:] by A1,XBOOLE_0:def 3;
then ex x,y being object st NAT = [x,y] by RELAT_1:def 1;
hence contradiction;
end;
then FinSeq-Locations misses {NAT} by ZFMISC_1:50;
then
A2: FinSeq-Locations \ ({NAT}) = FinSeq-Locations by XBOOLE_1:83;
SCM-Data-Loc misses {NAT} by AMI_2:20,ZFMISC_1:50;
then
A3: SCM-Data-Loc misses {NAT};
A4: SCM-Memory \ ({NAT})
= SCM-Data-Loc \ ({NAT}) by XBOOLE_1:40
.= Int-Locations by A3,XBOOLE_1:83;
thus Data-Locations SCM+FSA
= SCM-Memory \/ FinSeq-Locations \ ({NAT})
by SCMFSA_1:5,SUBSET_1:def 8
.= Int-Locations \/ FinSeq-Locations by A2,A4,XBOOLE_1:42;
end;
theorem
for i,j being Nat st i <> j
holds intloc i <> intloc j by AMI_3:10;
reserve n for Nat,
I for Program of SCM+FSA;
theorem
not a in dom Start-At(l,SCM+FSA)
proof
assume a in dom Start-At(l,SCM+FSA);
then a = IC SCM+FSA by TARSKI:def 1;
hence contradiction by Th49;
end;
theorem
not f in dom Start-At(l,SCM+FSA)
proof
assume f in dom Start-At(l,SCM+FSA);
then f = IC SCM+FSA by TARSKI:def 1;
hence contradiction by Th50;
end;
theorem
for s1,s2 being State of SCM+FSA st IC s1 = IC s2 &
(for a being Int-Location holds s1.a = s2.a) &
(for f being FinSeq-Location holds s1.f = s2.f)
holds s1 = s2
proof
let s1,s2 be State of SCM+FSA such that
A1: IC s1 = IC s2;
IC SCM+FSA in dom s1 & IC SCM+FSA in dom s2 by MEMSTR_0:2;
then
A2: s1 = DataPart s1 +* Start-At (IC s1,SCM+FSA) &
s2 = DataPart s2 +* Start-At (IC s2,SCM+FSA) by MEMSTR_0:26;
assume that
A3: for a being Int-Location holds s1.a = s2.a and
A4: for f being FinSeq-Location holds s1.f = s2.f;
DataPart s1 = DataPart s2
proof
A5: dom DataPart s1 = Data-Locations SCM+FSA by MEMSTR_0:9;
hence dom DataPart s1 = dom DataPart s2 by MEMSTR_0:9;
let x be object;
assume
A6: x in dom DataPart s1;
then
A7: x in Int-Locations \/ FinSeq-Locations by A5,Th92;
per cases by A7,XBOOLE_0:def 3;
suppose x in Int-Locations;
then
A8: x is Int-Location by AMI_2:def 16;
thus (DataPart s1).x = s1.x by A6,A5,FUNCT_1:49
.= s2.x by A8,A3
.= (DataPart s2).x by A6,A5,FUNCT_1:49;
end;
suppose x in FinSeq-Locations;
then
A9: x is FinSeq-Location by Def3;
thus (DataPart s1).x = s1.x by A6,A5,FUNCT_1:49
.= s2.x by A9,A4
.= (DataPart s2).x by A6,A5,FUNCT_1:49;
end;
end;
hence thesis by A1,A2;
end;
registration let f be FinSeq-Location, w be FinSequence of INT;
cluster f .--> w -> data-only for PartState of SCM+FSA;
coherence by Th50,ZFMISC_1:11;
end;
registration let x be Int-Location, i be Integer;
cluster x .--> i -> data-only for PartState of SCM+FSA;
coherence by Th49,ZFMISC_1:11;
end;
registration let a,b;
cluster a:=b -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let a,b;
cluster AddTo(a,b) -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let a,b;
cluster SubFrom(a,b) -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let a,b;
cluster MultBy(a,b) -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let a,b;
cluster Divide(a,b) -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let lb;
cluster goto lb -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let lb,a;
cluster a=0_goto lb -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let lb,a;
cluster a>0_goto lb -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let fa,a,c;
cluster c:= (fa,a) -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let fa,a,c;
cluster (fa,a):=c -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let fa,a;
cluster a:=len fa -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;
registration let fa,a;
cluster fa:=<0,...,0>a -> No-StopCode;
coherence
proof
InsCode halt SCM+FSA = 0;
hence thesis;
end;
end;