:: The Construction and shiftability of Program Blocks for SCMPDS
:: 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, AMI_1, SCMPDS_2, SCMFSA_7, CARD_1, FUNCOP_1,
RELAT_1, FUNCT_1, NAT_1, ARYTM_3, XBOOLE_0, TARSKI, VALUED_1, EXTPRO_1,
FSM_1, INT_1, FUNCT_4, GRAPHSP, AMI_3, AMI_2, STRUCT_0, COMPLEX1,
XXREAL_0, ARYTM_1, TURING_1, AMISTD_2, SCMFSA6B, MSUALG_1, CIRCUIT2,
SCMPDS_4, PARTFUN1, ORDINAL4, FINSET_1, COMPOS_1, GOBRD13, MEMSTR_0;
notations TARSKI, XBOOLE_0, ENUMSET1, XTUPLE_0, SUBSET_1, CARD_1, FINSET_1,
ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, AFINSQ_1,
VALUED_1, FUNCT_4, FUNCT_7, INT_1, NAT_1, INT_2, XXREAL_0, STRUCT_0,
MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, SCMPDS_2;
constructors INT_2, SCMPDS_1, SCMPDS_3, DOMAIN_1, RELSET_1, PRE_POLY, AMI_3,
FUNCT_7;
registrations FUNCT_1, ORDINAL1, XREAL_0, NAT_1, INT_1, SCMPDS_2, FINSET_1,
FUNCT_4, PRE_POLY, AFINSQ_1, COMPOS_1, ORDINAL5, EXTPRO_1, FUNCT_7,
MEMSTR_0, AMI_3, COMPOS_0, CARD_3, STRUCT_0, RELSET_1, XTUPLE_0;
requirements REAL, NUMERALS, SUBSET, BOOLE, ARITHM;
definitions EXTPRO_1;
equalities TARSKI, COMPOS_1, EXTPRO_1, XBOOLE_0, SCMPDS_2, FUNCOP_1, AFINSQ_1,
MEMSTR_0;
theorems NAT_1, TARSKI, FUNCT_4, FUNCT_1, INT_1, RELAT_1, SCMPDS_2, AMI_2,
FUNCT_2, FUNCT_7, SCMPDS_3, ENUMSET1, ABSVALUE, GRFUNC_1, XBOOLE_0,
XREAL_1, FUNCOP_1, VALUED_1, AFINSQ_1, PARTFUN1, COMPOS_1, EXTPRO_1,
PBOOLE, STRUCT_0, MEMSTR_0, XTUPLE_0;
schemes NAT_1, CLASSES1;
begin :: Definition of a program block and its basic properties
reserve l, m, n for Nat,
i,j,k for Instruction of SCMPDS,
I,J,K for Program of SCMPDS,
p,q,r for PartState of SCMPDS;
reserve a,b,c for Int_position,
s,s1,s2 for State of SCMPDS,
k1,k2 for Integer;
theorem Th1:
InsCode i in {0,1,4,5,6,14} or Exec(i,s).IC SCMPDS = IC s + 1
proof
assume
A1: not InsCode i in {0,1,4,5,6,14};
A2: InsCode i = 0 or ... or InsCode i = 14 by SCMPDS_2:6;
per cases by A2,A1,ENUMSET1:def 4;
suppose
InsCode i = 2;
then ex a,k1 st i = a:=k1 by SCMPDS_2:28;
hence thesis by SCMPDS_2:45;
end;
suppose
InsCode i = 3;
then ex a,k1 st i = saveIC(a,k1) by SCMPDS_2:29;
hence thesis by SCMPDS_2:59;
end;
suppose
InsCode i = 7;
then ex a,k1,k2 st i = (a,k1) := k2 by SCMPDS_2:33;
hence thesis by SCMPDS_2:46;
end;
suppose
InsCode i = 8;
then ex a,k1,k2 st i = AddTo(a,k1,k2) by SCMPDS_2:34;
hence thesis by SCMPDS_2:48;
end;
suppose
InsCode i = 9;
then ex a,b,k1,k2 st i = AddTo(a,k1,b,k2) by SCMPDS_2:35;
hence thesis by SCMPDS_2:49;
end;
suppose
InsCode i = 10;
then ex a,b,k1,k2 st i = SubFrom(a,k1,b,k2) by SCMPDS_2:36;
hence thesis by SCMPDS_2:50;
end;
suppose
InsCode i = 11;
then ex a,b,k1,k2 st i = MultBy(a,k1,b,k2) by SCMPDS_2:37;
hence thesis by SCMPDS_2:51;
end;
suppose
InsCode i = 12;
then ex a,b,k1,k2 st i = Divide(a,k1,b,k2) by SCMPDS_2:38;
hence thesis by SCMPDS_2:52;
end;
suppose
InsCode i = 13;
then ex a,b,k1,k2 st i = (a,k1):=(b,k2) by SCMPDS_2:39;
hence thesis by SCMPDS_2:47;
end;
end;
theorem
for s1,s2 being State of SCMPDS st IC s1 = IC s2 & for a being
Int_position holds s1.a = s2.a holds s1 = s2
proof
let s1,s2 be State of SCMPDS such that
A1: IC s1 = IC s2 and
A2: for a being Int_position holds s1.a = s2.a;
A3: (the carrier of SCMPDS) = {IC SCMPDS } \/ SCM-Data-Loc
by SCMPDS_2:84,STRUCT_0:4
.= {IC SCMPDS } \/ SCM-Data-Loc;
A4: dom(s2|(dom s2)) = dom s2 /\ (dom s2) by RELAT_1:61
.= dom s2
.= {IC SCMPDS } \/ SCM-Data-Loc by A3,PARTFUN1:def 2;
A5: dom(s1|(dom s1)) = dom s1 /\ (dom s1) by RELAT_1:61
.= dom s1
.= {IC SCMPDS } \/ SCM-Data-Loc by A3,PARTFUN1:def 2;
A6: s1|(dom s1) = s1 & s2|(dom s2) = s2 by RELAT_1:69;
now
let x be object;
assume
A7: x in {IC SCMPDS } \/ SCM-Data-Loc;
per cases by A7,XBOOLE_0:def 3;
suppose
x in {IC SCMPDS};
then
A8: x = IC SCMPDS by TARSKI:def 1;
hence (s1|(dom s1)).x = IC s1 by A5,A7,FUNCT_1:47
.= (s2|(dom s2)).x by A1,A4,A7,A8,FUNCT_1:47;
end;
suppose
x in SCM-Data-Loc;
then
A9: x is Int_position by AMI_2:def 16;
thus (s1|(dom s1)).x = s1.x by A5,A7,FUNCT_1:47
.= s2.x by A2,A9
.= (s2|(dom s2)).x by A4,A7,FUNCT_1:47;
end;
end;
hence s1 = s2 by A6,A5,A4,FUNCT_1:2;
end;
theorem Th3:
for k1,k2 be Nat st k1 <> k2 holds DataLoc(k1,0) <>
DataLoc(k2,0)
proof
let k1,k2 be Nat;
assume
A1: k1<>k2;
assume
DataLoc(k1,0) = DataLoc(k2,0);
then |.k1+0.| =|.k2+0.| by XTUPLE_0:1;
then k1=|.k2.| by ABSVALUE:def 1;
hence contradiction by A1,ABSVALUE:def 1;
end;
theorem Th4:
for dl being Int_position ex i being Nat st dl =
DataLoc(i,0)
proof
let dl be Int_position;
consider i being Nat such that
A1: dl = [1,i] by AMI_2:23,def 16;
take i;
thus thesis by A1,ABSVALUE:def 1;
end;
scheme
SCMPDSEx{ G(set) -> Integer, I() -> Element of NAT }:
ex S being State of SCMPDS st IC S = I() &
for i being Nat holds S.DataLoc(i,0) = G(i)
proof
set S1={IC SCMPDS }, S2=SCM-Data-Loc, S3=NAT;
defpred P[object,object] means ex m st $1 = IC SCMPDS & $2 = I()
or $1 = DataLoc(m,0) & $2 = G(m);
A1: for e being object st e in the carrier of SCMPDS
ex u being object st P[e,u]
proof
let e be object;
assume
e in the carrier of SCMPDS;
then
A2: e in S1 \/ S2 by SCMPDS_2:84,STRUCT_0:4;
now
per cases by A2,XBOOLE_0:def 3;
case
e in S1;
hence e = IC SCMPDS by TARSKI:def 1;
end;
case
e in S2;
then e is Int_position by AMI_2:def 16;
hence ex m st e = DataLoc(m,0) by Th4;
end;
end;
then consider m such that
A3: e = IC SCMPDS or e = DataLoc(m,0);
per cases by A3;
suppose
A4: e = IC SCMPDS;
take u = I();
thus thesis by A4;
end;
suppose
A5: e = DataLoc(m,0);
take u = G(m);
thus thesis by A5;
end;
end;
consider f being Function such that
A6: dom f = the carrier of SCMPDS and
A7: for e being object st e in the carrier of SCMPDS holds P[e,f.e] from
CLASSES1:sch 1(A1);
A8: dom the Object-Kind of SCMPDS = the carrier of SCMPDS by FUNCT_2:def 1;
now
let x be object;
assume
A9: x in dom the Object-Kind of SCMPDS;
then
A10: x in S1 \/ S2 by A8,SCMPDS_2:84,STRUCT_0:4;
consider m such that
A11: x = IC SCMPDS & f.x = I() or x = DataLoc(m,0) & f.x = G(m) by A7,A8,A9;
per cases by A10,XBOOLE_0:def 3;
suppose
x in S2;
then x is Int_position by AMI_2:def 16;
then (the_Values_of SCMPDS).x = Values DataLoc(m,0) by A11,SCMPDS_2:43
.= INT by SCMPDS_2:5;
hence f.x in (the_Values_of SCMPDS).x by A11,INT_1:def 2;
end;
suppose
A12: x in S1;
(the_Values_of SCMPDS).x = Values IC SCMPDS by TARSKI:def 1,A12
.= NAT by MEMSTR_0:def 6;
hence f.x in (the_Values_of SCMPDS).x
by A11,A12,SCMPDS_2:2,TARSKI:def 1;
end;
end;
then reconsider f as State of SCMPDS by A6,A8,FUNCT_1:def 14,PARTFUN1:def 2
,RELAT_1:def 18;
consider m such that
A13: IC SCMPDS = IC SCMPDS & f.IC SCMPDS = I() or
IC SCMPDS = DataLoc(m,0) & f.IC SCMPDS = G(m) by A7;
take f;
thus IC f = I() by A13,SCMPDS_2:43;
let i be Nat;
ex m st ( DataLoc(i,0) = IC SCMPDS & f.DataLoc(i,0) = I() or
DataLoc(i,0) = DataLoc(m,0) & f.DataLoc
(i,0) = G(m)) by A7;
hence thesis by Th3,SCMPDS_2:43;
end;
theorem
for s being State of SCMPDS holds dom s = {IC SCMPDS} \/ SCM-Data-Loc
proof
let s be State of SCMPDS;
dom s = the carrier of SCMPDS by PARTFUN1:def 2;
hence thesis by SCMPDS_2:84,STRUCT_0:4;
end;
theorem
for s being State of SCMPDS, x being set st x in dom s holds x is
Int_position or x = IC SCMPDS
proof
set S1={IC SCMPDS}, S2=SCM-Data-Loc, S3=NAT;
let s be State of SCMPDS;
let x be set;
assume
A1: x in dom s;
dom s = the carrier of SCMPDS by PARTFUN1:def 2;
then x in S1 \/ S2 by A1,SCMPDS_2:84,STRUCT_0:4;
then x in S1 or x in S2 by XBOOLE_0:def 3;
hence thesis by AMI_2:def 16,TARSKI:def 1;
end;
::$CT
theorem Th7:
for s1,s2 being State of SCMPDS holds (for a being Int_position
holds s1.a = s2.a) iff DataPart s1 = DataPart s2
proof
set T1={IC SCMPDS}, T2=SCM-Data-Loc, T3=NAT;
let s1,s2 be State of SCMPDS;
A1: now
assume
A2: for a being Int_position holds s1.a = s2.a;
hereby
let x be set;
assume
x in SCM-Data-Loc;
then x is Int_position by AMI_2:def 16;
hence s1.x=s2.x by A2;
end;
end;
A3: (for x be set st x in SCM-Data-Loc holds s1.x = s2.x) implies
for a being Int_position holds s1.a=s2.a by AMI_2:def 16;
A4: dom s2 = the carrier of SCMPDS by PARTFUN1:def 2;
dom s1 = the carrier of SCMPDS by PARTFUN1:def 2;
hence thesis by A4,A1,A3,FUNCT_1:95,SCMPDS_2:84;
end;
reserve x for set;
begin :: Combining two consecutive blocks into one program block
notation
let I,J be Program of SCMPDS;
synonym I ';'↑ J for I ^ J;
end;
definition
let I,J be Program of SCMPDS;
redefine func I ';' J -> Program of SCMPDS equals :: redefines ';' (SCMPDS_4, synonym) → ^ (AFINSQ_1, redefinition) → ^ (ORDINAL4, definition)
I +* Shift(J, card I);
compatibility by AFINSQ_1:77;
coherence;
end;
begin :: Combining a block and a instruction into one program block
definition
let i, J;
func i ';' J -> Program of SCMPDS equals
Load i ';' J;
correctness;
end;
definition
let I, j;
func I ';' j -> Program of SCMPDS equals
I ';' Load j;
correctness;
end;
definition
let i,j;
func i ';' j -> Program of SCMPDS equals
Load i ';' Load j;
correctness;
end;
theorem
i ';' j = Load i ';' j;
theorem
i ';' j = i ';' Load j;
theorem
I ';' J ';' k = I ';' (J ';' k) by AFINSQ_1:27;
theorem
I ';' j ';' K = I ';' (j ';' K) by AFINSQ_1:27;
theorem
I ';' j ';' k = I ';' (j ';' k) by AFINSQ_1:27;
theorem
i ';' J ';' K = i ';' (J ';' K) by AFINSQ_1:27;
theorem
i ';' J ';' k = i ';' (J ';' k) by AFINSQ_1:27;
theorem
i ';' j ';' K = i ';' (j ';' K) by AFINSQ_1:27;
theorem
i ';' j ';' k = i ';' (j ';' k) by AFINSQ_1:27;
reserve l,l1,loc for Nat;
theorem
not a in dom Start-At(l,SCMPDS)
proof
A1: dom Start-At(l,SCMPDS) = {IC SCMPDS} by FUNCOP_1:13;
assume
a in dom Start-At(l,SCMPDS);
then a = IC SCMPDS by A1,TARSKI:def 1;
hence contradiction by SCMPDS_2:43;
end;
definition
let s be State of SCMPDS, li be Int_position, k be Integer;
redefine func s+*(li,k) -> PartState of SCMPDS; :: redefines +* (FUNCT_7, definition)
coherence
proof
A1: dom s = the carrier of SCMPDS by PARTFUN1:def 2;
now
let x be object;
assume x in dom(s+*(li,k));
then
A2: x in dom s by A1,PARTFUN1:def 2;
per cases;
suppose
A3: x = li;
then
A4: (the_Values_of SCMPDS).x = Values li
.= INT by SCMPDS_2:5;
(s+*(li,k)).x = k by A1,A3,FUNCT_7:31;
hence (s+*(li,k)).x in (the_Values_of SCMPDS).x by A4,INT_1:def 2;
end;
suppose
x <> li;
then (s+*(li,k)).x = s.x by FUNCT_7:32;
hence (s+*(li,k)).x in (the_Values_of SCMPDS).x
by A2,FUNCT_1:def 14;
end;
end;
hence thesis by FUNCT_1:def 14;
end;
end;
begin :: The notions of paraclosed,parahalting and their basic properties
definition
let I be Program of SCMPDS, s be State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
func IExec(I,P,s) -> State of SCMPDS equals
Result(P+*stop I,s);
coherence;
end;
definition
let I be Program of SCMPDS;
attr I is paraclosed means
:Def6:
for s being 0-started State of SCMPDS, n being Nat,
P being Instruction-Sequence of SCMPDS
st stop I c= P
holds IC Comput(P,s,n) in dom stop(I);
attr I is parahalting means
for s being 0-started State of SCMPDS,
P being Instruction-Sequence of SCMPDS
st stop I c= P
holds P halts_on s;
end;
Lm1: Load halt SCMPDS is parahalting
proof
let s be 0-started State of SCMPDS,
P being Instruction-Sequence of SCMPDS;
set m = Load halt SCMPDS, m0= stop (m);
assume
A1: m0 c= P;
A2: IC s = 0 by MEMSTR_0:def 11;
take 0;
IC Comput(P,s,0) in NAT;
hence IC Comput(P,s,0) in dom P by PARTFUN1:def 2;
A3: m. 0 = halt SCMPDS;
dom m={ 0} by FUNCOP_1:13;
then
A4: 0 in dom m by TARSKI:def 1;
then
A5: 0 in dom m0 by FUNCT_4:12;
A6: P/.IC s = P.IC s by PBOOLE:143;
CurInstr(P,Comput(P,s,0))
= m0. 0 by A1,A5,A2,A6,GRFUNC_1:2
.= halt SCMPDS by A3,A4,AFINSQ_1:def 3;
hence thesis;
end;
registration
cluster parahalting for Program of SCMPDS;
existence by Lm1;
end;
::$CT
theorem Th18:
for P,Q being Instruction-Sequence of SCMPDS
st Q = P +*((IC s,IC s + 1) --> (goto 1, goto -1))
holds
not Q halts_on s
proof
let P,Q be Instruction-Sequence of SCMPDS such that
A1: Q = P +*((IC s,IC s + 1) --> (goto 1, goto -1));
set m=(IC s,IC s + 1) --> (goto 1, goto -1);
A2: m.(IC s + 1)=goto -1 by FUNCT_4:63;
IC s<>IC s + 1;
then
A3: m.(IC s) = goto 1 by FUNCT_4:63;
defpred X[Nat] means
IC(Comput(Q,s,$1)) = IC s or IC(Comput(Q,s,$1)) = IC s + 1;
A4: dom m = {IC s,IC s + 1} by FUNCT_4:62;
then
A5: IC s + 1 in dom m by TARSKI:def 2;
A6: IC s in dom m by A4,TARSKI:def 2;
now
let n;
set Cn=Comput(Q,s,n);
assume
A7: IC Cn = IC s or IC Cn = IC s + 1;
per cases by A7;
case
A8: IC Cn = IC s;
then
A9: CurInstr(Q,Cn) = Q.IC s by PBOOLE:143
.= goto 1 by A6,A3,A1,FUNCT_4:13;
thus IC (Comput(Q,s,n+1)) = IC Following(Q,Cn)
by EXTPRO_1:3
.= ICplusConst(Cn,1) by A9,SCMPDS_2:54
.= IC s + 1 by A8,SCMPDS_3:10;
end;
case
A10: IC Cn = IC s + 1;
reconsider i = IC s as Element of NAT;
A11: ex j be Element of NAT st j = IC Cn & ICplusConst(Cn,-1) =|.j+(-1)
.| by SCMPDS_2:def 18;
A12: CurInstr(Q,Comput(Q,s,n))
= Q.(IC s + 1) by A10,PBOOLE:143
.= goto -1 by A5,A2,A1,FUNCT_4:13;
thus IC(Comput(Q,s,n+1)) = IC Following(Q,Cn)
by EXTPRO_1:3
.=|.i+4 + -4 .| by A10,A12,A11,SCMPDS_2:54
.=IC s by ABSVALUE:def 1;
end;
end;
then
A13: for n st X[n] holds X[n+1];
let nn be Nat;
reconsider n=nn as Nat;
assume IC Comput(Q,s,nn) in dom Q;
A14: X[0];
A15: for n holds X[n] from NAT_1:sch 2(A14,A13);
per cases by A15;
suppose
IC(Comput(Q,s,n)) = IC s;
then CurInstr(Q,Comput(Q,s,n))
= Q.IC s by PBOOLE:143
.= goto 1 by A6,A3,A1,FUNCT_4:13;
hence thesis by SCMPDS_2:73;
end;
suppose
IC(Comput(Q,s,n)) = IC s + 1;
then CurInstr(Q,Comput(Q,s,n))
= Q.(IC s + 1) by PBOOLE:143
.= goto -1 by A5,A2,A1,FUNCT_4:13;
hence thesis by SCMPDS_2:73;
end;
end;
theorem Th19:
for P1,P2 being Instruction-Sequence of SCMPDS
st s1 = s2 & I c= P1 & I c= P2 & (for m st m < n
holds IC (Comput(P2,s2,m)) in dom I)
for m st m <= n
holds
Comput(P1,s1,m) = Comput(P2,s2,m)
proof
let P1,P2 be Instruction-Sequence of SCMPDS;
assume that
A1: s1 = s2 and
A2: I c= P1 and
A3: I c= P2 and
A4: for m st m < n holds IC(Comput(P2,s2,m)) in dom I;
defpred X[Nat] means $1 <= n implies
Comput(P1,s1,$1) = Comput(P2,s2,$1);
A5: for m st X[m] holds X[m+1]
proof
let m such that
A6: m <= n implies
Comput(P1,s1,m) = Comput(P2,s2,m);
A7: Comput(P2,s2,m+1) = Following(P2,Comput(P2,s2,m)) by EXTPRO_1:3
.= Exec(CurInstr(P2,Comput(P2,s2,m)),Comput(P2,s2,m));
A8: Comput(P1,s1,m+1) = Following(P1,Comput(P1,s1,m)) by EXTPRO_1:3
.= Exec(CurInstr(P1,Comput(P1,s1,m)),Comput(P1,s1,m));
assume
A9: m+1 <= n;
A10: IC(Comput(P2,s2,m)) in dom I by A4,A9,NAT_1:13;
CurInstr(P1,Comput(P1,s1,m))
= P1.IC(Comput(P1,s1,m)) by PBOOLE:143
.= I.IC(Comput(P1,s1,m)) by A2,A10,A9,A6,GRFUNC_1:2,NAT_1:13
.= P2.IC(Comput(P2,s2,m)) by A3,A10,A9,A6,GRFUNC_1:2,NAT_1:13
.= CurInstr(P2,Comput(P2,s2,m)) by PBOOLE:143;
hence thesis by A6,A8,A7,A9,NAT_1:13;
end;
Comput(P1,s1,0) = Comput(P2,s2,0) by A1;
then
A11: X[0];
thus for m holds X[m] from NAT_1:sch 2(A11,A5);
end;
reserve l1,l2 for Nat,
i1,i2 for Instruction of SCMPDS;
registration
cluster parahalting -> paraclosed for Program of SCMPDS;
coherence
proof
let I be Program of SCMPDS;
assume
A1: I is parahalting;
let s be 0-started State of SCMPDS, n be Nat,
P being Instruction-Sequence of SCMPDS;
defpred X[Nat] means not IC Comput(P,s,$1) in dom stop(I);
assume
A2: stop(I) c= P;
assume
not IC Comput(P,s,n) in dom stop(I);
then
A3: ex n be Nat st X[n];
consider n be Nat such that
A4: X[n] and
A5: for m be Nat st X[m] holds n <= m from NAT_1:sch 5(A3);
reconsider n as Nat;
A6: for m st m < n holds IC(Comput(P,s,m)) in dom stop I by A5;
set s2 = Comput(P,s,n),
Ig = ((IC s2,IC s2 + 1) --> (goto 1,goto -1));
reconsider P0 = P +* Ig as Instruction-Sequence of SCMPDS;
reconsider P3 = P +* (IC s2,goto 1) as Instruction-Sequence of SCMPDS;
reconsider P2 = P3 +* (IC s + 12,goto -1) as
Instruction-Sequence of SCMPDS;
reconsider P4 = P3 +* (IC s2 + 1,goto -1)
as Instruction-Sequence of SCMPDS;
A7: P0 = P4 by FUNCT_7:139;
stop I c= P3 by A2,A4,FUNCT_7:89;
then
A8: stop I c= P0 by A7,A4,AFINSQ_1:73,FUNCT_7:89;
then
A9: Comput(P0,s,n) = s2 by A2,A6,Th19;
not P0 halts_on s2 by Th18;
hence contradiction by A1,A8,A9,EXTPRO_1:22;
end;
end;
begin :: Shiftability of program blocks and instructions
definition
let i be Instruction of SCMPDS;
let n be Nat;
pred i valid_at n means
(InsCode i= 14 implies ex k1 st i = goto k1 &
n+k1 >= 0) & (InsCode i= 4 implies ex a,k1,k2 st i = (a,k1)<>0_goto k2 & n+k2
>= 0 ) & (InsCode i= 5 implies ex a,k1,k2 st i = (a,k1)<=0_goto k2 & n+k2 >= 0
) & (InsCode i= 6 implies ex a,k1,k2 st i = (a,k1)>=0_goto k2 & n+k2 >= 0);
end;
reserve l for Nat;
definition
let IT be finite (the InstructionsF of SCMPDS)-valued NAT-defined Function;
attr IT is shiftable means
:Def9:
for n,i st n in dom IT & i=IT.(n)
holds InsCode i <> 1 & InsCode i <> 3 & i valid_at n;
end;
Lm2: Load halt SCMPDS is shiftable
proof
set m = Load halt SCMPDS;
A1: dom m={ 0} by FUNCOP_1:13;
let n,i;
assume that
A2: n in dom m and
A3: i=m.( n);
A4: n= 0 by A1,A2,TARSKI:def 1;
i = [0,{},{}] by A3,A4,SCMPDS_2:80;
then InsCode i = 0;
hence thesis;
end;
theorem Th20:
for i be Instruction of SCMPDS,m,n be Nat st i
valid_at m & m <= n holds i valid_at n
proof
let i be Instruction of SCMPDS,m,n be Nat;
assume that
A1: i valid_at m and
A2: m <= n;
A3: now
assume
InsCode i= 4;
then consider a,k1,k2 such that
A4: i = (a,k1)<>0_goto k2 and
A5: m+k2 >= 0 by A1;
take a,k1,k2;
thus i = (a,k1)<>0_goto k2 by A4;
thus n+k2 >= 0 by A2,A5,XREAL_1:6;
end;
A6: now
assume
InsCode i= 6;
then consider a,k1,k2 such that
A7: i = (a,k1)>=0_goto k2 and
A8: m+k2 >= 0 by A1;
take a,k1,k2;
thus i = (a,k1)>=0_goto k2 by A7;
thus n+k2 >= 0 by A2,A8,XREAL_1:6;
end;
A9: now
assume
InsCode i= 5;
then consider a,k1,k2 such that
A10: i = (a,k1)<=0_goto k2 and
A11: m+k2 >= 0 by A1;
take a,k1,k2;
thus i = (a,k1)<=0_goto k2 by A10;
thus n+k2 >= 0 by A2,A11,XREAL_1:6;
end;
now
assume
InsCode i= 14;
then consider k1 such that
A12: i=goto k1 and
A13: m+k1 >= 0 by A1;
take k1;
thus i=goto k1 by A12;
thus n+k1 >= 0 by A2,A13,XREAL_1:6;
end;
hence thesis by A3,A9,A6;
end;
registration
cluster parahalting shiftable for Program of SCMPDS;
existence by Lm1,Lm2;
end;
definition
let i be Instruction of SCMPDS;
attr i is shiftable means
:Def10:
InsCode i = 2 or InsCode i <> 14 & InsCode i > 6;
end;
registration
cluster shiftable for Instruction of SCMPDS;
existence
proof
take i=DataLoc(0,0):=1;
thus thesis;
end;
end;
registration
let a,k1;
cluster a := k1 -> shiftable;
coherence;
end;
registration
let a,k1,k2;
cluster (a,k1) := k2 -> shiftable;
coherence;
end;
registration
let a,k1,k2;
cluster AddTo(a,k1,k2) -> shiftable;
coherence;
end;
registration
let a,b,k1,k2;
cluster AddTo(a,k1,b,k2) -> shiftable;
coherence
proof
InsCode AddTo(a,k1,b,k2)=9 by SCMPDS_2:21;
hence thesis;
end;
cluster SubFrom(a,k1,b,k2) -> shiftable;
coherence
proof
InsCode SubFrom(a,k1,b,k2)=10 by SCMPDS_2:22;
hence thesis;
end;
cluster MultBy(a,k1,b,k2) -> shiftable;
coherence
proof
InsCode MultBy(a,k1,b,k2)=11 by SCMPDS_2:23;
hence thesis;
end;
cluster Divide(a,k1,b,k2) -> shiftable;
coherence
proof
InsCode Divide(a,k1,b,k2)=12 by SCMPDS_2:24;
hence thesis;
end;
cluster (a,k1) := (b,k2) -> shiftable;
coherence
proof
InsCode (a,k1) := (b,k2)=13 by SCMPDS_2:25;
hence thesis;
end;
end;
registration
let I,J be shiftable Program of SCMPDS;
cluster I ';' J -> shiftable for Program of SCMPDS;
coherence
proof
set IJ=I ';' J;
now
set D = {l+card I where l is Nat: l in dom J };
let n,i such that
A1: n in dom IJ and
A2: i=IJ.( n);
dom Shift(J,card I) = D by VALUED_1:def 12;
then
A3: dom IJ = dom I \/ D by FUNCT_4:def 1;
per cases by A1,A3,XBOOLE_0:def 3;
suppose
A4: n in dom I;
then I. n=i by A2,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A4,Def9;
end;
suppose
n in D;
then consider l being Nat such that
A5: n = l+card I and
A6: l in dom J;
A7: J. l =i by A2,A5,A6,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3 by A6,Def9;
i valid_at l by A6,A7,Def9;
hence i valid_at n by A5,Th20,NAT_1:11;
end;
end;
hence thesis;
end;
end;
registration
let i be shiftable Instruction of SCMPDS;
cluster Load i -> shiftable for Program of SCMPDS;
coherence
proof let p be Program of SCMPDS such that
A1: p = Load i;
let n,j such that
A2: n in dom p and
A3: j=p. n;
dom p = { 0 } by A1,FUNCOP_1:13;
then n = 0 by A2,TARSKI:def 1;
then
A4: j=i by A3,A1;
hence InsCode j <> 1 by Def10;
thus InsCode j <> 3 by A4,Def10;
InsCode j <> 4 & InsCode j <> 5 & InsCode j <> 6 & InsCode j <> 14
by A4,Def10;
hence j valid_at n;
end;
end;
registration
let i be shiftable Instruction of SCMPDS, J be shiftable Program of SCMPDS;
cluster i ';' J -> shiftable;
coherence;
end;
registration
let I be shiftable Program of SCMPDS, j be shiftable Instruction of SCMPDS;
cluster I ';' j -> shiftable;
coherence;
end;
registration
let i,j be shiftable Instruction of SCMPDS;
cluster i ';' j -> shiftable;
coherence;
end;
registration
cluster Stop SCMPDS -> parahalting shiftable;
coherence by Lm1,Lm2;
end;
registration
let I be shiftable Program of SCMPDS;
cluster stop I -> shiftable;
coherence;
end;
theorem
for I being shiftable Program of SCMPDS,k1 be Integer st card I + k1
>= 0 holds I ';' goto k1 is shiftable
proof
let I be shiftable Program of SCMPDS,k1 be Integer;
set J= Load goto k1;
set Ig=I ';' goto k1;
assume
A1: card I + k1 >= 0;
now
set D = {l+card I where l is Nat: l in dom J };
let n,i such that
A2: n in dom Ig and
A3: i=Ig.( n);
dom Shift(J,card I) = D by VALUED_1:def 12;
then
A4: dom Ig = dom I \/ D by FUNCT_4:def 1;
per cases by A2,A4,XBOOLE_0:def 3;
suppose
A5: n in dom I;
then I. n=i by A3,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A5,Def9;
end;
suppose
n in D;
then consider l being Nat such that
A6: n = l+card I and
A7: l in dom J;
dom J = { 0 } by FUNCOP_1:13;
then
A8: l = 0 by A7,TARSKI:def 1;
then
A9: goto k1 =J. l
.=i by A3,A6,A7,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3;
thus i valid_at n by A1,A6,A8,A9;
end;
end;
hence thesis;
end;
registration
let n be Nat;
cluster Load goto n -> shiftable for Program of SCMPDS;
coherence
proof
set k1=n;
set J= Load goto k1;
now
let n,i such that
A1: n in dom J and
A2: i=J. n;
dom J = { 0 } by FUNCOP_1:13;
then n = 0 by A1,TARSKI:def 1;
then
A3: goto k1 =i by A2;
hence InsCode i <> 1 & InsCode i <> 3;
A4: n+k1 >=0 & InsCode i <> 6 by A3;
thus i valid_at n by A3,A4;
end;
hence thesis;
end;
end;
theorem
for I being shiftable Program of SCMPDS,k1,k2 be Integer,a be
Int_position st card I + k2 >= 0 holds I ';' (a,k1)<>0_goto k2 is shiftable
proof
let I be shiftable Program of SCMPDS,k1,k2 be Integer,a be Int_position;
set ii= (a,k1)<>0_goto k2, J= Load ii;
set Ig=I ';' ii;
assume
A1: card I + k2 >= 0;
now
set D = {l+card I where l is Nat: l in dom J };
let n,i such that
A2: n in dom Ig and
A3: i=Ig.( n);
dom Shift(J,card I) = D by VALUED_1:def 12;
then
A4: dom Ig = dom I \/ D by FUNCT_4:def 1;
per cases by A2,A4,XBOOLE_0:def 3;
suppose
A5: n in dom I;
then I. n=i by A3,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A5,Def9;
end;
suppose
n in D;
then consider l being Nat such that
A6: n = l+card I and
A7: l in dom J;
dom J = { 0 } by FUNCOP_1:13;
then
A8: l = 0 by A7,TARSKI:def 1;
then
A9: ii=J. l
.=i by A3,A6,A7,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3;
thus i valid_at n by A1,A6,A8,A9;
end;
end;
hence thesis;
end;
registration
let k1 be Integer,a be Int_position,n be Nat;
cluster Load (a,k1)<>0_goto n -> shiftable for Program of SCMPDS;
coherence
proof
set k2=n;
set ii= (a,k1)<>0_goto k2, J= Load ii;
now
let n,i such that
A1: n in dom J and
A2: i=J. n;
dom J = { 0 } by FUNCOP_1:13;
then n = 0 by A1,TARSKI:def 1;
then
A3: ii =i by A2;
hence InsCode i <> 1 & InsCode i <> 3;
A4: n+k2 >=0 & InsCode i <> 6 & InsCode i <> 14 by A3;
thus i valid_at n by A3,A4;
end;
hence thesis;
end;
end;
theorem
for I being shiftable Program of SCMPDS,k1,k2 be Integer,a be
Int_position st card I + k2 >= 0 holds I ';' (a,k1)<=0_goto k2 is shiftable
proof
let I be shiftable Program of SCMPDS,k1,k2 be Integer,a be Int_position;
set ii= (a,k1)<=0_goto k2, J= Load ii;
set Ig=I ';' ii;
assume
A1: card I + k2 >= 0;
now
set D = {l+card I where l is Nat: l in dom J };
let n,i such that
A2: n in dom Ig and
A3: i=Ig.( n);
dom Shift(J,card I) = D by VALUED_1:def 12;
then
A4: dom Ig = dom I \/ D by FUNCT_4:def 1;
per cases by A2,A4,XBOOLE_0:def 3;
suppose
A5: n in dom I;
then I. n=i by A3,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A5,Def9;
end;
suppose
n in D;
then consider l being Nat such that
A6: n = l+card I and
A7: l in dom J;
dom J = { 0 } by FUNCOP_1:13;
then
A8: l = 0 by A7,TARSKI:def 1;
then
A9: ii =J. l
.=i by A3,A6,A7,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3;
thus i valid_at n by A1,A6,A8,A9;
end;
end;
hence thesis;
end;
registration
let k1 be Integer,a be Int_position,n be Nat;
cluster Load (a,k1)<=0_goto n -> shiftable for Program of SCMPDS;
coherence
proof
set k2=n;
set ii= (a,k1)<=0_goto k2, J= Load ii;
now
let n,i such that
A1: n in dom J and
A2: i=J. n;
dom J = { 0 } by FUNCOP_1:13;
then n = 0 by A1,TARSKI:def 1;
then
A3: ii =i by A2;
hence InsCode i <> 1 & InsCode i <> 3;
A4: n+k2 >=0 & InsCode i <> 6 & InsCode i <> 14 by A3;
thus i valid_at n by A3,A4;
end;
hence thesis;
end;
end;
theorem
for I being shiftable Program of SCMPDS,k1,k2 be Integer,a be
Int_position st card I + k2 >= 0 holds I ';' (a,k1)>=0_goto k2 is shiftable
proof
let I be shiftable Program of SCMPDS,k1,k2 be Integer,a be Int_position;
set ii= (a,k1)>=0_goto k2, J= Load ii;
set Ig=I ';' ii;
assume
A1: card I + k2 >= 0;
now
set D = {l+card I where l is Nat: l in dom J };
let n,i such that
A2: n in dom Ig and
A3: i=Ig.( n);
dom Shift(J,card I) = D by VALUED_1:def 12;
then
A4: dom Ig = dom I \/ D by FUNCT_4:def 1;
per cases by A2,A4,XBOOLE_0:def 3;
suppose
A5: n in dom I;
then I. n=i by A3,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3 & i valid_at n by A5,Def9;
end;
suppose
n in D;
then consider l being Nat such that
A6: n = l+card I and
A7: l in dom J;
dom J = { 0 } by FUNCOP_1:13;
then
A8: l = 0 by A7,TARSKI:def 1;
then
A9: ii =J. l
.=i by A3,A6,A7,AFINSQ_1:def 3;
hence InsCode i <> 1 & InsCode i <> 3;
thus i valid_at n by A1,A6,A8,A9;
end;
end;
hence thesis;
end;
registration
let k1 be Integer,a be Int_position,n be Nat;
cluster Load (a,k1)>=0_goto n -> shiftable for Program of SCMPDS;
coherence
proof
set k2=n;
set ii= (a,k1)>=0_goto k2, J= Load ii;
now
let n,i such that
A1: n in dom J and
A2: i=J. n;
dom J = { 0 } by FUNCOP_1:13;
then n = 0 by A1,TARSKI:def 1;
then
A3: ii =i by A2;
hence InsCode i <> 1 & InsCode i <> 3;
A4: n+k2 >=0 & InsCode i <> 5 & InsCode i <> 14 by A3;
thus i valid_at n by A3,A4;
end;
hence thesis;
end;
end;
theorem Th25:
for s1,s2 being State of SCMPDS, n,m being Nat,k1 be
Integer st IC s1= m & m+k1>=0 & IC s1 + n = IC s2
holds ICplusConst(s1,k1) +n = ICplusConst(s2,k1)
proof
let s1,s2 be State of SCMPDS, n,m be Nat,k1 be Integer;
assume that
A1: IC s1= m and
A2: m+k1>=0 and
A3: IC s1 + n = IC s2;
reconsider nk = ICplusConst(s1,k1) as Element of NAT;
reconsider mk=m+k1 as Element of NAT by A2,INT_1:3;
ex n1 be Element of NAT st n1 = IC s1 & ICplusConst(s1, k1) = |.n1+k1.|
by SCMPDS_2:def 18;
then
(ex n2 be Element of NAT st n2 = IC s2 & ICplusConst(s2, k1) = |.n2+k1.|
)& nk=mk by A1,ABSVALUE:def 1,SCMPDS_2:def 18;
hence thesis by A1,A3,ABSVALUE:def 1;
end;
theorem Th26:
for s1,s2 being State of SCMPDS, n,m being Nat, i
being Instruction of SCMPDS holds IC s1= m & i valid_at m & InsCode i <>
1 & InsCode i <> 3 & IC s1 + n = IC s2 & DataPart s1 = DataPart s2 implies
IC Exec(i,s1) + n = IC Exec(i,s2) & DataPart Exec(i,s1) = DataPart Exec(i,s2)
proof
let s1,s2 be State of SCMPDS, n,m be Nat;
let i be Instruction of SCMPDS;
assume that
A1: IC s1= m and
A2: i valid_at m and
A3: InsCode i <> 1 & InsCode i <> 3 and
A4: IC s1 + n = IC s2 and
A5: DataPart s1 = DataPart s2;
A6: now
let a,k1;
thus s1.DataLoc(s1.a,k1) =s1.DataLoc(s2.a,k1) by A5,Th7
.=s2.DataLoc(s2.a,k1) by A5,Th7;
end;
reconsider k1 = IC s1 as Nat;
set Ci=InsCode i;
A7: IC s1 + 1 + n = IC s2 + 1 by A4;
A8: now
assume
Ci <> 0 & Ci <> 14 & Ci<>1 & Ci<>4 & Ci<>5 & Ci<> 6;
then
A9: not Ci in {0,1,4,5,6,14} by ENUMSET1:def 4;
then IC Exec(i,s1) = IC s1 + 1 by Th1;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A7,A9,Th1;
end;
Ci = 0 or ... or Ci = 14 by SCMPDS_2:6;
then per cases by A3;
suppose Ci = 0;
then
A10: Exec(i,s1) = s1 & Exec(i,s2) = s2 by SCMPDS_2:86;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A4;
thus DataPart Exec(i,s1) = DataPart Exec(i,s2) by A5,A10;
end;
suppose
Ci = 14;
then consider k1 such that
A11: i = goto k1 and
A12: m+k1 >= 0 by A2;
IC Exec(i,s1) = ICplusConst(s1,k1) by A11,SCMPDS_2:54;
hence IC Exec(i,s1) + n = ICplusConst(s2,k1) by A1,A4,A12,Th25
.= IC Exec(i,s2) by A11,SCMPDS_2:54;
now
let a;
thus Exec(i, s1).a = s1.a by A11,SCMPDS_2:54
.=s2.a by A5,Th7
.=Exec(i, s2).a by A11,SCMPDS_2:54;
end;
hence thesis by Th7;
end;
suppose
A13: Ci = 2;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A8;
consider a,k1 such that
A14: i = a := k1 by A13,SCMPDS_2:28;
now
let b;
per cases;
suppose
A15: a=b;
hence Exec(i, s1).b= k1 by A14,SCMPDS_2:45
.=Exec(i,s2).b by A14,A15,SCMPDS_2:45;
end;
suppose
A16: a<>b;
hence Exec(i,s1).b = s1.b by A14,SCMPDS_2:45
.=s2.b by A5,Th7
.=Exec(i,s2).b by A14,A16,SCMPDS_2:45;
end;
end;
hence thesis by Th7;
end;
suppose
Ci = 4;
then consider a,k1,k2 such that
A17: i = (a,k1)<>0_goto k2 and
A18: m+k2 >= 0 by A2;
hereby
per cases;
suppose
A19: s1.DataLoc(s1.a,k1) <> 0;
then
A20: s2.DataLoc(s2.a,k1) <> 0 by A6;
IC Exec(i,s1) = ICplusConst(s1,k2) by A17,A19,SCMPDS_2:55;
hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A4,A18,Th25
.= IC Exec(i,s2) by A17,A20,SCMPDS_2:55;
end;
suppose
s1.DataLoc(s1.a,k1) = 0;
then s2.DataLoc(s2.a,k1) = 0 & IC Exec(i,s1) = IC s1 + 1 by A6,A17,
SCMPDS_2:55;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A7,A17,SCMPDS_2:55;
end;
end;
now
let a;
thus Exec(i, s1).a = s1.a by A17,SCMPDS_2:55
.=s2.a by A5,Th7
.=Exec(i, s2).a by A17,SCMPDS_2:55;
end;
hence thesis by Th7;
end;
suppose
Ci = 5;
then consider a,k1,k2 such that
A21: i = (a,k1)<=0_goto k2 and
A22: m+k2 >= 0 by A2;
hereby
per cases;
suppose
A23: s1.DataLoc(s1.a,k1) <= 0;
then
A24: s2.DataLoc(s2.a,k1) <= 0 by A6;
IC Exec(i,s1) = ICplusConst(s1,k2) by A21,A23,SCMPDS_2:56;
hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A4,A22,Th25
.= IC Exec(i,s2) by A21,A24,SCMPDS_2:56;
end;
suppose
s1.DataLoc(s1.a,k1) > 0;
then s2.DataLoc(s2.a,k1) > 0 & IC Exec(i,s1) = IC s1 + 1 by A6,A21,
SCMPDS_2:56;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A7,A21,SCMPDS_2:56;
end;
end;
now
let a;
thus Exec(i, s1).a = s1.a by A21,SCMPDS_2:56
.=s2.a by A5,Th7
.=Exec(i, s2).a by A21,SCMPDS_2:56;
end;
hence thesis by Th7;
end;
suppose
Ci = 6;
then consider a,k1,k2 such that
A25: i = (a,k1)>=0_goto k2 and
A26: m+k2 >= 0 by A2;
hereby
per cases;
suppose
A27: s1.DataLoc(s1.a,k1) >= 0;
then
A28: s2.DataLoc(s2.a,k1) >= 0 by A6;
IC Exec(i,s1) = ICplusConst(s1,k2) by A25,A27,SCMPDS_2:57;
hence IC Exec(i,s1) + n = ICplusConst(s2,k2) by A1,A4,A26,Th25
.= IC Exec(i,s2) by A25,A28,SCMPDS_2:57;
end;
suppose
s1.DataLoc(s1.a,k1) < 0;
then s2.DataLoc(s2.a,k1) < 0 & IC Exec(i,s1) = IC s1 + 1 by A6,A25,
SCMPDS_2:57;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A7,A25,SCMPDS_2:57;
end;
end;
now
let a;
thus Exec(i, s1).a = s1.a by A25,SCMPDS_2:57
.=s2.a by A5,Th7
.=Exec(i, s2).a by A25,SCMPDS_2:57;
end;
hence thesis by Th7;
end;
suppose
A29: Ci = 7;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A8;
consider a,k1,k2 such that
A30: i = (a,k1) := k2 by A29,SCMPDS_2:33;
now
let b;
per cases;
suppose
A31: DataLoc(s1.a,k1)=b;
then
A32: DataLoc(s2.a,k1)=b by A5,Th7;
thus Exec(i, s1).b= k2 by A30,A31,SCMPDS_2:46
.=Exec(i,s2).b by A30,A32,SCMPDS_2:46;
end;
suppose
A33: DataLoc(s1.a,k1)<>b;
then
A34: DataLoc(s2.a,k1)<>b by A5,Th7;
thus Exec(i,s1).b = s1.b by A30,A33,SCMPDS_2:46
.=s2.b by A5,Th7
.=Exec(i,s2).b by A30,A34,SCMPDS_2:46;
end;
end;
hence thesis by Th7;
end;
suppose
A35: Ci = 8;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A8;
consider a,k1,k2 such that
A36: i = AddTo(a,k1,k2) by A35,SCMPDS_2:34;
now
let b;
per cases;
suppose
A37: DataLoc(s1.a,k1)=b;
then
A38: DataLoc(s2.a,k1)=b by A5,Th7;
thus Exec(i, s1).b= s1.DataLoc(s1.a,k1)+k2 by A36,A37,SCMPDS_2:48
.= s2.DataLoc(s2.a,k1)+k2 by A6
.=Exec(i,s2).b by A36,A38,SCMPDS_2:48;
end;
suppose
A39: DataLoc(s1.a,k1)<>b;
then
A40: DataLoc(s2.a,k1)<>b by A5,Th7;
thus Exec(i,s1).b = s1.b by A36,A39,SCMPDS_2:48
.=s2.b by A5,Th7
.=Exec(i,s2).b by A36,A40,SCMPDS_2:48;
end;
end;
hence thesis by Th7;
end;
suppose
A41: Ci = 9;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A8;
consider a,b,k1,k2 such that
A42: i = AddTo(a,k1,b,k2) by A41,SCMPDS_2:35;
now
let c;
per cases;
suppose
A43: DataLoc(s1.a,k1)=c;
then
A44: DataLoc(s2.a,k1)=c by A5,Th7;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)+s1.DataLoc(s1.b,k2) by A42,A43
,SCMPDS_2:49
.= s2.DataLoc(s2.a,k1)+s1.DataLoc(s1.b,k2) by A6
.= s2.DataLoc(s2.a,k1)+s2.DataLoc(s2.b,k2) by A6
.=Exec(i,s2).c by A42,A44,SCMPDS_2:49;
end;
suppose
A45: DataLoc(s1.a,k1)<>c;
then
A46: DataLoc(s2.a,k1)<>c by A5,Th7;
thus Exec(i,s1).c = s1.c by A42,A45,SCMPDS_2:49
.=s2.c by A5,Th7
.=Exec(i,s2).c by A42,A46,SCMPDS_2:49;
end;
end;
hence thesis by Th7;
end;
suppose
A47: Ci = 10;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A8;
consider a,b,k1,k2 such that
A48: i = SubFrom(a,k1,b,k2) by A47,SCMPDS_2:36;
now
let c;
per cases;
suppose
A49: DataLoc(s1.a,k1)=c;
then
A50: DataLoc(s2.a,k1)=c by A5,Th7;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)-s1.DataLoc(s1.b,k2) by A48,A49
,SCMPDS_2:50
.= s2.DataLoc(s2.a,k1)-s1.DataLoc(s1.b,k2) by A6
.= s2.DataLoc(s2.a,k1)-s2.DataLoc(s2.b,k2) by A6
.=Exec(i,s2).c by A48,A50,SCMPDS_2:50;
end;
suppose
A51: DataLoc(s1.a,k1)<>c;
then
A52: DataLoc(s2.a,k1)<>c by A5,Th7;
thus Exec(i,s1).c = s1.c by A48,A51,SCMPDS_2:50
.=s2.c by A5,Th7
.=Exec(i,s2).c by A48,A52,SCMPDS_2:50;
end;
end;
hence thesis by Th7;
end;
suppose
A53: Ci = 11;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A8;
consider a,b,k1,k2 such that
A54: i = MultBy(a,k1,b,k2) by A53,SCMPDS_2:37;
now
let c;
per cases;
suppose
A55: DataLoc(s1.a,k1)=c;
then
A56: DataLoc(s2.a,k1)=c by A5,Th7;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)*s1.DataLoc(s1.b,k2) by A54,A55
,SCMPDS_2:51
.= s2.DataLoc(s2.a,k1)*s1.DataLoc(s1.b,k2) by A6
.= s2.DataLoc(s2.a,k1)*s2.DataLoc(s2.b,k2) by A6
.=Exec(i,s2).c by A54,A56,SCMPDS_2:51;
end;
suppose
A57: DataLoc(s1.a,k1)<>c;
then
A58: DataLoc(s2.a,k1)<>c by A5,Th7;
thus Exec(i,s1).c = s1.c by A54,A57,SCMPDS_2:51
.=s2.c by A5,Th7
.=Exec(i,s2).c by A54,A58,SCMPDS_2:51;
end;
end;
hence thesis by Th7;
end;
suppose
A59: Ci = 12;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A8;
consider a,b,k1,k2 such that
A60: i = Divide(a,k1,b,k2) by A59,SCMPDS_2:38;
now
let c;
per cases;
suppose
A61: DataLoc(s1.b,k2)=c;
then
A62: DataLoc(s2.b,k2)=c by A5,Th7;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) mod s1.DataLoc(s1.b,k2) by A60
,A61,SCMPDS_2:52
.= s2.DataLoc(s2.a,k1) mod s1.DataLoc(s1.b,k2) by A6
.= s2.DataLoc(s2.a,k1) mod s2.DataLoc(s2.b,k2) by A6
.= Exec(i,s2).c by A60,A62,SCMPDS_2:52;
end;
suppose
A63: DataLoc(s1.b,k2)<>c;
then
A64: DataLoc(s2.b,k2)<>c by A5,Th7;
hereby
per cases;
suppose
A65: DataLoc(s1.a,k1)<>c;
then
A66: DataLoc(s2.a,k1)<>c by A5,Th7;
thus Exec(i, s1).c = s1.c by A60,A63,A65,SCMPDS_2:52
.=s2.c by A5,Th7
.=Exec(i,s2).c by A60,A64,A66,SCMPDS_2:52;
end;
suppose
A67: DataLoc(s1.a,k1)=c;
then
A68: DataLoc(s2.a,k1)=c by A5,Th7;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) div s1.DataLoc(s1.b,k2)
by A60,A63,A67,SCMPDS_2:52
.= s2.DataLoc(s2.a,k1) div s1.DataLoc(s1.b,k2) by A6
.= s2.DataLoc(s2.a,k1) div s2.DataLoc(s2.b,k2) by A6
.= Exec(i,s2).c by A60,A64,A68,SCMPDS_2:52;
end;
end;
end;
end;
hence thesis by Th7;
end;
suppose
A69: Ci = 13;
hence IC Exec(i,s1) + n = IC Exec(i,s2) by A8;
consider a,b,k1,k2 such that
A70: i = (a,k1):=(b,k2) by A69,SCMPDS_2:39;
now
let c;
per cases;
suppose
A71: DataLoc(s1.a,k1)=c;
then
A72: DataLoc(s2.a,k1)=c by A5,Th7;
thus Exec(i, s1).c = s1.DataLoc(s1.b,k2) by A70,A71,SCMPDS_2:47
.= s2.DataLoc(s2.b,k2) by A6
.=Exec(i,s2).c by A70,A72,SCMPDS_2:47;
end;
suppose
A73: DataLoc(s1.a,k1)<>c;
then
A74: DataLoc(s2.a,k1)<>c by A5,Th7;
thus Exec(i,s1).c = s1.c by A70,A73,SCMPDS_2:47
.=s2.c by A5,Th7
.=Exec(i,s2).c by A70,A74,SCMPDS_2:47;
end;
end;
hence thesis by Th7;
end;
end;
theorem
for P1,P2 being Instruction-Sequence of SCMPDS
for s1 being 0-started State of SCMPDS
for J being parahalting shiftable Program of SCMPDS st stop J c= P1
for n being Nat st Shift(stop J,n) c= P2 &
IC s2 = n & DataPart s1 = DataPart s2
for i being Nat holds
IC Comput(P1,s1,i) + n = IC Comput(P2,s2,i) &
CurInstr(P1,Comput(P1,s1,i)) =
CurInstr(P2,Comput(P2,s2,i)) &
DataPart Comput(P1,s1,i) = DataPart
Comput(P2,s2,i)
proof
let P1,P2 be Instruction-Sequence of SCMPDS;
let s1 be 0-started State of SCMPDS;
let I be parahalting shiftable Program of SCMPDS;
set SI=stop I;
assume
A1: SI c= P1;
let n be Nat;
assume that
A2: Shift(SI,n) c= P2 and
A3: IC s2 = n and
A4: DataPart s1 = DataPart s2;
A5: 0 in dom SI by COMPOS_1:36;
then
A6: 0 + n in dom Shift(SI,n) by VALUED_1:24;
defpred P[Nat] means IC Comput(P1,s1,$1) + n = IC Comput(
P2,s2,$1) &
CurInstr(P1,Comput(P1,s1,$1))
= CurInstr(P2,Comput(P2,s2,$1)) & DataPart
Comput(P1,s1,$1) = DataPart Comput(P2,s2,$1);
A7: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A8: P[k];
reconsider m = IC Comput(P1,s1,k) as Nat;
set i = CurInstr(P1,Comput(P1,s1,k));
A9: Comput(P1,s1,k+1) =
Following(P1,Comput(P1,s1,k))
by EXTPRO_1:3
.= Exec(CurInstr(P1,Comput(P1,s1,k)),
Comput(P1,s1,k));
reconsider l = IC Comput(P1,s1,k+1) as Nat;
A10: IC Comput(P1,s1,k+1) in dom SI by A1,Def6;
then
A11: l+n in dom Shift(SI,n) by VALUED_1:24;
A12: Comput(P2,s2,k+1) =
Following(P2,Comput(P2,s2,k))
by EXTPRO_1:3
.= Exec(CurInstr(P2,Comput(P2,s2,k)),
Comput(P2,s2,k));
A13: IC Comput(P1,s1,k)
in dom SI by A1,Def6;
A14: i = P1.IC Comput(P1,s1,k) by PBOOLE:143
.= SI.IC Comput(P1,s1,k) by A1,A13,GRFUNC_1:2;
then
A15: InsCode i <> 1 & InsCode i <> 3 by A13,Def9;
A16: i valid_at m by A13,A14,Def9;
hence
A17: IC Comput(P1,s1,k+1) + n = IC Comput(P2,s2,k+1)
by A8,A9,A12,A15,Th26;
CurInstr(P1,Comput(P1,s1,k+1)) = P1.l by PBOOLE:143
.= SI.l by A1,A10,GRFUNC_1:2;
hence CurInstr(P1,Comput(P1,s1,k+1))
= Shift(SI,n).(IC Comput(P2,s2,k+1)) by A17,A10,VALUED_1:def 12
.= P2.IC Comput(P2,s2,k+1) by A2,A17,A11,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s2,k+1)) by PBOOLE:143;
thus thesis by A8,A9,A12,A15,A16,Th26;
end;
A18: P1.IC s1 = P1. 0 by MEMSTR_0:def 11
.= SI. 0 by A1,A5,GRFUNC_1:2;
let i be Nat;
A19: DataPart Comput(P1,s1,0) = DataPart s2 by A4
.= DataPart Comput(P2,s2,0);
A20: IC Comput(P1,s1,0)
= IC s1
.= 0 by MEMSTR_0:def 11;
A21: P2/.IC s2 = P2.IC s2 by PBOOLE:143;
A22: P1/.IC s1 = P1.IC s1 by PBOOLE:143;
CurInstr(P1,Comput(P1,s1,0))
= CurInstr(P1,s1)
.= Shift(SI,n).( 0 + n) by A5,A18,A22,VALUED_1:def 12
.= CurInstr(P2,Comput(P2,s2,0))
by A2,A3,A6,A21,GRFUNC_1:2;
then
A23: P[0] by A3,A20,A19;
for k being Nat holds P[k] from NAT_1:sch 2(A23,A7);
hence thesis;
end;