:: Computation and Program Shift in the SCMPDS Computer
:: by JingChao Chen
::
:: Received June 15, 1999
:: Copyright (c) 1999-2026 Association of Mizar Users
:: (Stowarzyszenie Uzytkownikow Mizara, Bialystok, Poland).
:: This code can be distributed under the GNU General Public Licence
:: version 3.0 or later, or the Creative Commons Attribution-ShareAlike
:: License version 3.0 or later, subject to the binding interpretation
:: detailed in file COPYING.interpretation.
:: See COPYING.GPL and COPYING.CC-BY-SA for the full text of these
:: licenses, or see http://www.gnu.org/licenses/gpl.html and
:: http://creativecommons.org/licenses/by-sa/3.0/.
environ
vocabularies NUMBERS, SUBSET_1, SCMPDS_2, INT_1, FSM_1, AMI_1, COMPLEX1,
ARYTM_3, FUNCT_1, AMI_2, STRUCT_0, XBOOLE_0, RELAT_1, TARSKI, CARD_1,
AMI_3, GRAPHSP, EXTPRO_1, XXREAL_0, ARYTM_1, FUNCT_4, FUNCOP_1, CIRCUIT2,
PARTFUN1, AMISTD_5, FINSET_1, COMPOS_1, GOBRD13, NAT_1;
notations TARSKI, XBOOLE_0, SUBSET_1, ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1,
FUNCT_1, PARTFUN1, FUNCT_4, FINSET_1, INT_1, NAT_1, STRUCT_0, FUNCOP_1,
INT_2, XXREAL_0, MEMSTR_0, COMPOS_1, EXTPRO_1, AMI_2, AMISTD_5, SCMPDS_2;
constructors DOMAIN_1, INT_2, SCMPDS_1, SCMPDS_2, REAL_1, PRE_POLY, AMI_3,
AMISTD_5, FUNCT_7, RELSET_1;
registrations XBOOLE_0, RELAT_1, FUNCT_1, ORDINAL1, XREAL_0, INT_1, CARD_3,
AMI_3, SCMPDS_2, FINSET_1, COMPOS_1, EXTPRO_1, FUNCT_4, FUNCOP_1,
MEMSTR_0, COMPOS_0, NAT_1;
requirements NUMERALS, SUBSET, BOOLE, ARITHM, REAL;
definitions EXTPRO_1, AMISTD_5;
equalities EXTPRO_1, AMI_2, FUNCOP_1, SCMPDS_2, MEMSTR_0;
theorems GRFUNC_1, FUNCOP_1, TARSKI, FUNCT_4, FUNCT_1, ZFMISC_1, INT_1,
RELAT_1, ABSVALUE, SCMPDS_2, XBOOLE_0, XBOOLE_1, NUMBERS, PBOOLE,
PARTFUN1, EXTPRO_1, AMISTD_5, MEMSTR_0, AMI_2;
begin :: Preliminaries
reserve j, k, m, n for Nat,
a,b for Int_position,
k1,k2 for Integer;
reserve P,P1,P2 for Instruction-Sequence of SCMPDS;
theorem
for k1 be Integer,s1,s2 being State of SCMPDS st IC s1 = IC s2
holds ICplusConst(s1,k1)=ICplusConst(s2,k1)
proof
let k1 be Integer,s1,s2 be State of SCMPDS;
A1: ex i being Element of NAT st i = IC s1 & ICplusConst(s1,k1 ) = |.i+k1.|
by SCMPDS_2:def 18;
assume IC s1 = IC s2;
hence thesis by A1,SCMPDS_2:def 18;
end;
theorem
for k1 be Integer,a be Int_position,s1,s2 being State of SCMPDS
st DataPart s1 = DataPart s2 holds s1.DataLoc(s1.a,k1)=s2.DataLoc(s2.a,k1)
proof
let k1 be Integer,a be Int_position,s1,s2 be State of SCMPDS;
assume
A1: DataPart s1 = DataPart s2;
A2: a in SCM-Data-Loc by AMI_2:def 16;
then
A3: s1.a= (DataPart s1).a by FUNCT_1:49,SCMPDS_2:84
.= s2.a by A1,A2,FUNCT_1:49,SCMPDS_2:84;
A4: DataLoc(s1.a,k1) in SCM-Data-Loc by AMI_2:def 16;
hence s1.DataLoc(s1.a,k1)= (DataPart s1).DataLoc(s1.a,k1) by FUNCT_1:49
,SCMPDS_2:84
.= s2.DataLoc(s2.a,k1) by A1,A4,A3,FUNCT_1:49,SCMPDS_2:84;
end;
theorem
for a be Int_position,s1,s2 being State of SCMPDS st DataPart s1
= DataPart s2 holds s1.a=s2.a
proof
let a be Int_position,s1,s2 be State of SCMPDS;
assume
A1: DataPart s1 = DataPart s2;
A2: a in SCM-Data-Loc by AMI_2:def 16;
hence s1.a= (DataPart s1).a by FUNCT_1:49,SCMPDS_2:84
.= s2.a by A1,A2,FUNCT_1:49,SCMPDS_2:84;
end;
theorem
not IC SCMPDS in SCM-Data-Loc
proof
assume IC SCMPDS in SCM-Data-Loc;
then IC SCMPDS is Int_position by AMI_2:def 16;
then Values IC SCMPDS = INT by SCMPDS_2:5;
hence contradiction by MEMSTR_0:def 6,NUMBERS:7;
end;
begin :: Finite partial states of SCMPDS
::$CT
theorem
for s being State of SCMPDS ,iloc being Nat
, a being Int_position holds s.a = (s +* Start-At(iloc,SCMPDS)).a
proof
let s be State of SCMPDS, iloc be Nat, a be
Int_position;
a in the carrier of SCMPDS;
then a in dom s by PARTFUN1:def 2;
then
A1: dom (Start-At(iloc,SCMPDS)) = {IC SCMPDS } &
a in dom s \/ dom (Start-At(iloc,SCMPDS))
by XBOOLE_0:def 3;
a <> IC SCMPDS by SCMPDS_2:43;
then not a in {IC SCMPDS } by TARSKI:def 1;
hence thesis by A1,FUNCT_4:def 1;
end;
theorem
for s, t being State of SCMPDS holds s +* t|(SCM-Data-Loc ) is State
of SCMPDS;
begin :: Autonomic finite partial states of SCMPDS and its computation
definition
let la be Int_position;
let a be Integer;
redefine func la .--> a -> FinPartState of SCMPDS; :: redefines .--> (FUNCOP_1, definition)
coherence
proof
a is Element of INT & Values la = INT by INT_1:def 2,SCMPDS_2:5;
hence thesis;
end;
end;
registration
cluster SCMPDS -> IC-recognized;
coherence
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic FinPartState of SCMPDS such that
A1: p is non empty;
assume
A2: not IC SCMPDS in dom p;
not IC SCMPDS in dom p by A2;
then
A3: dom p misses {IC SCMPDS} by ZFMISC_1:50;
dom p c= {IC SCMPDS} \/ dom DataPart p by MEMSTR_0:32;
then
A4: dom p c= dom DataPart p by A3,XBOOLE_1:73;
A5: dom DataPart p <> {} by A1,A4,XBOOLE_1:3;
DataPart p c= p by MEMSTR_0:12;
then
A6: dom DataPart p c= dom p by RELAT_1:11;
p is not q-autonomic
proof
set il = the Element of (NAT) \ dom q;
set d1 = the Element of dom DataPart p;
A7: d1 in dom DataPart p by A5;
dom DataPart p c= the carrier of SCMPDS by RELAT_1:def 18;
then reconsider d1 as Element of SCMPDS by A7;
not NAT c= dom q;
then
A8: (NAT) \ dom q <> {} by XBOOLE_1:37;
then reconsider il as Element of NAT by XBOOLE_0:def 5;
A9: not il in dom q by A8,XBOOLE_0:def 5;
dom DataPart p c= SCM-Data-Loc by RELAT_1:58,SCMPDS_2:84;
then reconsider d1 as Int_position by A7,AMI_2:def 16;
A10: IC SCMPDS in dom (Start-At(il,SCMPDS)) by TARSKI:def 1;
A11: dom p misses {IC SCMPDS} by A2,ZFMISC_1:50;
set p2 = p +* Start-At(il,SCMPDS);
set p1 = p +* Start-At(il,SCMPDS);
set q2 = q +* (il .--> (d1:=1));
set q1 = q +* (il .--> (d1:=0));
A13: dom q misses dom (il .--> (d1:=1)) by A9,ZFMISC_1:50;
A14: dom q misses dom (il .--> (d1:=0)) by A9,ZFMISC_1:50;
consider s1 being State of SCMPDS such that
A15: p1 c= s1 by PBOOLE:141;
consider S1 being Instruction-Sequence of SCMPDS
such that
A16: q1 c= S1 by PBOOLE:145;
consider s2 being State of SCMPDS such that
A17: p2 c= s2 by PBOOLE:141;
consider S2 being Instruction-Sequence of SCMPDS
such that
A18: q2 c= S2 by PBOOLE:145;
take P1 = S1, P2 = S2;
dom p /\ dom Start-At(il,SCMPDS)
= dom p /\ {IC SCMPDS}
.= {} by A11,XBOOLE_0:def 7
.= {};
then dom p misses dom (Start-At(il,SCMPDS)) by XBOOLE_0:def 7;
then p c= p1 by FUNCT_4:32;
then
A19: p c= s1 by A15,XBOOLE_1:1;
q c= q1 by A14,FUNCT_4:32;
hence q c= P1 by A16,XBOOLE_1:1;
dom p /\ dom (Start-At(il,SCMPDS))
= dom p /\ {IC SCMPDS}
.= {} by A11,XBOOLE_0:def 7
.= {};
then dom p misses dom (Start-At(il,SCMPDS)) by XBOOLE_0:def 7;
then p c= p2 by FUNCT_4:32;
then
A20: p c= s2 by A17,XBOOLE_1:1;
q c= q2 by A13,FUNCT_4:32;
hence q c= P2 by A18,XBOOLE_1:1;
take s1,s2;
p c= s1 by A19;
hence p c= s1;
thus p c= s2 by A20;
take 1;
A21: dom p2 = dom p \/ dom (Start-At(il,SCMPDS)) by FUNCT_4:def 1;
A22: dom q2 = dom q \/ dom (il .--> (d1:=1)) by FUNCT_4:def 1;
A23: IC SCMPDS in dom (Start-At(il,SCMPDS)) by A10;
then IC SCMPDS in dom p2 by A21,XBOOLE_0:def 3;
then
A24: IC s2 = p2.IC SCMPDS by A17,GRFUNC_1:2
.= (Start-At(il,SCMPDS)).IC SCMPDS by A23,FUNCT_4:13
.= (Start-At(il,SCMPDS)).IC SCMPDS
.= il by FUNCOP_1:72;
il in dom (il .--> (d1:=1)) by TARSKI:def 1;
then
A25: il in dom ((il .--> (d1:=1)));
then il in dom q2 by A22,XBOOLE_0:def 3;
then
A26: S2.il = q2.il by A18,GRFUNC_1:2
.= ((il .--> (d1:=1))).il by A25,FUNCT_4:13
.= (il .--> (d1:=1)).il
.=(d1:=1) by FUNCOP_1:72;
A27: S2/.IC s2 = S2.IC s2 by PBOOLE:143;
A28: Comput(S2,s2,0+1).d1 = (Following(S2,Comput(S2,s2,0))).d1 by EXTPRO_1:3
.= (Following(S2,s2)).d1
.= 1 by A24,A26,A27,SCMPDS_2:45;
A29: dom p c= the carrier of SCMPDS by RELAT_1:def 18;
dom Comput(S1,s1,1) = the carrier of SCMPDS by PARTFUN1:def 2;
then
A30: dom (Comput(S1,s1,1)|dom p) = dom p by A29,RELAT_1:62;
A31: dom p1 = dom p \/ dom (Start-At(il,SCMPDS)) by FUNCT_4:def 1;
A32: dom q1 = dom q \/ dom (il .--> (d1:=0)) by FUNCT_4:def 1;
A33: IC SCMPDS in dom (Start-At(il,SCMPDS)) by A10;
then IC SCMPDS in dom p1 by A31,XBOOLE_0:def 3;
then
A34: IC s1 = p1.IC SCMPDS by A15,GRFUNC_1:2
.= (Start-At(il,SCMPDS)).IC SCMPDS by A33,FUNCT_4:13
.= (Start-At(il,SCMPDS)).IC SCMPDS
.= il by FUNCOP_1:72;
il in dom (il .--> (d1:=0)) by TARSKI:def 1;
then
A36: il in dom(il .--> (d1:=0));
then il in dom q1 by A32,XBOOLE_0:def 3;
then
A37: S1.il = q1.il by A16,GRFUNC_1:2
.= (il .--> (d1:=0)).il by A36,FUNCT_4:13
.= (il .--> (d1:=0)).il
.=(d1:=0) by FUNCOP_1:72;
A38: S1/.IC s1 = S1.IC s1 by PBOOLE:143;
A39: dom ( Comput(S2,s2,1)) = the carrier of SCMPDS
by PARTFUN1:def 2;
A40: dom ( Comput(S2,s2,1)|dom p) = dom p
by A29,A39,RELAT_1:62;
Comput(S1,s1,0+1).d1 =
(Following(S1,Comput(S1,s1,0))).d1
by EXTPRO_1:3
.= (Following(S1,s1)).d1
.= 0 by A34,A37,A38,SCMPDS_2:45;
then
(Comput(S1,s1,1)|dom p).d1 = 0
by A7,A30,A6,FUNCT_1:47;
hence thesis by A28,A7,A40,A6,FUNCT_1:47;
end;
hence contradiction;
end;
end;
theorem Th7:
for s1,s2 being State of SCMPDS,k1,k2,m be Integer st IC s1= IC
s2 & k1 <> k2 & m=IC s1 & m+k1 >= 0 & m+k2 >= 0 holds ICplusConst(s1,k1) <>
ICplusConst(s2,k2)
proof
let s1,s2 be State of SCMPDS,k1,k2,m be Integer;
assume that
A1: IC s1 = IC s2 and
A2: k1<>k2 and
A3: m=IC s1 and
A4: m+k1 >= 0 and
A5: m+k2 >= 0;
ex i being Element of NAT st i = IC s1 & ICplusConst(s1, k1)=|.i+k1.| by
SCMPDS_2:def 18;
then
A6: ICplusConst(s1,k1)=m+k1 by A3,A4,ABSVALUE:def 1;
assume
A7: ICplusConst(s1,k1) = ICplusConst(s2,k2);
ex j being Element of NAT st j = IC s2 & ICplusConst(s2, k2)=|.j+k2.| by
SCMPDS_2:def 18;
then ICplusConst(s2,k2)=m+k2 by A1,A3,A5,ABSVALUE:def 1;
hence contradiction by A2,A7,A6;
end;
theorem
for s1,s2 being State of SCMPDS,k1,k2 be Nat st IC s1
= IC s2 & k1 <> k2 holds ICplusConst(s1,k1) <> ICplusConst(s2,k2)
proof
let s1,s2 be State of SCMPDS,k1,k2 be Nat;
reconsider m=IC s1 as Element of NAT;
set mm=m+2;
A1: mm-2+k1>=0;
A2: mm-2+k2>=0;
assume IC s1 = IC s2 & k1<>k2;
hence thesis by A1,A2,Th7;
end;
theorem Th9:
for s being State of SCMPDS holds IC s + 1 = ICplusConst(s,1)
proof
let s be State of SCMPDS;
consider j being Element of NAT such that
A1: j = IC s and
A2: ICplusConst(s,1)=|.j+1.| by SCMPDS_2:def 18;
reconsider mj = IC s as Element of NAT;
A3: j*1 >= 0;
IC s + 1 = |.mj.|+1 by ABSVALUE:def 1
.= |.mj.|+|.1.| by ABSVALUE:def 1
.= |.mj+1.| by A1,A3,ABSVALUE:11;
hence thesis by A1,A2;
end;
registration
cluster SCMPDS -> CurIns-recognized;
coherence
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCMPDS,
s be State of SCMPDS such that
A1: p c= s;
let P be Instruction-Sequence of SCMPDS such that
A2: q c= P;
let i be Nat;
set Csi = Comput(P,s,i);
set loc = IC Csi;
set loc1 = loc+1;
assume not IC Comput(P,s,i) in dom q;
then
A3: not loc in dom q;
set I = the Int_position := 0;
set q1 = q +* (loc .--> I);
set q2 = q +* (loc .--> halt SCMPDS);
reconsider P1 = P +* (loc .--> I) as Instruction-Sequence of SCMPDS;
reconsider P2 = P +* (loc .--> halt SCMPDS)
as Instruction-Sequence of SCMPDS;
A5: loc in dom (loc .--> halt SCMPDS) by TARSKI:def 1;
A7: loc in dom (loc .--> I) by TARSKI:def 1;
A8: dom q misses dom (loc .--> halt SCMPDS) 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 SCMPDS).loc = halt SCMPDS by FUNCOP_1:72;
then
A12: P2.loc = halt SCMPDS by A5,FUNCT_4:13;
(loc .--> I).loc = I by FUNCOP_1:72;
then
A13: P1.loc = I by A7,FUNCT_4:13;
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 SCMPDS 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;
A20: Cs1k = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i)
.= Exec(I,Cs1i) by A19;
A21: IC Exec(I,Cs1i) = IC Cs1i + 1 by SCMPDS_2:45;
A22: IC SCMPDS in dom p by AMISTD_5:6;
A23: IC Csi = IC(Csi|dom p) by A22,FUNCT_1:49;
then IC Cs1i = loc by A16,A22,FUNCT_1:49;
then
A24: IC Cs1k = loc+1 by A20,A21
.= loc1;
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 be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCMPDS, s1, s2
being State of SCMPDS st p c= s1 & p c= s2 &
q c= P1 & q c= P2
for i being Nat,k1,k2 be Integer,a,b be Int_position st CurInstr(P1,
Comput(P1,s1,i)) = (a,k1) := (b,k2)
& a in dom p & DataLoc(Comput(P1,s1,i).a,k1) in dom p holds Comput
(P1,s1,i)
.DataLoc(Comput(P1,s1,i).b,k2) = Comput(P2,s2,i).
DataLoc(Comput(P2,s2,i).b,k2)
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCMPDS,
s1, s2 be State
of SCMPDS such that
A1: p c= s1 & p c= s2 and
A2: q c= P1 & q c= P2;
A3: p c= s1 & p c= s2 by A1;
let i be Nat,k1,k2 be Integer,a,b be Int_position;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
assume that
A4: I = (a,k1) := (b,k2) and
A5: a in dom p and
A6: DataLoc(Cs1i.a,k1) in dom p;
a in dom p implies (Cs1i|dom p).a = Cs1i.a &
(Cs2i|dom p).a = Cs2i.a
by FUNCT_1:49;
then
A7: Cs1i.a=Cs2i.a by A5,A2,A3,EXTPRO_1:def 10;
set Cs1i1 = Comput(P1,s1,i+1);
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then
A8: Cs1i1.DataLoc(Cs1i.a,k1) = Cs1i.DataLoc(Cs1i.b,k2)
by A4,SCMPDS_2:47;
set Cs2i1 = Comput(P2,s2,i+1);
A9: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
A10: DataLoc(Cs1i.a,k1) in dom p implies
(Cs1i1|dom p).DataLoc(Cs1i.a,k1) =
Cs1i1.DataLoc(Cs1i.a,k1) &
(Cs2i1|dom p).DataLoc(Cs1i.a,k1) = Cs2i1.DataLoc(
Cs1i.a,k1) by FUNCT_1:49;
I = CurInstr(P2,Comput(P2,s2,i))
by A1,A2,AMISTD_5:7;
then Cs2i1.DataLoc(Cs2i.a,k1) = Cs2i.DataLoc(Cs2i.b,k2)
by A9,A4,SCMPDS_2:47;
hence thesis by A10,A6,A7,A8,A2,A3,EXTPRO_1:def 10;
end;
theorem
for q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCMPDS, s1, s2
being State of SCMPDS st p c= s1 & p c= s2 &
q c= P1 & q c= P2
for i being Nat,k1,k2 be Integer,a,b be Int_position st CurInstr(P1,
Comput(P1,s1,i)) = AddTo(a,k1,b,k2)
& a in dom p & DataLoc(Comput(P1,s1,i).a,k1) in dom p holds Comput
(P1,s1,i)
.DataLoc(Comput(P1,s1,i).b,k2) = Comput(P2,s2,i).
DataLoc(Comput(P2,s2,i).
b,k2)
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCMPDS,
s1, s2 be State
of SCMPDS such that
A1: p c= s1 & p c= s2 and
A2: q c= P1 & q c= P2;
A3: p c= s1 & p c= s2 by A1;
let i be Nat,k1,k2 be Integer,a,b be Int_position;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
assume that
A4: I = AddTo(a,k1,b,k2) and
A5: a in dom p and
A6: DataLoc(Cs1i.a,k1) in dom p;
a in dom p implies
(Cs1i|dom p).a = Cs1i.a & (Cs2i|dom p).a = Cs2i.a by FUNCT_1:49;
then
A7: Cs1i.a=Cs2i.a by A5,A2,A3,EXTPRO_1:def 10;
set Cs2i1 = Comput(P2,s2,i+1);
set Cs1i1 = Comput(P1,s1,i+1);
set D11=Cs1i1.DataLoc(Cs1i.a,k1), D21=Cs2i1.DataLoc(Cs2i.a,k1), C11=Cs1i.
DataLoc(Cs1i.a,k1), C12=Cs1i.DataLoc(Cs1i.b,k2), C21=Cs2i.DataLoc(Cs2i.a,k1),
C22=Cs2i.DataLoc(Cs2i.b,k2);
A8: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
DataLoc(Cs1i.a,k1) in dom p implies
(Cs1i1|dom p).DataLoc(Cs1i.a,k1) =
Cs1i1.DataLoc(Cs1i.a,k1) &
(Cs2i1|dom p).DataLoc(Cs1i.a,k1) = Cs2i1.DataLoc(
Cs1i.a,k1) by FUNCT_1:49;
then
A9: D11 = D21 by A6,A7,A2,A3,EXTPRO_1:def 10;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then
A10: D11 = C11+ C12 by A4,SCMPDS_2:49;
DataLoc(Cs1i.a,k1) in dom p
implies (Cs1i|dom p).DataLoc(Cs1i.a,k1) =
Cs1i.DataLoc(Cs1i.a,k1) &
(Cs2i|dom p).DataLoc(Cs1i.a,k1) = Cs2i.DataLoc(Cs1i.a
,k1) by FUNCT_1:49;
then
A11: C11=C21 by A6,A7,A2,A3,EXTPRO_1:def 10;
I = CurInstr(P2,Comput(P2,s2,i))
by A1,A2,AMISTD_5:7;
then D21 = C21 + C22 by A8,A4,SCMPDS_2:49;
hence thesis by A11,A9,A10;
end;
theorem
for q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCMPDS, s1, s2
being State of SCMPDS st p c= s1 & p c= s2 &
q c= P1 & q c= P2
for i being Nat,k1,k2 be Integer,a,b be Int_position st CurInstr(P1,
Comput(P1,s1,i)) = SubFrom(a,k1,b,k2
) & a in dom p & DataLoc(Comput(P1,s1,i).a,k1) in dom p holds
Comput(P1,s1,
i).DataLoc(Comput(P1,s1,i).b,k2) = Comput(P2,s2,i).
DataLoc(Comput(P2,s2,i
).b,k2)
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCMPDS,
s1, s2 be State
of SCMPDS such that
A1: p c= s1 & p c= s2 and
A2: q c= P1 & q c= P2;
A3: p c= s1 & p c= s2 by A1;
let i be Nat,k1,k2 be Integer,a,b be Int_position;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
assume that
A4: I = SubFrom(a,k1,b,k2) and
A5: a in dom p and
A6: DataLoc(Cs1i.a,k1) in dom p;
a in dom p implies
(Cs1i|dom p).a = Cs1i.a & (Cs2i|dom p).a = Cs2i.a by FUNCT_1:49;
then
A7: Cs1i.a=Cs2i.a by A5,A2,A3,EXTPRO_1:def 10;
set Cs2i1 = Comput(P2,s2,i+1);
set Cs1i1 = Comput(P1,s1,i+1);
set D11=Cs1i1.DataLoc(Cs1i.a,k1), D21=Cs2i1.DataLoc(Cs2i.a,k1), C11=Cs1i.
DataLoc(Cs1i.a,k1), C12=Cs1i.DataLoc(Cs1i.b,k2), C21=Cs2i.DataLoc(Cs2i.a,k1),
C22=Cs2i.DataLoc(Cs2i.b,k2);
A8: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
DataLoc(Cs1i.a,k1) in dom p
implies (Cs1i1|dom p).DataLoc(Cs1i.a,k1) =
Cs1i1.DataLoc(Cs1i.a,k1) &
(Cs2i1|dom p).DataLoc(Cs1i.a,k1) = Cs2i1.DataLoc(
Cs1i.a,k1) by FUNCT_1:49;
then
A9: D11 = D21 by A6,A7,A2,A3,EXTPRO_1:def 10;
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then
A10: D11 = C11- C12 by A4,SCMPDS_2:50;
DataLoc(Cs1i.a,k1) in dom p
implies (Cs1i|dom p).DataLoc(Cs1i.a,k1) =
Cs1i.DataLoc(Cs1i.a,k1) &
(Cs2i|dom p).DataLoc(Cs1i.a,k1) = Cs2i.DataLoc(Cs1i.a
,k1) by FUNCT_1:49;
then
A11: C11=C21 by A6,A7,A2,A3,EXTPRO_1:def 10;
I = CurInstr(P2,Comput(P2,s2,i))
by A1,A2,AMISTD_5:7;
then D21 = C21 - C22 by A8,A4,SCMPDS_2:50;
hence thesis by A11,A9,A10;
end;
theorem
for q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCMPDS, s1, s2
being State of SCMPDS st p c= s1 & p c= s2 &
q c= P1 & q c= P2
for i being Nat,k1,k2 be
Integer,a,b be Int_position st CurInstr(P1,
Comput(P1,s1,i)) = MultBy(a,k1,b,k2)
& a in dom p & DataLoc(Comput(P1,s1,i).a,k1) in dom p holds Comput
(P1,s1,i)
.DataLoc(Comput(P1,s1,i).a,k1) * Comput(P1,s1,i).
DataLoc(Comput(P1,s1,i).
b,k2) = Comput(P2,s2,i).DataLoc(Comput(P2,s2,i).a,k1)
* Comput(P2,s2,i).
DataLoc(Comput(P2,s2,i).b,k2)
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCMPDS,
s1, s2 be State
of SCMPDS such that
A1: p c= s1 & p c= s2 and
A2: q c= P1 & q c= P2;
A3: p c= s1 & p c= s2 by A1;
let i be Nat,k1,k2 be Integer,a,b be Int_position;
set I = CurInstr(P1,Comput(P1,s1,i));
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
assume that
A4: I = MultBy (a,k1,b,k2) and
A5: a in dom p and
A6: DataLoc(Cs1i.a,k1) in dom p;
a in dom p implies
(Cs1i|dom p).a = Cs1i.a & (Cs2i|dom p).a = Cs2i.a by FUNCT_1:49;
then
A7: Cs1i.a=Cs2i.a by A5,A2,A3,EXTPRO_1:def 10;
set Cs2i1 = Comput(P2,s2,i+1);
set Cs1i1 = Comput(P1,s1,i+1);
set D11=Cs1i1.DataLoc(Cs1i.a,k1), D21=Cs2i1.DataLoc(Cs2i.a,k1);
Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
then
A8: D11 = Cs1i.DataLoc(Cs1i.a,k1) * Cs1i.DataLoc(Cs1i.b,k2) by A4,SCMPDS_2:51;
A9: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
A10: DataLoc(Cs1i.a,k1) in dom p
implies (Cs1i1|dom p).DataLoc(Cs1i.a,k1) =
Cs1i1.DataLoc(Cs1i.a,k1) &
(Cs2i1|dom p).DataLoc(Cs1i.a,k1) = Cs2i1.DataLoc(
Cs1i.a,k1) by FUNCT_1:49;
I = CurInstr(P2,Comput(P2,s2,i))
by A1,A2,AMISTD_5:7;
then D21 = Cs2i.DataLoc(Cs2i.a,k1) * Cs2i.DataLoc(Cs2i.b,k2) by A9,A4,
SCMPDS_2:51;
hence thesis by A10,A6,A7,A8,A2,A3,EXTPRO_1:def 10;
end;
theorem
for q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCMPDS, s1, s2
being State of SCMPDS st p c= s1 & p c= s2 &
q c= P1 & q c= P2
for i,m being Nat,a being
Int_position,k1,k2 be Integer st CurInstr(P1,
Comput(P1,s1,i)) = (a,k1)<>0_goto
k2 & m= IC Comput(P1,s1,i) & m+k2 >= 0 & k2 <> 1 holds (Comput(
P1,s1,i).
DataLoc(Comput(P1,s1,i).a,k1) = 0 iff Comput(P2,s2,i)
.DataLoc(Comput(P2,s2,i).a,k1) = 0 )
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCMPDS,
s1, s2 be State
of SCMPDS such that
A1: p c= s1 & p c= s2 and
A2: q c= P1 & q c= P2;
let i,m be Nat,a be Int_position,k1,k2 be Integer;
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: IC Cs1i = IC Cs2i & (Cs1i1|dom p) = (Cs2i1|dom p)
by A1,A2,AMISTD_5:7,EXTPRO_1:def 10;
set I = CurInstr(P1,Comput(P1,s1,i));
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
A5: m+1>=0;
IC SCMPDS in dom p by AMISTD_5:6;
then IC SCMPDS in dom p;
then
A6: (Cs1i1|dom p).IC SCMPDS = Cs1i1.IC SCMPDS &
(Cs2i1|dom p).IC SCMPDS =
Cs2i1. IC SCMPDS by FUNCT_1:49;
A7: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A8: I = (a,k1)<>0_goto k2 and
A9: m= IC Cs1i & m+k2 >= 0 & k2 <> 1;
A10: I = CurInstr(P2,Comput(P2,s2,i))
by A1,A2,AMISTD_5:7;
A11: now
assume that
A12: Comput(P2,s2,i).DataLoc(Cs2i.a,k1) = 0 and
A13: Comput(P1,s1,i).DataLoc(Cs1i.a,k1) <> 0;
A14: Cs1i1.IC SCMPDS = ICplusConst(Cs1i,k2) by A4,A8,A13,SCMPDS_2:55;
Cs2i1.IC SCMPDS = IC Cs2i + 1 by A10,A7,A8,A12,SCMPDS_2:55
.=ICplusConst(Cs2i,1) by Th9;
hence contradiction by A6,A3,A9,A5,A14,Th7;
end;
now
assume that
A15: Comput(P1,s1,i).DataLoc(Cs1i.a,k1) = 0 and
A16: Comput(P2,s2,i).DataLoc(Cs2i.a,k1) <> 0;
A17: Cs2i1.IC SCMPDS = ICplusConst(Cs2i,k2) by A10,A7,A8,A16,SCMPDS_2:55;
Cs1i1.IC SCMPDS = IC Cs1i + 1 by A4,A8,A15,SCMPDS_2:55
.=ICplusConst(Cs1i,1) by Th9;
hence contradiction by A6,A3,A9,A5,A17,Th7;
end;
hence thesis by A11;
end;
theorem
for q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCMPDS, s1, s2
being State of SCMPDS st p c= s1 & p c= s2 &
q c= P1 & q c= P2
for i,m being Nat,a being
Int_position,k1,k2 be Integer st CurInstr(P1,
Comput(P1,s1,i)) = (a,k1)<=0_goto
k2 & m= IC Comput(P1,s1,i) & m+k2 >= 0 & k2 <> 1 holds (Comput(
P1,s1,i).
DataLoc(Comput(P1,s1,i).a,k1) > 0 iff Comput(P2,s2,i)
.DataLoc(Comput(P2,
s2,i).a,k1) > 0 )
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCMPDS,
s1, s2 be State
of SCMPDS such that
A1: p c= s1 & p c= s2 and
A2: q c= P1 & q c= P2;
let i,m be Nat,a be Int_position,k1,k2 be Integer;
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: IC Cs1i = IC Cs2i & (Cs1i1|dom p) = (Cs2i1|dom p)
by A1,A2,AMISTD_5:7,EXTPRO_1:def 10;
set I = CurInstr(P1,Comput(P1,s1,i));
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
A5: m+1>=0;
IC SCMPDS in dom p by AMISTD_5:6;
then IC SCMPDS in dom p;
then
A6: (Cs1i1|dom p).IC SCMPDS =
Cs1i1.IC SCMPDS & (Cs2i1|dom p).IC SCMPDS =
Cs2i1. IC SCMPDS by FUNCT_1:49;
A7: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A8: I = (a,k1)<=0_goto k2 and
A9: m= IC Cs1i & m+k2 >= 0 & k2 <> 1;
A10: I = CurInstr(P2,Comput(P2,s2,i))
by A1,A2,AMISTD_5:7;
A11: now
assume that
A12: Comput(P2,s2,i).DataLoc(Cs2i.a,k1) > 0 and
A13: Comput(P1,s1,i).DataLoc(Cs1i.a,k1) <= 0;
A14: Cs1i1.IC SCMPDS = ICplusConst(Cs1i,k2) by A4,A8,A13,SCMPDS_2:56;
Cs2i1.IC SCMPDS = IC Cs2i + 1 by A10,A7,A8,A12,SCMPDS_2:56
.=ICplusConst(Cs2i,1) by Th9;
hence contradiction by A6,A3,A9,A5,A14,Th7;
end;
now
assume that
A15: Comput(P1,s1,i).DataLoc(Cs1i.a,k1) > 0 and
A16: Comput(P2,s2,i).DataLoc(Cs2i.a,k1) <= 0;
A17: Cs2i1.IC SCMPDS = ICplusConst(Cs2i,k2) by A10,A7,A8,A16,SCMPDS_2:56;
Cs1i1.IC SCMPDS = IC Cs1i + 1 by A4,A8,A15,SCMPDS_2:56
.=ICplusConst(Cs1i,1) by Th9;
hence contradiction by A6,A3,A9,A5,A17,Th7;
end;
hence thesis by A11;
end;
theorem
for q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function
for p being q-autonomic non empty FinPartState of SCMPDS, s1, s2
being State of SCMPDS st p c= s1 & p c= s2 &
q c= P1 & q c= P2
for i,m being Nat,a being
Int_position,k1,k2 be Integer st CurInstr(P1,
Comput(P1,s1,i)) = (a,k1)>=0_goto
k2 & m= IC Comput(P1,s1,i) & m+k2 >= 0 & k2 <> 1 holds (Comput(
P1,s1,i).
DataLoc(Comput(P1,s1,i).a,k1) < 0 iff Comput(P2,s2,i)
.DataLoc(Comput(P2,
s2,i).a,k1) < 0 )
proof
let q be non halt-free finite
(the InstructionsF of SCMPDS)-valued NAT-defined Function;
let p be q-autonomic non empty FinPartState of SCMPDS,
s1, s2 be State
of SCMPDS such that
A1: p c= s1 & p c= s2 and
A2: q c= P1 & q c= P2;
let i,m be Nat,a be Int_position,k1,k2 be Integer;
set Cs1i = Comput(P1,s1,i);
set Cs2i = Comput(P2,s2,i);
set Cs1i1 = Comput(P1,s1,i+1);
set Cs2i1 = Comput(P2,s2,i+1);
A3: IC Cs1i = IC Cs2i & (Cs1i1|dom p) = (Cs2i1|dom p)
by A1,A2,AMISTD_5:7,EXTPRO_1:def 10;
set I = CurInstr(P1,Comput(P1,s1,i));
A4: Cs1i1 = Following(P1,Cs1i) by EXTPRO_1:3
.= Exec (CurInstr(P1,Cs1i), Cs1i);
A5: m+1>=0;
IC SCMPDS in dom p by AMISTD_5:6;
then IC SCMPDS in dom p;
then
A6: (Cs1i1|dom p).IC SCMPDS = Cs1i1.IC SCMPDS &
(Cs2i1|dom p).IC SCMPDS =
Cs2i1. IC SCMPDS by FUNCT_1:49;
A7: Cs2i1 = Following(P2,Cs2i) by EXTPRO_1:3
.= Exec (CurInstr(P2,Cs2i), Cs2i);
assume that
A8: I = (a,k1)>=0_goto k2 and
A9: m= IC Cs1i & m+k2 >= 0 & k2 <> 1;
A10: I = CurInstr(P2,Comput(P2,s2,i))
by A1,A2,AMISTD_5:7;
A11: now
assume that
A12: Comput(P2,s2,i).DataLoc(Cs2i.a,k1) < 0 and
A13: Comput(P1,s1,i).DataLoc(Cs1i.a,k1) >= 0;
A14: Cs1i1.IC SCMPDS = ICplusConst(Cs1i,k2) by A4,A8,A13,SCMPDS_2:57;
Cs2i1.IC SCMPDS = IC Cs2i + 1 by A10,A7,A8,A12,SCMPDS_2:57
.=ICplusConst(Cs2i,1) by Th9;
hence contradiction by A6,A3,A9,A5,A14,Th7;
end;
now
assume that
A15: Comput(P1,s1,i).DataLoc(Cs1i.a,k1) < 0 and
A16: Comput(P2,s2,i).DataLoc(Cs2i.a,k1) >= 0;
A17: Cs2i1.IC SCMPDS = ICplusConst(Cs2i,k2) by A10,A7,A8,A16,SCMPDS_2:57;
Cs1i1.IC SCMPDS = IC Cs1i + 1 by A4,A8,A15,SCMPDS_2:57
.=ICplusConst(Cs1i,1) by Th9;
hence contradiction by A6,A3,A9,A5,A17,Th7;
end;
hence thesis by A11;
end;