:: On the Decomposition of the States of SCM
:: by Yasushi Tanaka
::
:: Received November 23, 1993
:: Copyright (c) 1993-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, AMI_3, SUBSET_1, AMI_2, AMI_1, STRUCT_0, XBOOLE_0,
FSM_1, RELAT_1, FUNCT_1, TARSKI, FINSET_1, CARD_1, XXREAL_0, FINSEQ_1,
GRAPHSP, ARYTM_3, ARYTM_1, INT_1, FUNCT_4, FUNCOP_1, CIRCUIT2, PARTFUN1,
EXTPRO_1, RECDEF_2, CAT_1, AMISTD_5, COMPOS_1, NAT_1;
notations TARSKI, XBOOLE_0, XTUPLE_0, SUBSET_1, ORDINAL1, CARD_1, XCMPLX_0,
DOMAIN_1, RELAT_1, FUNCT_1, FUNCOP_1, PARTFUN1, FUNCT_4, NUMBERS, INT_1,
NAT_1, RECDEF_2, STRUCT_0, FINSET_1, FINSEQ_1, MEMSTR_0, COMPOS_0,
SCM_INST, COMPOS_1, EXTPRO_1, AMI_3, XXREAL_0, AMISTD_5;
constructors DOMAIN_1, FINSEQ_4, AMI_3, PRE_POLY, AMISTD_5, FUNCT_7, RELSET_1;
registrations XBOOLE_0, SETFAM_1, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, INT_1,
AMI_3, FINSET_1, CARD_1, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1, MEMSTR_0,
COMPOS_0, XTUPLE_0, FACIRC_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions EXTPRO_1, FUNCT_1, AMISTD_5;
equalities EXTPRO_1, AMI_3, FUNCOP_1, AMI_2, MEMSTR_0, SCM_INST;
theorems AMI_3, GRFUNC_1, TARSKI, FUNCOP_1, FUNCT_4, MEMSTR_0, FUNCT_1,
ZFMISC_1, ENUMSET1, RELAT_1, XBOOLE_0, XBOOLE_1, PBOOLE, PARTFUN1,
EXTPRO_1, AMISTD_5, AMI_2, COMPOS_1;
begin
reserve x,y for set;
theorem Th1:
for dl being Data-Location ex i being Nat st dl = dl.i
proof
let dl be Data-Location;
dl in Data-Locations SCM by AMI_2:def 16,AMI_3:27;
then consider x,y being object such that
A1: x in {1} and
A2: y in NAT and
A3: dl = [x,y] by AMI_3:27,ZFMISC_1:84;
reconsider k = y as Nat by A2;
take k;
thus thesis by A1,A3,TARSKI:def 1;
end;
theorem Th2:
for dl being Data-Location holds dl <> IC SCM
by Th1,AMI_3:13;
theorem
for il being Nat, dl being Data-Location
holds il <> dl
proof
let il be Nat, dl be Data-Location;
ex j being Nat st dl = dl.j by Th1;
hence thesis;
end;
reserve i, j, k for Nat;
theorem
for s being State of SCM, d being Data-Location
holds d in dom s
proof
let s be State of SCM, d be Data-Location;
A1: dom s = the carrier of SCM by PARTFUN1:def 2;
thus d in dom s by A1;
end;
registration
cluster Data-Locations SCM -> infinite;
coherence by AMI_3:27;
end;
reserve I,J,K for Element of Segm 9,
a,a1 for Nat,
b,b1,c for Element of Data-Locations SCM;
Lm1:
b is Data-Location
proof
b in Data-Locations SCM;
then reconsider b as Object of SCM;
b is Data-Location by AMI_2:def 16,AMI_3:27;
hence thesis;
end;
theorem
for l being Instruction of SCM holds InsCode(l) <= 8
proof
let l be Instruction of SCM;
l in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] : K in { 7,8 } }
or l in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} }
by AMI_3:27,XBOOLE_0:def 3;
then
A1: l in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
or l in { [K,<*a1*>,<*b1*>]
: K in { 7,8 } } or l in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} } by
XBOOLE_0:def 3;
per cases by A1,XBOOLE_0:def 3;
suppose
l in { [SCM-Halt,{},{}] };
then l = [SCM-Halt,{},{}] by TARSKI:def 1;
then l`1_3 = 0;
hence thesis;
end;
suppose
l in { [J,<*a*>,{}] : J = 6 };
then ex J,a st l = [J,<*a*>,{}] & J = 6;
then l`1_3 = 6;
hence thesis;
end;
suppose
l in { [K,<*a1*>,<*b1*>] : K in { 7,8 } };
then ex K,a1,b1 st l = [K,<*a1*>,<*b1*>] & K in { 7,8 };
then l`1_3 in { 7,8 };
then l`1_3 = 7 or l`1_3 = 8 by TARSKI:def 2;
hence thesis;
end;
suppose
l in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} };
then ex I,b,c st l = [I,{},<*b,c*>] & I in { 1,2,3,4,5};
then l`1_3 in { 1,2,3,4,5};
then l`1_3 = 1 or l`1_3 = 2 or l`1_3 = 3 or l`1_3 = 4 or l`1_3 = 5
by ENUMSET1:def 3;
hence thesis;
end;
end;
reserve a, b for Data-Location,
loc for Nat;
reserve I,J,K for Element of Segm 9,
a,a1 for Nat,
b,b1,c for Element of Data-Locations SCM,
da,db for Data-Location;
::$CT
theorem
for ins being Instruction of SCM st InsCode ins = 0 holds ins = halt SCM
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 0;
A2: now
assume ins in { [J,<*a*>,{}] : J = 6 };
then ex J,a st ins = [J,<*a*>,{}] & J = 6;
then InsCode ins = 6;
hence contradiction by A1;
end;
now
assume ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} };
then ex I,b,c st ins = [I,{},<*b,c*>] & I in { 1,2,3,4,5};
then InsCode ins in { 1,2,3,4,5};
hence contradiction by A1,ENUMSET1:def 3;
end;
then
A3: ins in { [SCM-Halt,{},{}] }
\/ { [J,<*a*>,{}] : J = 6 } \/ { [K,<*a1*>,<*b1*>] :
K in { 7,8 } } by AMI_3:27,XBOOLE_0:def 3;
now
assume ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } };
then ex K,a1,b1 st ins = [K,<*a1*>,<*b1*>] & K in { 7,8 };
then InsCode ins in {7,8};
hence contradiction by A1, TARSKI:def 2;
end;
then ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
by A3,XBOOLE_0:def 3;
then ins in {[SCM-Halt,{},{}]} by A2,XBOOLE_0:def 3;
then ins = [SCM-Halt,{},{}] by TARSKI:def 1;
hence thesis by AMI_3:26;
end;
theorem
for ins being Instruction of SCM st InsCode ins = 1 holds ex da,
db st ins = da:=db
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 1;
A2: now
assume ins in { [J,<*a*>,{}] : J = 6 };
then ex J,a st ins = [J,<*a*>,{}] & J = 6;
hence contradiction by A1;
end;
A3: now
assume ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } };
then consider K,a1,b1 such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in { 7,8 };
InsCode ins = K by A4;
hence contradiction by A1,A5,TARSKI:def 2;
end;
InsCode halt SCM = 0 by COMPOS_1:70;
then not ins in { [SCM-Halt,{},{}] } by A1,AMI_3:26,TARSKI:def 1;
then not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 } by A2,
XBOOLE_0:def 3;
then
not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 3;
then ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} }
by AMI_3:27,XBOOLE_0:def 3;
then consider I,b,c such that
A6: ins = [I,{},<*b,c*>] and
I in { 1,2,3,4,5};
reconsider da = b ,db = c as Data-Location by Lm1;
take da,db;
thus thesis by A1,A6;
end;
theorem
for ins being Instruction of SCM st InsCode ins = 2 holds ex da,
db st ins = AddTo(da,db)
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 2;
A2: now
assume ins in { [J,<*a*>,{}] : J = 6 };
then ex J,a st ins = [J,<*a*>,{}] & J = 6;
hence contradiction by A1;
end;
A3: now
assume ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } };
then consider K,a1,b1 such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in { 7,8 };
InsCode ins = K by A4;
hence contradiction by A1,A5,TARSKI:def 2;
end;
InsCode halt SCM = 0 by COMPOS_1:70;
then not ins in { [SCM-Halt,{},{}] } by A1,AMI_3:26,TARSKI:def 1;
then not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 } by A2,
XBOOLE_0:def 3;
then
not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 3;
then ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} }
by AMI_3:27,XBOOLE_0:def 3;
then consider I,b,c such that
A6: ins = [I,{},<*b,c*>] and
I in { 1,2,3,4,5};
reconsider da = b ,db = c as Data-Location by Lm1;
take da,db;
thus thesis by A1,A6;
end;
theorem
for ins being Instruction of SCM st InsCode ins = 3 holds ex da,
db st ins = SubFrom(da,db)
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 3;
A2: now
assume ins in { [J,<*a*>,{}] : J = 6 };
then ex J,a st ins = [J,<*a*>,{}] & J = 6;
hence contradiction by A1;
end;
A3: now
assume ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } };
then consider K,a1,b1 such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in { 7,8 };
InsCode ins = K by A4;
hence contradiction by A1,A5,TARSKI:def 2;
end;
InsCode halt SCM = 0 by COMPOS_1:70;
then not ins in { [SCM-Halt,{},{}] } by A1,AMI_3:26,TARSKI:def 1;
then not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 } by A2,
XBOOLE_0:def 3;
then
not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 3;
then ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} }
by AMI_3:27,XBOOLE_0:def 3;
then consider I,b,c such that
A6: ins = [I,{},<*b,c*>] and
I in { 1,2,3,4,5};
reconsider da = b ,db = c as Data-Location by Lm1;
take da,db;
thus thesis by A1,A6;
end;
theorem
for ins being Instruction of SCM st InsCode ins = 4 holds ex da,
db st ins = MultBy(da,db)
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 4;
A2: now
assume ins in { [J,<*a*>,{}] : J = 6 };
then ex J,a st ins = [J,<*a*>,{}] & J = 6;
hence contradiction by A1;
end;
A3: now
assume ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } };
then consider K,a1,b1 such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in { 7,8 };
InsCode ins = K by A4;
hence contradiction by A1,A5,TARSKI:def 2;
end;
InsCode halt SCM = 0 by COMPOS_1:70;
then not ins in { [SCM-Halt,{},{}] } by A1,AMI_3:26,TARSKI:def 1;
then not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 } by A2,
XBOOLE_0:def 3;
then
not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 3;
then ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} }
by AMI_3:27,XBOOLE_0:def 3;
then consider I,b,c such that
A6: ins = [I,{},<*b,c*>] and
I in { 1,2,3,4,5};
reconsider da = b ,db = c as Data-Location by Lm1;
take da,db;
thus thesis by A1,A6;
end;
theorem
for ins being Instruction of SCM st InsCode ins = 5 holds ex da,
db st ins = Divide(da,db)
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 5;
A2: now
assume ins in { [J,<*a*>,{}] : J = 6 };
then ex J,a st ins = [J,<*a*>,{}] & J = 6;
hence contradiction by A1;
end;
A3: now
assume ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } };
then consider K,a1,b1 such that
A4: ins = [K,<*a1*>,<*b1*>] and
A5: K in { 7,8 };
InsCode ins = K by A4;
hence contradiction by A1,A5,TARSKI:def 2;
end;
InsCode halt SCM = 0 by COMPOS_1:70;
then not ins in { [SCM-Halt,{},{}] } by A1,AMI_3:26,TARSKI:def 1;
then not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 } by A2,
XBOOLE_0:def 3;
then
not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] : K in { 7,8 } } by A3,XBOOLE_0:def 3;
then ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} }
by AMI_3:27,XBOOLE_0:def 3;
then consider I,b,c such that
A6: ins = [I,{},<*b,c*>] and
I in { 1,2,3,4,5};
reconsider da = b ,db = c as Data-Location by Lm1;
take da,db;
thus thesis by A1,A6;
end;
theorem
for ins being Instruction of SCM st InsCode ins = 6 holds ex loc
st ins = SCM-goto loc
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 6;
now
assume ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} };
then consider I,b,c such that
A2: ins = [I,{},<*b,c*>] and
A3: I in { 1,2,3,4,5};
InsCode ins = I by A2;
hence contradiction by A1,A3,ENUMSET1:def 3;
end;
then
A4: ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] :
K in { 7,8 } } by AMI_3:27,XBOOLE_0:def 3;
now
assume ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } };
then consider K,a1,b1 such that
A5: ins = [K,<*a1*>,<*b1*>] and
A6: K in { 7,8 };
InsCode ins = K by A5;
hence contradiction by A1,A6,TARSKI:def 2;
end;
then
A7: ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
by A4,XBOOLE_0:def 3;
InsCode halt SCM = 0 by COMPOS_1:70;
then not ins in { [SCM-Halt,{},{}] } by A1,AMI_3:26,TARSKI:def 1;
then ins in { [J,<*a*>,{}] : J = 6 } by A7,XBOOLE_0:def 3;
then consider J,a such that
A8: ins = [J,<*a*>,{}] & J = 6;
reconsider loc = a as Nat;
take loc;
thus thesis by A8;
end;
theorem
for ins being Instruction of SCM st InsCode ins = 7 holds ex loc
,da st ins = da=0_goto loc
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 7;
A2: now
assume ins in { [J,<*a*>,{}] : J = 6 };
then ex J,a st ins = [J,<*a*>,{}] & J = 6;
hence contradiction by A1;
end;
now
assume ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} };
then consider I,b,c such that
A3: ins = [I,{},<*b,c*>] and
A4: I in { 1,2,3,4,5};
InsCode ins = I by A3;
hence contradiction by A1,A4,ENUMSET1:def 3;
end;
then
A5: ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] :
K in { 7,8 } } by AMI_3:27,XBOOLE_0:def 3;
InsCode halt SCM = 0 by COMPOS_1:70;
then not ins in { [SCM-Halt,{},{}] } by A1,AMI_3:26,TARSKI:def 1;
then not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 } by A2,
XBOOLE_0:def 3;
then ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } } by A5,XBOOLE_0:def 3;
then consider K,a1,b1 such that
A6: ins = [K,<*a1*>,<*b1*>] and
K in { 7,8 };
reconsider da = b1 as Data-Location by Lm1;
reconsider loc = a1 as Nat;
take loc,da;
thus thesis by A1,A6;
end;
theorem
for ins being Instruction of SCM st InsCode ins = 8 holds ex loc
,da st ins = da>0_goto loc
proof
let ins be Instruction of SCM such that
A1: InsCode ins = 8;
A2: now
assume ins in { [J,<*a*>,{}] : J = 6 };
then ex J,a st ins = [J,<*a*>,{}] & J = 6;
hence contradiction by A1;
end;
now
assume ins in { [I,{},<*b,c*>] : I in { 1,2,3,4,5} };
then consider I,b,c such that
A3: ins = [I,{},<*b,c*>] and
A4: I in { 1,2,3,4,5};
InsCode ins = I by A3;
hence contradiction by A1,A4,ENUMSET1:def 3;
end;
then
A5: ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 }
\/ { [K,<*a1*>,<*b1*>] : K in { 7,8 } } by AMI_3:27,XBOOLE_0:def 3;
InsCode halt SCM = 0 by COMPOS_1:70;
then not ins in { [SCM-Halt,{},{}] } by A1,AMI_3:26,TARSKI:def 1;
then not ins in { [SCM-Halt,{},{}] } \/ { [J,<*a*>,{}] : J = 6 } by A2,
XBOOLE_0:def 3;
then ins in { [K,<*a1*>,<*b1*>] : K in { 7,8 } } by A5,XBOOLE_0:def 3;
then consider K,a1,b1 such that
A6: ins = [K,<*a1*>,<*b1*>] and
K in { 7,8 };
reconsider da = b1 as Data-Location by Lm1;
reconsider loc = a1 as Nat;
take loc,da;
thus thesis by A1,A6;
end;
begin :: Finite partial states of SCM
theorem
for s being State of SCM, iloc being Nat, a
being Data-Location holds s.a = (s +* Start-At(iloc,SCM)).a
proof
let s be State of SCM, iloc be Nat, a be
Data-Location;
a in the carrier of SCM;
then a in dom s by PARTFUN1:def 2;
then
A1: dom (Start-At(iloc,SCM)) = {IC SCM} &
a in dom s \/ dom (Start-At(iloc,SCM)) by XBOOLE_0:def 3;
a <> IC SCM by Th2;
then not a in {IC SCM} by TARSKI:def 1;
hence thesis by A1,FUNCT_4:def 1;
end;
begin :: Autonomic finite partial states of SCM
registration
cluster SCM -> IC-recognized;
coherence
proof
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic
FinPartState of SCM st DataPart p <> {}
holds IC SCM in dom p
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic FinPartState of SCM;
assume DataPart p <> {};
then
A1: dom DataPart p <> {};
assume
A2: not IC SCM in dom p;
then dom p misses {IC SCM} by ZFMISC_1:50;
then
A3: dom p /\ {IC SCM} = {} by XBOOLE_0:def 7;
p is not q-autonomic
proof
set il = the Element of (NAT \ dom q);
set d2 = the Element of Data-Locations SCM \ dom p;
set d1 = the Element of dom DataPart p;
A4: d1 in dom DataPart p by A1;
DataPart p c= p by MEMSTR_0:12;
then
A5: dom DataPart p c= dom p by RELAT_1:11;
dom DataPart p c= the carrier of SCM by RELAT_1:def 18;
then reconsider d1 as Element of SCM by A4;
not Data-Locations SCM c= dom p;
then
A6: Data-Locations SCM \ dom p <> {} by XBOOLE_1:37;
then d2 in Data-Locations SCM by XBOOLE_0:def 5;
then reconsider d2 as Data-Location by AMI_2:def 16,AMI_3:27;
A7: not d2 in dom p by A6,XBOOLE_0:def 5;
then
A8: dom p misses {d2} by ZFMISC_1:50;
not NAT c= dom q;
then
A9: (NAT) \ dom q <> {} by XBOOLE_1:37;
then reconsider il as Element of NAT by XBOOLE_0:def 5;
A10: not il in dom q by A9,XBOOLE_0:def 5;
dom DataPart p c= Data-Locations SCM by RELAT_1:58;
then reconsider d1 as Data-Location by A4,AMI_2:def 16,AMI_3:27;
set p2 = p +* (( d2.--> 1) +* Start-At(il,SCM));
set p1 = p +* (( d2.--> 0) +* Start-At(il,SCM));
set q2 = q +* (il .--> (d1:=d2));
set q1 = q +* (il .--> (d1:=d2));
consider s1 being State of SCM such that
A11: p1 c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCM
such that
A12: q1 c= S1 by PBOOLE:145;
A13: dom p misses {d2} by A7,ZFMISC_1:50;
A14: dom (( d2.--> 1) +* Start-At(il,SCM))
= dom ( d2.--> 1) \/ dom(Start-At(il,SCM)) by FUNCT_4:def 1;
consider s2 being State of SCM such that
A15: p2 c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCM
such that
A16: q2 c= S2 by PBOOLE:145;
A17: dom p c= the carrier of SCM by RELAT_1:def 18;
dom ( Comput(S2,s2,1)) = the carrier of SCM by PARTFUN1:def 2;
then
A18: dom ( Comput(S2,s2,1)|dom p) = dom p
by A17,RELAT_1:62;
A19: dom ( Comput(S1,s1,1)) = the carrier of SCM by PARTFUN1:def 2;
A20: dom ( Comput(S1,s1,1)|dom p) = dom p
by A17,A19,RELAT_1:62;
A21: dom p2 = dom p \/ dom (( d2.--> 1) +* Start-At(il,SCM)) by FUNCT_4:def 1;
A22: dom q2 = dom q \/ dom ((il .--> (d1:=d2))) by FUNCT_4:def 1;
A24: IC SCM in dom (Start-At(il,SCM)) by TARSKI:def 1;
then
A25: IC SCM in dom (( d2.--> 1) +* Start-At(il,SCM)) by A14,XBOOLE_0:def 3;
then IC SCM in dom p2 by A21,XBOOLE_0:def 3;
then
A26: IC s2 = p2.IC SCM by A15,GRFUNC_1:2
.= (( d2.--> 1) +* Start-At(il,SCM)).IC SCM by A25,FUNCT_4:13
.= (Start-At(il,SCM)).IC SCM by A24,FUNCT_4:13
.= il by FUNCOP_1:72;
d2 <> IC SCM by Th2;
then
A27: not d2 in dom (Start-At(il,SCM)) by TARSKI:def 1;
d2 in dom ( d2.--> 1) by TARSKI:def 1;
then
A28: d2 in dom (( d2.--> 1) +* Start-At(il,SCM)) by A14,XBOOLE_0:def 3;
then d2 in dom p2 by A21,XBOOLE_0:def 3;
then
A29: s2.d2 = p2.d2 by A15,GRFUNC_1:2
.= (( d2.--> 1) +* Start-At(il,SCM)).d2 by A28,FUNCT_4:13
.= (( d2.--> 1)).d2 by A27,FUNCT_4:11
.= 1 by FUNCOP_1:72;
A31: il in dom (il .--> (d1:=d2)) by TARSKI:def 1;
then il in dom q2 by A22,XBOOLE_0:def 3;
then
A32: S2.il = q2.il by A16,GRFUNC_1:2
.= (il .--> (d1:=d2)).il by A31,FUNCT_4:13
.=(d1:=d2) by FUNCOP_1:72;
A33: (S2)/.IC s2 = S2.IC s2 by PBOOLE:143;
A34: Comput(S2,s2,0+1).d1
= (Following(S2,Comput(S2,s2,0))).d1 by EXTPRO_1:3
.= (Following(S2,s2)).d1
.= 1 by A26,A32,A29,A33,AMI_3:2;
dom p misses {IC SCM} by A2,ZFMISC_1:50;
then
A35: dom p /\ {IC SCM} = {} by XBOOLE_0:def 7;
take P = S1, Q = S2;
dom (( d2.--> 0) +* Start-At(il,SCM))
= dom(( d2.--> 0)) \/ dom(Start-At(il,SCM)) by FUNCT_4:def 1
.= dom(( d2.--> 0)) \/ {IC SCM}
.= {d2} \/ {IC SCM};
then
dom p /\ dom (( d2.--> 0) +* Start-At(il,SCM))
= dom p /\ {d2} \/ {} by A35,XBOOLE_1:23
.= {} by A8,XBOOLE_0:def 7;
then dom p misses dom (( d2.--> 0) +* Start-At(il,SCM))
by XBOOLE_0:def 7;
then
p c= p1 by FUNCT_4:32;
then
A36: p c= s1 by A11,XBOOLE_1:1;
dom q misses dom (il .--> (d1:=d2)) by A10,ZFMISC_1:50;
then q c= q1 by FUNCT_4:32;
hence q c= P by A12,XBOOLE_1:1;
A37: dom p1 = dom p \/ dom (( d2.--> 0) +* Start-At(
il,SCM)) by FUNCT_4:def 1;
dom ((d2.--> 1) +* Start-At(il,SCM))
= dom(( d2.--> 1)) \/ dom(Start-At(il,SCM)) by FUNCT_4:def 1
.= dom(( d2.--> 1)) \/ {IC SCM}
.= {d2} \/ {IC SCM};
then
dom p /\ dom (( d2.--> 1) +* Start-At(il,SCM)) = dom
p /\ ({d2}) \/ {} by A3,XBOOLE_1:23
.= {} by A13,XBOOLE_0:def 7;
then dom p misses
dom (( d2.--> 1) +* Start-At(il,SCM))
by XBOOLE_0:def 7;
then p c= p2 by FUNCT_4:32;
then
A38: p c= s2 by A15,XBOOLE_1:1;
dom q misses dom (il .--> (d1:=d2)) by A10,ZFMISC_1:50;
then q c= q2 by FUNCT_4:32;
hence q c= Q by A16,XBOOLE_1:1;
take s1,s2;
thus p c= s1 by A36;
thus p c= s2 by A38;
take 1;
A39: dom (( d2.--> 0) +* Start-At(il,SCM))
= dom (( d2.--> 0)) \/ dom(Start-At(il,SCM)) by FUNCT_4:def 1;
A41: IC SCM in dom (Start-At(il,SCM)) by TARSKI:def 1;
then
A42: IC SCM in dom (( d2.--> 0) +* Start-At(il,SCM))
by A39,XBOOLE_0:def 3;
then IC SCM in dom p1 by A37,XBOOLE_0:def 3;
then
A43: IC s1 = p1.IC SCM by A11,GRFUNC_1:2
.= (( d2.--> 0) +* Start-At(il,SCM)).IC SCM by A42,FUNCT_4:13
.= (Start-At(il,SCM)).IC SCM by A41,FUNCT_4:13
.= il by FUNCOP_1:72;
d2 <> IC SCM by Th2;
then
A44: not d2 in dom (Start-At(il,SCM)) by TARSKI:def 1;
d2 in dom ( d2.--> 0) by TARSKI:def 1;
then
A45: d2 in dom (( d2.--> 0) +* Start-At(il,SCM)) by A39,XBOOLE_0:def 3;
then d2 in dom p1 by A37,XBOOLE_0:def 3;
then
A46: s1.d2 = p1.d2 by A11,GRFUNC_1:2
.= (( d2.--> 0) +* Start-At(il,SCM)).d2 by A45,FUNCT_4:13
.= (( d2.--> 0)).d2 by A44,FUNCT_4:11
.= 0 by FUNCOP_1:72;
A47: il in dom(il .--> (d1:=d2)) by TARSKI:def 1;
dom q1 = dom q \/ dom ((il .--> (d1:=d2))) by FUNCT_4:def 1;
then il in dom q1 by A47,XBOOLE_0:def 3;
then
A48: S1.il = q1.il by A12,GRFUNC_1:2
.= (il .--> (d1:=d2)).il by A47,FUNCT_4:13
.=(d1:=d2) by FUNCOP_1:72;
A49: (S1)/.IC s1 = S1.IC s1 by PBOOLE:143;
Comput(S1,s1,0+1).d1
= (Following(S1,Comput(S1,s1,0))).d1 by EXTPRO_1:3
.= 0 by A43,A48,A46,A49,AMI_3:2;
then (Comput(P,s1,1)|dom p).d1 = 0 by A4,A5,A20,FUNCT_1:47;
hence Comput(P,s1,1)|dom p
<> Comput(Q,s2,1)|dom p by A18,A34,A4,A5,FUNCT_1:47;
end;
hence contradiction;
end;
hence thesis by AMISTD_5:3;
end;
end;
registration
cluster SCM -> CurIns-recognized;
coherence
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s be State of SCM such that
A1: p c= s;
let P be Instruction-Sequence of SCM such that
A2: q c= P;
let i be Nat;
set Csi = Comput(P,s,i);
set loc = IC Csi;
assume
A3: not IC Comput(P,s,i) in dom q;
set I = dl.0 := dl.0;
set q1 = q +* (loc .--> I);
set q2 = q +* (loc .--> halt SCM);
reconsider P1 = P +* (loc .--> I)
as Instruction-Sequence of SCM;
reconsider P2 = P +* (loc .--> halt SCM)
as Instruction-Sequence of SCM;
A5: loc in dom (loc .--> halt SCM) by TARSKI:def 1;
A7: loc in dom (loc .--> I) by TARSKI:def 1;
A8: dom q misses dom (loc .--> halt SCM) by A3,ZFMISC_1:50;
A9: dom q misses dom (loc .--> I) by A3,ZFMISC_1:50;
A10: q1 c= P1 by A2,FUNCT_4:123;
A11: q2 c= P2 by A2,FUNCT_4:123;
set Cs2i = Comput(P2,s,i), Cs1i = Comput(P1,s,i);
p is not q-autonomic
proof
(loc .--> halt SCM).loc = halt SCM by FUNCOP_1:72;
then
A12: P2.loc = halt SCM by A5,FUNCT_4:13;
A13: (loc .--> I).loc = I by FUNCOP_1:72;
take P1, P2;
q c= q1 by A9,FUNCT_4:32;
hence
A14: q c= P1 by A10,XBOOLE_1:1;
q c= q2 by A8,FUNCT_4:32;
hence
A15: q c= P2 by A11,XBOOLE_1:1;
take s, s;
thus p c= s by A1;
A16: (Cs1i|dom p) = (Csi|dom p) by A14,A2,A1,EXTPRO_1:def 10;
thus p c= s by A1;
A17: (Cs1i|dom p) = (Cs2i|dom p) by A14,A15,A1,EXTPRO_1:def 10;
take k = i+1;
set Cs1k = Comput(P1,s,k);
A18: IC SCM in dom p by AMISTD_5:6;
IC Csi = IC(Csi|dom p) by A18,FUNCT_1:49;
then
IC Cs1i = loc by A16,A18,FUNCT_1:49;
then
A19: CurInstr(P1,Cs1i) = P1.loc by PBOOLE:143
.= I by A13,A7,FUNCT_4:13;
A20: Cs1k = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec(I,Cs1i) by A19;
A21: IC Exec(I,Cs1i) = IC Cs1i + 1 by AMI_3:2;
A22: IC SCM in dom p by AMISTD_5:6;
A23: IC Csi = IC(Csi|dom p) by A22,FUNCT_1:49;
then
A24: IC Cs1k = loc+1 by A20,A21,A16,A22,FUNCT_1:49;
set Cs2k = Comput(P2,s,k);
A25: Cs2k = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
A26: P2/.IC Cs2i = P2.IC Cs2i by PBOOLE:143;
IC Cs2i = loc by A16,A23,A17,A22,FUNCT_1:49;
then
A27: IC Cs2k = loc by A25,A12,A26,EXTPRO_1:def 3;
IC(Cs1k|dom p) = IC Cs1k & IC(Cs2k|dom p) = IC Cs2k
by A22,FUNCT_1:49;
hence thesis by A24,A27;
end;
hence contradiction;
end;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM,
s1, s2 being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db being Data-Location,
I being Instruction of SCM
st I = CurInstr(P1,Comput(P1,s1,i))
holds I = da := db & da in dom p implies
Comput(P1,s1,i).db = Comput(P2,s2,i).db
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s1, s2 be State of SCM such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Data-Location, I be Instruction of SCM
such that
A3: I = CurInstr(P1,Comput(P1,s1,i));
set Cs2i1 = Comput(P2,s2,i+1);
set Cs2i = Comput(P2,s2,i);
A4: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A5: I = da := db and
A6: da in dom p & Comput(P1,s1,i).db <> Comput(P2,s2,
i).db;
I = CurInstr(P2,Comput(P2,s2,i)) by A3,A2,A1,AMISTD_5:7;
then
A7: Cs2i1.da = Cs2i.db by A4,A5,AMI_3:2;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs1i = Comput(P1,s1,i);
A8: da in dom p implies (Cs1i1|dom p).da = Cs1i1.da &
(Cs2i1|dom p).da = Cs2i1.da by FUNCT_1:49;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then Cs1i1.da = Cs1i.db by A3,A5,AMI_3:2;
hence contradiction by A8,A6,A7,A2,A1,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM st
I = CurInstr(P1,Comput(P1,
s1,i))
holds I = AddTo(da, db) & da in dom p implies Comput(P1,s1,i).da
+
Comput(P1,s1,i).db = Comput(P2,s2,i).da + Comput(
P2,s2,i).db
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s1, s2 be State of
SCM such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Data-Location, I be Instruction of SCM
such that
A3: I = CurInstr(P1,Comput(P1,s1,i));
set Cs2i1 = Comput(P2,s2,i+1);
set Cs2i = Comput(P2,s2,i);
A4: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A5: I = AddTo(da, db) and
A6: da in dom p & Comput(P1,s1,i).da + Comput(P1,s1,i
).db <>
Comput(P2,s2, i).da + Comput(P2,s2,i).db;
I = CurInstr(P2,Comput(P2,s2,i)) by A3,A2,A1,AMISTD_5:7;
then
A7: Cs2i1.da = Cs2i.da + Cs2i.db by A4,A5,AMI_3:3;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs1i = Comput(P1,s1,i);
A8: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then Cs1i1.da = Cs1i.da + Cs1i.db by A3,A5,AMI_3:3;
hence contradiction by A8,A6,A7,A2,A1,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM st
I = CurInstr(P1,Comput(P1,
s1,i))
holds I = SubFrom(da, db) & da in dom p implies Comput(P1,s1,i).
da -
Comput(P1,s1,i).db = Comput(P2,s2,i).da - Comput(
P2,s2,i).db
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s1, s2 be State of
SCM such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Data-Location, I be Instruction of SCM
such that
A3: I = CurInstr(P1,Comput(P1,s1,i));
set Cs2i1 = Comput(P2,s2,i+1);
set Cs2i = Comput(P2,s2,i);
A4: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A5: I = SubFrom(da, db) and
A6: da in dom p & Comput(P1,s1,i).da - Comput(P1,s1,i
).db <>
Comput(P2,s2, i).da - Comput(P2,s2,i).db;
I = CurInstr(P2,Comput(P2,s2,i)) by A3,A2,A1,AMISTD_5:7;
then
A7: Cs2i1.da = Cs2i.da - Cs2i.db by A4,A5,AMI_3:4;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs1i = Comput(P1,s1,i);
A8: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then Cs1i1.da = Cs1i.da - Cs1i.db by A3,A5,AMI_3:4;
hence contradiction by A8,A6,A7,A2,A1,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM
st I = CurInstr(P1,Comput(P1,s1,i))
holds I = MultBy(da, db) & da in dom p implies Comput(P1,s1,i).
da *
Comput(P1,s1,i).db = Comput(P2,s2,i).da * Comput(P2,s2,i).db
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s1, s2 be State of
SCM such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Data-Location, I be Instruction of SCM
such that
A3: I = CurInstr(P1,Comput(P1,s1,i));
set Cs2i1 = Comput(P2,s2,i+1);
set Cs2i = Comput(P2,s2,i);
A4: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A5: I = MultBy(da, db) and
A6: da in dom p & Comput(P1,s1,i).da * Comput(P1,s1,i
).db <>
Comput(P2,s2, i).da * Comput(P2,s2,i).db;
I = CurInstr(P2,Comput(P2,s2,i)) by A3,A2,A1,AMISTD_5:7;
then
A7: Cs2i1.da = Cs2i.da * Cs2i.db by A4,A5,AMI_3:5;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs1i = Comput(P1,s1,i);
A8: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then Cs1i1.da = Cs1i.da * Cs1i.db by A3,A5,AMI_3:5;
hence contradiction by A8,A6,A7,A2,A1,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM
st I = CurInstr(P1,Comput(P1,s1,i))
holds I = Divide(da, db) & da in dom p & da <> db implies
Comput(P1,s1
,i).da div Comput(P1,s1,i).db = Comput(P2,s2,i).da
div Comput(P2,s2,i).db
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s1, s2 be State of
SCM such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Data-Location, I be Instruction of SCM
such that
A3: I = CurInstr(P1,Comput(P1,s1,i));
set Cs2i1 = Comput(P2,s2,i+1);
set Cs2i = Comput(P2,s2,i);
A4: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A5: I = Divide(da, db) and
A6: da in dom p and
A7: da <> db and
A8: Comput(P1,s1,i).da div Comput(P1,s1,i).db <> Comput(P2,s2,i).
da div Comput(P2,s2,i).db;
I = CurInstr(P2,Comput(P2,s2,i)) by A3,A2,A1,AMISTD_5:7;
then
A9: Cs2i1.da = Cs2i.da div Cs2i.db by A4,A5,A7,AMI_3:6;
set Cs1i1 = Comput(P1,s1,i+1);
set Cs1i = Comput(P1,s1,i);
A10: da in dom p implies
(Cs1i1|dom p).da = Cs1i1.da & (Cs2i1|dom p).da =
Cs2i1.da by FUNCT_1:49;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then Cs1i1.da = Cs1i.da div Cs1i.db by A3,A5,A7,AMI_3:6;
hence contradiction by A10,A8,A9,A2,A6,A1,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da, db
being Data-Location, I being Instruction of SCM st
I = CurInstr(P1,Comput(P1,s1,i))
holds I = Divide(da, db) & db in dom p implies Comput(P1,s1,i).
da mod
Comput(P1,s1,i).db = Comput(P2,s2,i).da mod Comput(P2,s2,i).db
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s1, s2 be State of
SCM such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM
such that
A2: q c= P1 & q c= P2;
let i be Nat, da, db be Data-Location, I be Instruction of SCM
such that
A3: I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i1 = Comput(P1,s1,i+1);
set Cs1i = Comput(P1,s1,i);
set Cs2i1 = Comput(P2,s2,i+1);
set Cs2i = Comput(P2,s2,i);
A4: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A5: I = Divide(da, db) and
A6: db in dom p and
A7: Comput(P1,s1,i).da mod Comput(P1,s1,i).db <>
Comput(P2,s2,i).
da mod Comput(P2,s2,i).db;
A8: (Cs1i1|dom p).db = Cs1i1.db &
(Cs2i1|dom p).db = Cs2i1.db by A6,FUNCT_1:49;
I = CurInstr(P2,Comput(P2,s2,i)) by A3,A2,A1,AMISTD_5:7;
then
A9: Cs2i1.db = Cs2i.da mod Cs2i.db by A4,A5,AMI_3:6;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then Cs1i1.db = Cs1i.da mod Cs1i.db by A3,A5,AMI_3:6;
hence contradiction by A7,A8,A9,A2,A1,EXTPRO_1:def 10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da being
Data-Location, loc being Nat, I being Instruction of
SCM st I = CurInstr(P1,Comput(P1,s1,i))
holds I = da=0_goto loc & loc <> (IC Comput(P1,s1,i)) + 1
implies ( Comput(P1,s1,i).da = 0 iff Comput(P2,s2,i)
.da = 0)
proof
let q be non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s1, s2 be State of
SCM such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM
such that
A2: q c= P1 & q c= P2;
let i be Nat, da be Data-Location, loc be Nat
, I be Instruction of SCM such that
A3: I = CurInstr(P1,Comput(P1,s1,i));
set Cs2i1 = Comput(P2,s2,i+1);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i = Comput(P2,s2,i);
set Cs1i = Comput(P1,s1,i);
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
A5: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
IC SCM in dom p by AMISTD_5:6;
then
A6: (Cs1i1|dom p).IC SCM = IC Cs1i1 &
(Cs2i1|dom p).IC SCM = IC Cs2i1 by FUNCT_1:49;
assume that
A7: I = da=0_goto loc and
A8: loc <> (IC Comput(P1,s1,i)) + 1;
A9: I = CurInstr(P2,Comput(P2,s2,i)) by A3,A2,A1,AMISTD_5:7;
A10: now
assume
Comput(P2,s2,i).da = 0 & Comput(P1,s1,i).da <> 0;
then Cs2i1.IC SCM = loc & Cs1i1.IC SCM = IC Cs1i + 1 by A3,A9,A4,A5,A7,
AMI_3:8;
hence contradiction by A6,A8,A2,A1,EXTPRO_1:def 10;
end;
A11: (Cs1i1|dom p) = (Cs2i1|dom p) by A2,A1,EXTPRO_1:def 10;
now
assume
Comput(P1,s1,i).da = 0 & Comput(P2,s2,i).da <> 0;
then Cs1i1.IC SCM = loc & Cs2i1.IC SCM = IC Cs2i + 1 by A3,A9,A4,A5,A7,
AMI_3:8;
hence contradiction by A6,A11,A8,A2,A1,AMISTD_5:7;
end;
hence thesis by A10;
end;
theorem
for q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCM, s1, s2
being State of SCM st p c= s1 & p c= s2
for P1,P2 being Instruction-Sequence of SCM
st q c= P1 & q c= P2
for i being Nat, da being
Data-Location, loc being Nat, I being Instruction of
SCM st I = CurInstr(P1,Comput(P1,s1,i))
holds I = da>0_goto loc & loc <> (IC Comput(P1,s1,i)) + 1
implies ( Comput(P1,s1,i).da > 0 iff Comput(P2,s2,i)
.da > 0)
proof
let q being non halt-free finite
(the InstructionsF of SCM)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCM,
s1, s2 be State of SCM such that
A1: p c= s1 & p c= s2;
let P1,P2 be Instruction-Sequence of SCM
such that
A2: q c= P1 & q c= P2;
let i be Nat, da be Data-Location, loc be Nat
, I be Instruction of SCM such that
A3: I = CurInstr(P1,Comput(P1,s1,i));
set Cs2i1 = Comput(P2,s2,i+1);
set Cs1i1 = Comput(P1,s1,i+1);
A4: Cs1i1|dom p = Cs2i1|dom p by A2,A1,EXTPRO_1:def 10;
set Cs2i = Comput(P2,s2,i);
set Cs1i = Comput(P1,s1,i);
A5: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
IC SCM in dom p by AMISTD_5:6;
then
A6: (Cs1i1|dom p).IC SCM = IC Cs1i1 &
(Cs2i1|dom p).IC SCM = IC Cs2i1 by FUNCT_1:49;
A7: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A8: I = da>0_goto loc and
A9: loc <> (IC Comput(P1,s1,i)) + 1;
A10: I = CurInstr(P2,Comput(P2,s2,i)) by A3,A2,A1,AMISTD_5:7;
A11: now
assume that
A12: Comput(P2,s2,i).da > 0 and
A13: Comput(P1,s1,i).da <= 0;
Cs2i1.IC SCM = loc by A10,A7,A8,A12,AMI_3:9;
hence contradiction by A3,A5,A6,A4,A8,A9,A13,AMI_3:9;
end;
A14: IC Cs1i = IC Cs2i by A2,A1,AMISTD_5:7;
now
assume that
A15: Comput(P1,s1,i).da > 0 and
A16: Comput(P2,s2,i).da <= 0;
Cs1i1.IC SCM = loc by A3,A5,A8,A15,AMI_3:9;
hence contradiction by A14,A10,A7,A6,A4,A8,A9,A16,AMI_3:9;
end;
hence thesis by A11;
end;
theorem
for s1,s2 being State of SCM st IC(s1) = IC(s2) &
(for a being Data-Location holds s1.a = s2.a)
holds s1 = s2
proof
let s1,s2 be State of SCM such that
A1: IC(s1) = IC(s2);
IC SCM in dom s1 & IC SCM in dom s2 by MEMSTR_0:2;
then
A2: s1 = DataPart s1 +* Start-At (IC s1,SCM) &
s2 = DataPart s2 +* Start-At (IC s2,SCM) by MEMSTR_0:26;
assume
A3: for a being Data-Location holds s1.a = s2.a;
DataPart s1 = DataPart s2
proof
A4: dom DataPart s1 = Data-Locations SCM by MEMSTR_0:9;
hence
dom DataPart s1 = dom DataPart s2 by MEMSTR_0:9;
let x be object;
assume
A5: x in dom DataPart s1;
then
A6: x is Data-Location by A4,AMI_2:def 16,AMI_3:27;
thus (DataPart s1).x = s1.x by A5,A4,FUNCT_1:49
.= s2.x by A6,A3
.= (DataPart s2).x by A5,A4,FUNCT_1:49;
end;
hence thesis by A1,A2;
end;