:: Computation of Two Consecutive 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, SCMPDS_2, AMI_1, FSM_1, INT_1, SETFAM_1,
RELAT_1, SCMFSA_7, CARD_1, SCMPDS_4, FUNCT_1, AMISTD_2, VALUED_1,
ARYTM_3, TARSKI, XXREAL_0, TURING_1, FUNCT_4, XBOOLE_0, SCMFSA6B,
CIRCUIT2, GRAPHSP, MSUALG_1, AMI_2, AMI_3, SCMPDS_1, COMPLEX1, STRUCT_0,
ARYTM_1, NAT_1, SCMPDS_5, PARTFUN1, EXTPRO_1, SCMFSA6C, COMPOS_1,
SCMFSA6A;
notations TARSKI, XBOOLE_0, XTUPLE_0, SETFAM_1, ENUMSET1, SUBSET_1, CARD_1,
ORDINAL1, NUMBERS, XCMPLX_0, RELAT_1, FUNCT_1, PARTFUN1, FUNCT_4, INT_1,
NAT_1, STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, VALUED_1, AMI_2,
FUNCT_7, SCMPDS_I, SCMPDS_1, SCMPDS_2, INT_2, SCMPDS_4, XXREAL_0;
constructors ENUMSET1, XXREAL_0, REAL_1, INT_2, SCMPDS_1, SCMPDS_4, PRE_POLY,
DOMAIN_1, AMI_3, NAT_D, MEMSTR_0, RELSET_1, XTUPLE_0;
registrations XREAL_0, INT_1, SCMPDS_2, SCMPDS_4, ORDINAL1, AFINSQ_1,
COMPOS_1, EXTPRO_1, FUNCT_4, MEMSTR_0, AMI_3, COMPOS_0, XTUPLE_0, NAT_1;
requirements NUMERALS, REAL, SUBSET, BOOLE, ARITHM;
definitions TARSKI, COMPOS_1, SCMPDS_4, EXTPRO_1, COMPOS_0;
equalities FUNCOP_1, COMPOS_1, SCMPDS_4, AFINSQ_1, EXTPRO_1, MEMSTR_0,
COMPOS_0;
expansions TARSKI, COMPOS_1, SCMPDS_4, EXTPRO_1, COMPOS_0;
theorems NAT_1, TARSKI, FUNCT_4, FUNCT_1, INT_1, RELAT_1, SCMPDS_2, SCMPDS_3,
ENUMSET1, ABSVALUE, GRFUNC_1, SCMPDS_4, MEMSTR_0, XBOOLE_0, XBOOLE_1,
XREAL_1, FUNCOP_1, XXREAL_0, VALUED_1, AFINSQ_1, PBOOLE, PARTFUN1,
COMPOS_1, EXTPRO_1, AMI_2, COMPOS_0;
schemes NAT_1;
begin :: Preliminaries
reserve x for set,
m,n for Nat,
a,b,c for Int_position,
i for Instruction of SCMPDS,
s,s1,s2 for State of SCMPDS,
k1,k2 for Integer,
loc,l1 for Nat,
I,J for Program of SCMPDS,
N for with_non-empty_elements set;
Lm1: card Stop SCMPDS = 1 by AFINSQ_1:34;
::$CT 11
theorem Th1:
for I,J being Program of SCMPDS holds I c= stop (I ';' J)
proof
let I,J be Program of SCMPDS;
set IS=I ';' (J ';' Stop SCMPDS),
Ip=stop (I ';' J);
A1: I c= IS by AFINSQ_1:74;
thus thesis by A1,AFINSQ_1:27;
end;
theorem Th2:
dom stop I c= dom stop (I ';' J)
proof
set sI=stop I, sIJ=stop (I ';'J);
A1: card sIJ=card (I ';' J) +1 by Lm1,AFINSQ_1:17
.=card I + card J +1 by AFINSQ_1:17
.=card I + 1 + card J;
card sI=card I +1 by Lm1,AFINSQ_1:17;
then
A2: card sI <= card sIJ by A1,NAT_1:11;
set A = NAT;
let x be object;
assume
A3: x in dom sI;
dom sI c= A by RELAT_1:def 18;
then reconsider l=x as Nat by A3;
reconsider n = l as Nat;
n < card sI by A3,AFINSQ_1:66;
then n < card sIJ by A2,XXREAL_0:2;
hence x in dom sIJ by AFINSQ_1:66;
end;
theorem Th3:
for I,J being Program of SCMPDS holds
stop I +* stop (I ';' J) = stop (I ';' J)
proof
let I,J be Program of SCMPDS;
set sI=stop I, IsI=sI, sIJ=stop (I ';' J), IsIJ= sIJ;
dom sI c= dom sIJ by Th2;
hence thesis by FUNCT_4:19;
end;
set SA0 = Start-At(0,SCMPDS);
theorem Th4:
(Initialize s).a = s.a
proof
not a in dom SA0 by SCMPDS_4:18;
hence (Initialize s).a =s.a by FUNCT_4:11;
end;
reserve P,P1,P2,Q for Instruction-Sequence of SCMPDS;
theorem Th5:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS
st stop I c= P1 & stop I c= P2
for k being Nat holds
Comput(P1,s,k) = Comput(P2,s,k) &
CurInstr(P1,Comput(P1,s,k)) = CurInstr(P2,Comput(P2,s,k))
proof
let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS;
set SI=stop I;
assume that
A1: SI c= P1 and
A2: SI c= P2;
let k be Nat;
A3: IC Comput(P1,s,k) in dom SI by A1,SCMPDS_4:def 6;
A4: IC Comput(P2,s,k) in dom SI by A2,SCMPDS_4:def 6;
for m being Nat st m < k holds IC(Comput(P2,s,m))
in dom
SI by A2,SCMPDS_4:def 6;
hence
A5: Comput(P1,s,k) = Comput(P2,s,k) by A1,A2,SCMPDS_4:21;
thus CurInstr(P2,Comput(P2,s,k))
= P2.IC Comput(P2,s,k) by PBOOLE:143
.= SI.IC Comput(P2,s,k) by A2,A4,GRFUNC_1:2
.= P1.IC Comput(P1,s,k) by A1,A5,A3,GRFUNC_1:2
.= CurInstr(P1,Comput(P1,s,k)) by PBOOLE:143;
end;
theorem Th6:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS
st stop I c= P1 & stop I c= P2
holds LifeSpan(P1,s) = LifeSpan(P2,s) &
Result(P1,s) = Result(P2,s)
proof
let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS;
set SI=stop I;
assume that
A1: SI c= P1 and
A2: SI c= P2;
A3: P2 halts_on s by A2,SCMPDS_4:def 7;
A4: P1 halts_on s by A1,SCMPDS_4:def 7;
A5: now
let l be Nat;
assume
A6: CurInstr(P2,Comput(P2,s,l)) = halt SCMPDS;
CurInstr(P1,Comput(P1,s,l))
= CurInstr(P2,Comput(P2,s,l))
by A1,A2,Th5;
hence LifeSpan(P1,s) <= l by A4,A6,EXTPRO_1:def 15;
end;
CurInstr(P2,Comput(P2,s,LifeSpan(P1,s)))
= CurInstr(P1,Comput(P1,s,LifeSpan(P1,s))) by A1,A2,Th5
.= halt SCMPDS by A4,EXTPRO_1:def 15;
hence
A7: LifeSpan(P1,s) = LifeSpan(P2,s) by A5,A3,EXTPRO_1:def 15;
P2 halts_on s by A2,SCMPDS_4:def 7;
then
A8: Result(P2,s) = Comput(P2,s,LifeSpan(P1,s))
by A7,EXTPRO_1:23;
P1 halts_on s by A1,SCMPDS_4:def 7;
then
Result(P1,s) = Comput(P1,s,LifeSpan(P1,s))
by EXTPRO_1:23;
hence thesis by A1,A2,A8,Th5;
end;
::$CT
theorem Th7:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS, J being Program of SCMPDS
st stop I c= P
for m st m <= LifeSpan(P,s)
holds Comput(P,s,m) = Comput(P+*(I ';' J),s,m)
proof
let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS, J be Program of SCMPDS;
set SI=stop I;
defpred X[Nat] means $1 <= LifeSpan(P,s) implies
Comput(P,s,$1) = Comput(P+*(I ';' J),s,$1);
assume
A1: SI c= P;
then
A2: P halts_on s by SCMPDS_4:def 7;
A3: for m st X[m] holds X[m+1]
proof
dom(I ';' J) = dom I \/ dom Shift(J, card I) by FUNCT_4:def 1;
then
A4: dom I c= dom(I ';' J) by XBOOLE_1:7;
let m;
assume
A5: m <= LifeSpan(P,s) implies Comput(P,s,m) = Comput(P+*(I ';' J),s,m);
assume
A6: m+1 <= LifeSpan(P,s);
A7: Comput(P+*(I ';' J),s,m+1)
= Following(P+*(I ';' J),Comput(P+*(I ';' J),s,m)) by EXTPRO_1:3;
A8: Comput(P,s,m+1) = Following(P,Comput(P,s,m)) by EXTPRO_1:3;
A9: I ';' J c= P+*(I ';' J) by FUNCT_4:25;
A10: IC Comput(P,s,m) in dom SI by A1,SCMPDS_4:def 6;
A11: P/.IC Comput(P,s,m) = P.IC Comput(P,s,m) by PBOOLE:143;
A12: CurInstr(P,Comput(P,s,m)) = SI.IC (Comput(P,s,m))
by A10,A11,A1,GRFUNC_1:2;
A13: (P+*(I ';' J))/.IC Comput(P+*(I ';' J),s,m)
= (P+*(I ';' J)).IC Comput(P+*(I ';' J),s,m) by PBOOLE:143;
m < LifeSpan(P,s) by A6,NAT_1:13;
then SI.IC(Comput(P,s,m)) <> halt SCMPDS by A2,A12,EXTPRO_1:def 15;
then
A14: IC Comput(P,s,m) in dom I by A10,COMPOS_1:51;
CurInstr(P,Comput(P,s,m))
=I.IC (Comput(P,s,m)) by A12,A14,AFINSQ_1:def 3
.=(I ';' J).IC(Comput(P,s,m))
by A14,AFINSQ_1:def 3
.= CurInstr(P+*(I ';' J),Comput(P+*(I ';' J),s,m))
by A6,A9,A14,A4,A13,A5,GRFUNC_1:2,NAT_1:13;
hence thesis by A5,A6,A8,A7,NAT_1:13;
end;
A15: X[0];
thus for m holds X[m] from NAT_1:sch 2(A15,A3);
end;
theorem Th8:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS, J being Program of SCMPDS
st stop I c= P
for m st m <= LifeSpan(P,s)
holds Comput(P,s,m) = Comput(P+*stop(I ';' J), s,m)
proof
let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS, J be Program of SCMPDS;
assume
A1: stop I c= P;
set sIJ=stop (I ';' J), SS=Stop SCMPDS;
let m;
assume
A2: m <= LifeSpan(P,s);
P +* sIJ = P +* (I ';' (J ';' SS)) by AFINSQ_1:27;
hence thesis by A1,A2,Th7;
end;
Lm2: Load (DataLoc(0,0):=0) is parahalting
proof
set ii= DataLoc(0,0):=0, m0= stop Load ii;
let s be 0-started State of SCMPDS;
let P such that
A1: m0 c= P;
A2: m0 = Macro ii;
take 1;
IC Comput(P,s,1) in NAT;
hence IC Comput(P,s,1) in dom P by PARTFUN1:def 2;
A3: IC s = 0 by MEMSTR_0:def 11;
then
A4: IC Exec(ii, s) = 0+1 by SCMPDS_2:45;
1 in dom m0 by A2,COMPOS_1:57;
then m0. 1 = P. 1 by A1,GRFUNC_1:2;
then
A5: P. 1 = halt SCMPDS by A2,COMPOS_1:59;
0 in dom m0 by A2,COMPOS_1:57;
then
A6: m0. 0 = P. 0 by A1,GRFUNC_1:2;
A7: P/.IC s = P.IC s by PBOOLE:143;
Comput(P,s,0+1) = Following(P,Comput(P,s,0)) by EXTPRO_1:3
.= Following(P,s)
.= Exec(ii,s) by A3,A6,A7,A2,COMPOS_1:58;
hence thesis by A5,A4,PBOOLE:143;
end;
begin :: Non halting instrutions and parahalting instrutions
definition
::$CD
let i be Instruction of SCMPDS;
attr i is parahalting means
:Def1:
Load i is parahalting;
end;
registration
cluster No-StopCode shiftable parahalting for Instruction of SCMPDS;
existence
proof
take i=DataLoc(0,0):=0;
InsCode i=2 by SCMPDS_2:14;
then i <> halt SCMPDS;
hence i is No-StopCode;
thus thesis by Lm2;
end;
end;
theorem
goto k1 is No-StopCode
proof
A1: InsCode goto k1 = 14 by SCMPDS_2:12;
thus goto k1 <> halt the InstructionsF of SCMPDS by A1;
end;
registration
let a;
cluster return a -> No-StopCode;
coherence
proof
set i=return a;
InsCode i=1 by SCMPDS_2:13;
then i <> halt SCMPDS;
hence thesis;
end;
end;
registration
let a,k1;
cluster a := k1 -> No-StopCode;
coherence
proof
set i=a:=k1;
InsCode i=2 by SCMPDS_2:14;
then i <> halt SCMPDS;
hence thesis;
end;
cluster saveIC(a,k1) -> No-StopCode;
coherence
proof
set i=saveIC(a,k1);
InsCode i=3 by SCMPDS_2:15;
then i <> halt SCMPDS;
hence thesis;
end;
end;
registration
let a,k1,k2;
cluster (a,k1)<>0_goto k2 -> No-StopCode;
coherence
proof
set i=(a,k1)<>0_goto k2;
InsCode i=4 by SCMPDS_2:16;
then i <> halt SCMPDS;
hence thesis;
end;
cluster (a,k1)<=0_goto k2 -> No-StopCode;
coherence
proof
set i=(a,k1)<=0_goto k2;
InsCode i=5 by SCMPDS_2:17;
then i <> halt SCMPDS;
hence thesis;
end;
cluster (a,k1)>=0_goto k2 -> No-StopCode;
coherence
proof
set i=(a,k1)>=0_goto k2;
InsCode i=6 by SCMPDS_2:18;
then i <> halt SCMPDS;
hence thesis;
end;
cluster (a,k1) := k2 -> No-StopCode;
coherence
proof
set i=(a,k1) := k2;
InsCode i=7 by SCMPDS_2:19;
then i <> halt SCMPDS;
hence thesis;
end;
end;
registration
let a,k1,k2;
cluster AddTo(a,k1,k2) -> No-StopCode;
coherence
proof
set i=AddTo(a,k1,k2);
InsCode i=8 by SCMPDS_2:20;
then i <> halt SCMPDS;
hence thesis;
end;
end;
registration
let a,b,k1,k2;
cluster AddTo(a,k1,b,k2) -> No-StopCode;
coherence
proof
set i=AddTo(a,k1,b,k2);
InsCode i=9 by SCMPDS_2:21;
then i <> halt SCMPDS;
hence thesis;
end;
cluster SubFrom(a,k1,b,k2) -> No-StopCode;
coherence
proof
set i=SubFrom(a,k1,b,k2);
InsCode i=10 by SCMPDS_2:22;
then i <> halt SCMPDS;
hence thesis;
end;
cluster MultBy(a,k1,b,k2) -> No-StopCode;
coherence
proof
set i=MultBy(a,k1,b,k2);
InsCode i=11 by SCMPDS_2:23;
then i <> halt SCMPDS;
hence thesis;
end;
cluster Divide(a,k1,b,k2) -> No-StopCode;
coherence
proof
set i=Divide(a,k1,b,k2);
InsCode i=12 by SCMPDS_2:24;
then i <> halt SCMPDS;
hence thesis;
end;
cluster (a,k1) := (b,k2) -> No-StopCode;
coherence
proof
set i=(a,k1) := (b,k2);
InsCode i=13 by SCMPDS_2:25;
then i <> halt SCMPDS;
hence thesis;
end;
end;
registration
cluster halt SCMPDS -> parahalting;
coherence
proof
Stop SCMPDS=Load halt SCMPDS;
hence thesis;
end;
end;
registration
let i be parahalting Instruction of SCMPDS;
cluster Load i -> parahalting for Program of SCMPDS;
coherence by Def1;
end;
:: ??? is sequential
Lm3: (for s holds Exec(i,s).IC SCMPDS = IC s + 1)
implies Load i is parahalting
proof
assume
A1: for s holds Exec(i,s).IC SCMPDS = IC s + 1;
set m0= stop Load i;
let t be 0-started State of SCMPDS;
A2: m0 = Macro i;
let Q such that
A3: m0 c= Q;
take 1;
IC Comput(Q,t,1) in NAT;
hence IC Comput(Q,t,1) in dom Q by PARTFUN1:def 2;
A4: IC t = 0 by MEMSTR_0:def 11;
then
A5: IC Exec(i, t) = 0+1 by A1;
1 in dom m0 by A2,COMPOS_1:57;
then m0. 1 = Q. 1 by A3,GRFUNC_1:2;
then
A6: Q. 1 = halt SCMPDS by A2,COMPOS_1:59;
0 in dom m0 by A2,COMPOS_1:57;
then
A7: m0. 0 = Q. 0 by A3,GRFUNC_1:2;
A8: Q/.IC t = Q.IC t by PBOOLE:143;
Comput(Q,t,0+1) = Following(Q,Comput(Q,t,0)) by EXTPRO_1:3
.= Following(Q,t)
.= Exec(i,t) by A4,A7,A8,A2,COMPOS_1:58;
hence thesis by A5,A6,PBOOLE:143;
end;
registration
let a,k1;
cluster a := k1 -> parahalting;
coherence
proof
set i= a:=k1;
for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:45;
then Load i is parahalting by Lm3;
hence thesis;
end;
end;
registration
let a,k1,k2;
cluster (a,k1) := k2 -> parahalting;
coherence
proof
set i= (a,k1) := k2;
for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:46;
then Load i is parahalting by Lm3;
hence thesis;
end;
cluster AddTo(a,k1,k2) -> parahalting;
coherence
proof
set i= AddTo(a,k1,k2);
for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:48;
then Load i is parahalting by Lm3;
hence thesis;
end;
end;
registration
let a,b,k1,k2;
cluster AddTo(a,k1,b,k2) -> parahalting;
coherence
proof
set i= AddTo(a,k1,b,k2);
for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:49;
then Load i is parahalting by Lm3;
hence thesis;
end;
cluster SubFrom(a,k1,b,k2) -> parahalting;
coherence
proof
set i= SubFrom(a,k1,b,k2);
for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:50;
then Load i is parahalting by Lm3;
hence thesis;
end;
cluster MultBy(a,k1,b,k2) -> parahalting;
coherence
proof
set i= MultBy(a,k1,b,k2);
for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:51;
then Load i is parahalting by Lm3;
hence thesis;
end;
cluster Divide(a,k1,b,k2) -> parahalting;
coherence
proof
set i= Divide(a,k1,b,k2);
for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:52;
then Load i is parahalting by Lm3;
hence thesis;
end;
cluster (a,k1) := (b,k2) -> parahalting;
coherence
proof
set i= (a,k1) := (b,k2);
for s holds Exec(i,s).IC SCMPDS = IC s + 1 by SCMPDS_2:47;
then Load i is parahalting by Lm3;
hence thesis;
end;
end;
theorem Th10:
InsCode i =1 implies i is not parahalting
proof
consider s such that
A1: for a holds s.a = 2 by SCMPDS_2:61;
set P = the Instruction-Sequence of SCMPDS;
assume InsCode i=1;
then consider a such that
A2: i = return a by SCMPDS_2:27;
assume i is parahalting;
then reconsider Li = Load i as parahalting Program of SCMPDS;
set pi= Macro i;
set s1=Initialize s, P1= P+*pi;
s1.DataLoc(s1.a,RetIC)=s.DataLoc(s1.a,RetIC) by Th4
.=2 by A1;
then
A3: Exec(i, s1).IC SCMPDS =|.2.|+2 by A2,SCMPDS_2:58
.= 2+2 by ABSVALUE:def 1
.= 4;
set C1=Comput(P1,s1,1);
stop Li c= P1 by FUNCT_4:25;
then
A4: IC C1 in dom pi by SCMPDS_4:def 6;
0 in dom pi by COMPOS_1:57;
then
A5: P1. 0= pi. 0 by FUNCT_4:13
.=i by COMPOS_1:58;
A6: card pi = 2 by COMPOS_1:56;
A7: P1/.IC s1 = P1.IC s1 by PBOOLE:143;
Comput(P1,s1,0+1) = Following(P1,Comput(P1,s1,0)) by EXTPRO_1:3
.= Following(P1,s1)
.= Exec(i, s1) by A5,A7,MEMSTR_0:47;
hence contradiction by A3,A4,A6,AFINSQ_1:66;
end;
registration
cluster parahalting shiftable halt-free for Program of SCMPDS;
existence
proof
set ii=DataLoc(0,0):=0;
take II=Load ii;
now
let x be Nat;
assume
x in dom II;
then x in { 0} by FUNCOP_1:13;
then x= 0 by TARSKI:def 1;
then
A1: II.x=ii;
InsCode ii=2 by SCMPDS_2:14;
hence II.x <> halt SCMPDS by A1;
end;
hence thesis;
end;
end;
registration
let I,J be halt-free Program of SCMPDS;
cluster I ';' J -> halt-free;
coherence
proof
set IJ=I ';' J;
set D = {n+card I where n is Nat: n in dom J };
dom Shift(J,card I) = D by VALUED_1:def 12;
then
A1: dom IJ = dom I \/ D by FUNCT_4:def 1;
let x be Nat such that
A2: x in dom IJ;
per cases by A2,A1,XBOOLE_0:def 3;
suppose
A3: x in dom I;
then I.x=IJ.x by AFINSQ_1:def 3;
hence IJ.x<>halt SCMPDS by A3,COMPOS_1:def 27;
end;
suppose
x in D;
then consider n being Nat such that
A4: x = n+card I and
A5: n in dom J;
J. n =IJ.x by A4,A5,AFINSQ_1:def 3;
hence IJ.x<>halt SCMPDS by A5,COMPOS_1:def 27;
end;
end;
end;
registration :: musi byc do najmniej jedna instrukcja rozna of halt
:: nie moze to byc np. Trivial-AMI
let i be No-StopCode Instruction of SCMPDS;
cluster Load i -> halt-free;
coherence
proof
set p=Load i;
now
let x be Nat;
assume
x in dom p;
then x = 0 by COMPOS_1:50;
then p.x=i;
hence p.x <>halt SCMPDS by COMPOS_0:def 12;
end;
hence thesis;
end;
end;
registration
let i be No-StopCode Instruction of SCMPDS, J be halt-free Program of
SCMPDS;
cluster i ';' J -> halt-free;
coherence;
end;
registration
let I be halt-free Program of SCMPDS, j be No-StopCode Instruction of
SCMPDS;
cluster I ';' j -> halt-free;
coherence;
end;
registration
let i,j be No-StopCode Instruction of SCMPDS;
cluster i ';' j -> halt-free;
coherence;
end;
theorem Th11:
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS st stop I c= P
holds IC Comput(P, s,LifeSpan(P +* stop I,s)) = card I
proof
let s be 0-started State of SCMPDS;
let I be parahalting halt-free Program of SCMPDS;
set Css= Comput(P, s,LifeSpan(P,s));
reconsider n = IC Css as Nat;
assume
A1: stop I c= P;
then
A2: P halts_on s by SCMPDS_4:def 7;
A3: P +* stop I = P by A1,FUNCT_4:98;
I c= stop I by AFINSQ_1:74;
then
A4: I c= P by A1;
now
assume
A5: IC Css in dom I;
then I.IC Css=P.IC Css by A4,GRFUNC_1:2
.=CurInstr(P,Css) by PBOOLE:143
.=halt SCMPDS by A2,EXTPRO_1:def 15;
hence contradiction by A5,COMPOS_1:def 27;
end;
then
A6: n >= card I by AFINSQ_1:66;
A7: card stop I =card I + 1 by Lm1,AFINSQ_1:17;
IC Css in dom stop(I) by A1,SCMPDS_4:def 6;
then n < card I + 1 by A7,AFINSQ_1:66;
then n <= card I by NAT_1:13;
hence thesis by A3,A6,XXREAL_0:1;
end;
theorem Th12:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS,k be Nat st
k < LifeSpan(P +* stop I,s)
holds IC Comput(P +* stop I,s,k) in dom I
proof let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS,k be Nat;
set ss= s, PP = P +* stop I, m=LifeSpan(PP,ss);
set Sk= Comput(PP, ss,k), Ik=IC Sk;
A1: stop I c= PP by FUNCT_4:25;
then
A2: PP halts_on ss by SCMPDS_4:def 7;
reconsider n = Ik as Nat;
A3: Ik in dom stop(I) by A1,SCMPDS_4:def 6;
A4: stop I c= PP by FUNCT_4:25;
assume
A5: k < m;
A6: now
assume
A7: n = card I;
A8: 0 in dom Stop SCMPDS by COMPOS_1:3;
A9: (Stop SCMPDS). 0 = halt SCMPDS;
CurInstr(PP,Sk) =PP.Ik by PBOOLE:143
.=(stop I).(0+n) by A3,A4,GRFUNC_1:2
.=halt SCMPDS by A7,A9,A8,AFINSQ_1:def 3;
hence contradiction by A5,A2,EXTPRO_1:def 15;
end;
card stop I=card I + 1 by Lm1,AFINSQ_1:17;
then n < card I + 1 by A3,AFINSQ_1:66;
then n <= card I by INT_1:7;
then n < card I by A6,XXREAL_0:1;
hence thesis by AFINSQ_1:66;
end;
theorem Th13:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS,k be Nat st
I c= P & k <= LifeSpan(P +* stop I,s)
holds Comput(P, s,k) = Comput(P +* stop I,s,k)
proof
let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS,k be Nat;
set m=LifeSpan(P +* stop I,s);
assume that
A1: I c= P and
A2: k <= m;
set s2 = s, P2 = P +* stop I;
defpred P[Nat] means
$1 <= m implies Comput(P,s,$1) = Comput(P2,s2,$1);
A3: P = P +* I by A1,FUNCT_4:98;
A4: now
let k be Nat;
assume
A5: P[k];
now
A6: Comput(P2,s2,k+1) = Following(P2,Comput(P2,s2,k)) by EXTPRO_1:3;
A7: Comput(P,s,k+1) = Following(P,Comput(P,s,k)) by EXTPRO_1:3;
A8: k < k+1 by XREAL_1:29;
assume
A9: k+1 <= m;
then
A10: k < m by A8,XXREAL_0:2;
then IC Comput(P2,s2,k) in dom I by Th12;
then
A11: IC Comput(P2,s2,k) in dom (stop I) by FUNCT_4:12;
A12: IC Comput(P2,s2,k) in dom I by A10,Th12;
CurInstr(P,Comput(P,s,k))
= P.IC Comput(P2,s2,k) by A5,A9,A8,PBOOLE:143,XXREAL_0:2
.= I.IC Comput(P2,s2,k) by A3,A10,Th12,FUNCT_4:13
.= (stop I).IC Comput(P2,s2,k) by A12,AFINSQ_1:def 3
.= (P +* stop I).IC Comput(P2,s2,k) by A11,FUNCT_4:13
.= CurInstr(P2,Comput(P2,s2,k)) by PBOOLE:143;
hence Comput(P,s,k+1) = Comput(P2,s2,k+1)
by A5,A9,A8,A7,A6,XXREAL_0:2;
end;
hence P[k+1];
end;
A13: P[0];
for k be Nat holds P[k] from NAT_1:sch 2(A13,A4);
hence thesis by A2;
end;
theorem Th14:
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS st I c= P
holds IC Comput(P,s,LifeSpan(P +* stop I,s)) = card I
proof
let s be 0-started State of SCMPDS;
let I be parahalting halt-free Program of SCMPDS;
set PP = P +* stop I, m=LifeSpan(PP,s);
A1: stop I c= PP by FUNCT_4:25;
A2: stop I +* PP = PP & PP +* stop I = PP by A1,FUNCT_4:97;
assume I c= P;
hence IC Comput(P,s,m) = IC Comput(PP,s,m) by Th13
.= card I by Th11,A2,FUNCT_4:25;
end;
theorem Th15:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS st I c= P
holds CurInstr(P,Comput(P, s,LifeSpan(P +* stop I,s))) = halt SCMPDS
or IC Comput(P, s,LifeSpan(P +* stop I,s)) = card I
proof
let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS;
set PP = P+* stop I, m=LifeSpan(PP,s);
set s1=Comput(P,s,m),
s2= Comput(PP, s,LifeSpan(PP +* stop I,Initialize s)),
Ik = IC s2;
A1: stop I c= PP by FUNCT_4:25;
then
A2: PP halts_on s by SCMPDS_4:def 7;
reconsider n = Ik as Nat;
A3: Ik in dom stop(I) by A1,SCMPDS_4:def 6;
A4: Initialize s = s by MEMSTR_0:44;
card stop I = card I + 1 by Lm1,AFINSQ_1:17;
then n < card I + 1 by A3,AFINSQ_1:66;
then
A5: n <= card I by INT_1:7;
A6: stop I c= PP by FUNCT_4:25;
assume
A7: I c= P;
then
A8: IC s1 =Ik by Th13,A4;
now
per cases by A5,XXREAL_0:1;
case
n < card I;
then
A9: n in dom I by AFINSQ_1:66;
thus halt SCMPDS
= CurInstr(PP,s2) by A2,A4,EXTPRO_1:def 15
.=PP.Ik by PBOOLE:143
.=(stop I).Ik by A3,A6,GRFUNC_1:2
.=I.Ik by A9,AFINSQ_1:def 3
.=P.IC s1 by A7,A8,A9,GRFUNC_1:2
.=CurInstr(P,s1) by PBOOLE:143;
end;
case n = card I;
hence IC s1 = card I by A7,Th13,A4;
end;
end;
hence thesis;
end;
theorem Th16:
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,k being Nat
st I c= P & k < LifeSpan(P +* stop I,s)
holds CurInstr(P,Comput(P,s,k)) <> halt SCMPDS
proof
let s be 0-started State of SCMPDS;
let I be parahalting halt-free Program of SCMPDS,k be Nat;
set PI = P +* stop I, s1= Comput(P, s,k), s2= Comput(PI, s,k);
assume that
A1: I c= P and
A2: k < LifeSpan(PI,s);
A3: IC s2 in dom I by A2,Th12;
A4: P/.IC s1 = P.IC s1 by PBOOLE:143;
CurInstr(P,s1)=P.IC s2 by A4,A1,A2,Th13
.=I.IC s2 by A1,A3,GRFUNC_1:2;
hence thesis by A3,COMPOS_1:def 27;
end;
theorem Th17:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS,
J being Program of SCMPDS, k being Nat
st k <= LifeSpan(P +* stop I,s)
holds Comput(P +* stop I,s,k) = Comput(P+*(I ';' J),s,k)
proof
let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS,J be Program of SCMPDS,
k be Nat;
set spI= stop I, P1 = P +* spI, P2 = P +* (I ';' J);
set n=LifeSpan(P1,s);
defpred X[Nat] means
$1 <= n implies Comput(P1,s,$1) = Comput(P2,s,$1);
A1: for n being Nat st X[n] holds X[n+1]
proof
let m be Nat;
assume
A2: m <= n implies Comput(P1,s,m) = Comput(P2,s,m);
A3: Comput(P2,s,m+1) = Following(P2,Comput(P2,s,m)) by EXTPRO_1:3;
spI c= P1 by FUNCT_4:25;
then
A4: IC Comput(P1,s,m) in dom spI by SCMPDS_4:def 6;
A5: Comput(P1,s,m+1) = Following(P1,Comput(P1,s,m)) by EXTPRO_1:3;
assume
A6: m+1 <= n;
A7: m < n by A6,NAT_1:13;
then IC Comput(P1,s,m) in dom I by Th12;
then
A8: IC Comput(P1,s,m) in dom (I ';' J) by FUNCT_4:12;
A9: IC Comput(P1,s,m) in dom I by A7,Th12;
CurInstr(P1,Comput(P1,s,m))
= P1.IC Comput(P1,s,m) by PBOOLE:143
.= spI.IC Comput(P1,s,m) by A4,FUNCT_4:13
.= I.IC Comput(P1,s,m) by A9,AFINSQ_1:def 3
.= (I ';' J).IC Comput(P1,s,m) by A9,AFINSQ_1:def 3
.= P2.IC Comput(P1,s,m) by A8,FUNCT_4:13
.=CurInstr(P2,Comput(P2,s,m)) by A6,A2,NAT_1:13,PBOOLE:143;
hence thesis by A2,A6,A5,A3,NAT_1:13;
end;
A10: X[0];
for k being Nat holds X[k] from NAT_1:sch 2(A10, A1);
hence thesis;
end;
theorem Th18:
for s being 0-started State of SCMPDS
for I being parahalting Program of SCMPDS,J being Program of SCMPDS,
k being Nat st k <= LifeSpan(P +* stop I,s)
holds Comput(P +* stop I, s,k) = Comput(P+*stop(I ';' J),s,k)
proof
let s be 0-started State of SCMPDS;
let I be parahalting Program of SCMPDS,J be Program of SCMPDS,
k be Nat;
A1: stop (I ';' J) = (I ';' (J ';' Stop SCMPDS)) by AFINSQ_1:27;
thus thesis by A1,Th17;
end;
registration
let I be parahalting Program of SCMPDS,
J be parahalting shiftable Program of SCMPDS;
cluster I ';' J -> parahalting for Program of SCMPDS;
coherence
proof
let p be Program of SCMPDS such that
A1: p = I ';' J;
let s be 0-started State of SCMPDS;
let P;
set sIJ = stop p;
set spJ = stop J, s1 = Initialize s,
P1 = P +* stop I,
m1 = LifeSpan(P1,s1),
s3 = Initialize Comput(P1, s1,m1),
P3 = P1 +* spJ,
m3 = LifeSpan(P3,s3),
D = SCM-Data-Loc;
A2: spJ c= P3 by FUNCT_4:25;
then
A3: P3 halts_on s3 by SCMPDS_4:def 7;
A4: DataPart Comput(P1,s1,m1) = DataPart s3 by MEMSTR_0:45;
A5: I c= sIJ by A1,Th1;
set s4 = Comput(P,s,m1), P4=P;
assume
A6: sIJ c= P;
A7: p c= sIJ by AFINSQ_1:74;
A8: s = Initialize s by MEMSTR_0:44;
P+*(I ';' J) = P by A7,A1,A6,FUNCT_4:98,XBOOLE_1:1;
then
A9: DataPart s4 = DataPart s3 by A4,A8,Th17;
per cases by A6,A5,Th15,A8,XBOOLE_1:1;
suppose
A10: CurInstr(P,s4) = halt SCMPDS;
take m1;
IC Comput(P,s,m1) in NAT;
hence IC Comput(P,s,m1) in dom P by PARTFUN1:def 2;
thus thesis by A10;
end;
suppose
A11: IC s4 = card I;
reconsider m = m1 + m3 as Nat;
take m;
IC Comput(P,s,m) in NAT;
hence IC Comput(P,s,m) in dom P by PARTFUN1:def 2;
A12: Comput(P,s,m1+m3) = Comput(P,Comput(P,s,m1),m3) by EXTPRO_1:4;
sIJ = I ';' (J ';' Stop SCMPDS) by A1,AFINSQ_1:27
.= I +* Shift(spJ, card I);
then Shift(spJ, card I) c= sIJ by FUNCT_4:25;
then
A13: Shift(spJ, card I) c= P4 by A6;
CurInstr(P3,Comput(P3,s3,m3)) = CurInstr(P,Comput(P,s,m1+m3))
by A12,A2,A9,A11,A13,SCMPDS_4:29;
hence thesis by A3,EXTPRO_1:def 15;
end;
end;
end;
registration
let i be parahalting Instruction of SCMPDS, J be parahalting shiftable
Program of SCMPDS;
cluster i ';' J -> parahalting;
coherence;
end;
registration
let I be parahalting Program of SCMPDS, j be parahalting shiftable
Instruction of SCMPDS;
cluster I ';' j -> parahalting;
coherence;
end;
registration
let i be parahalting Instruction of SCMPDS, j be parahalting shiftable
Instruction of SCMPDS;
cluster i ';' j -> parahalting;
coherence;
end;
theorem Th19:
for s being State of SCMPDS, s1 being 0-started State of SCMPDS,
J being parahalting shiftable Program of SCMPDS
st stop J c= P & s = Comput(P1 +* stop J, s1,m)
holds Exec(CurInstr(P,s),IncIC(s,n)) = IncIC(Following(P,s),n)
proof
let s be State of SCMPDS, s1 be 0-started State of SCMPDS,
J be parahalting shiftable Program of SCMPDS;
set pJ=stop J, s2=s1,
P2 = P1 +* pJ;
set i = CurInstr(P,s), ss=s +* Start-At(IC s + n,SCMPDS);
reconsider k = IC s as Element of NAT;
reconsider Nl=IC s + 1 as Element of NAT;
A1: IC ss + 1 = (k + n + 1) by FUNCT_4:113
.= IC (Exec(i, s) +*Start-At (Nl + n,SCMPDS)) by FUNCT_4:113;
assume
A2: pJ c= P;
assume
A3: s=Comput(P2,s2,m);
pJ c= P2 by FUNCT_4:25;
then
A4: IC s in dom pJ by A3,SCMPDS_4:def 6;
reconsider n1 = IC s as Nat;
set IEn=IC Exec(i,s)+n;
A5: IC ss = IC s + n by FUNCT_4:113;
A6: P/.IC s = P.IC s by PBOOLE:143;
A7: i=pJ.(n1) by A4,A6,A2,GRFUNC_1:2;
then
A8: InsCode i <> 1 by A4,SCMPDS_4:def 9;
A9: i valid_at n1 by A4,A7,SCMPDS_4:def 9;
A10: InsCode i <> 3 by A4,A7,SCMPDS_4:def 9;
InsCode i <= 14 by SCMPDS_2:6;
then InsCode i = 0 or ... or InsCode i = 14;
then per cases by A8,A10;
suppose
A11: InsCode i = 0;
A12: Following(P,s) = s by A11,SCMPDS_2:86;
thus Exec(CurInstr(P,s),IncIC(s,n)) = IncIC(s,n) by A11,SCMPDS_2:86
.= IncIC(Following(P,s),n) by A12;
end;
suppose
InsCode i = 14;
then consider k1 such that
A13: i = goto k1 and
A14: n1+k1 >= 0 by A9;
A15: IC Exec(i,s) =ICplusConst(s,k1) by A13,SCMPDS_2:54;
A16: now
let b;
thus Exec(i, ss).b= ss.b by A13,SCMPDS_2:54
.= s.b by SCMPDS_3:6
.= Exec(i, s).b by A13,SCMPDS_2:54
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
IC Exec(i, ss) =ICplusConst(ss,k1) by A13,SCMPDS_2:54
.=IEn by A5,A14,A15,SCMPDS_4:27
.= IC (IncIC(Exec(i,s),n)) by FUNCT_4:113;
hence thesis by A16,SCMPDS_2:44;
end;
suppose
InsCode i = 2;
then consider a,k1 such that
A17: i = a := k1 by SCMPDS_2:28;
A18: now
let b;
per cases;
suppose
A19: a = b;
hence Exec(i, ss).b = k1 by A17,SCMPDS_2:45
.= Exec(i,s).b by A17,A19,SCMPDS_2:45
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
suppose
A20: a <> b;
hence Exec(i, ss).b = ss.b by A17,SCMPDS_2:45
.= s.b by SCMPDS_3:6
.= Exec(i, s).b by A17,A20,SCMPDS_2:45
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
end;
IC Exec(i, s) = Nl by A17,SCMPDS_2:45;
then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n))
by A1,A17,SCMPDS_2:45;
hence thesis by A18,SCMPDS_2:44;
end;
suppose
InsCode i = 4;
then consider a,k1,k2 such that
A21: i = (a,k1)<>0_goto k2 and
A22: n1+k2 >= 0 by A9;
A23: now
per cases;
suppose
A24: s.DataLoc(s.a,k1) <> 0;
then
A25: IC Exec(i,s) =ICplusConst(s,k2) by A21,SCMPDS_2:55;
ss.DataLoc(s.a,k1) <> 0 by A24,SCMPDS_3:6;
then ss.DataLoc(ss.a,k1) <> 0 by SCMPDS_3:6;
hence IC Exec(i, ss) =ICplusConst(ss,k2) by A21,SCMPDS_2:55
.=IEn by A5,A22,A25,SCMPDS_4:27
.= IC (IncIC(Exec(i,s),n)) by FUNCT_4:113;
end;
suppose
A26: s.DataLoc(s.a,k1) = 0;
then ss.DataLoc(s.a,k1) = 0 by SCMPDS_3:6;
then
A27: ss.DataLoc(ss.a,k1) = 0 by SCMPDS_3:6;
IC Exec(i, s) = Nl by A21,A26,SCMPDS_2:55;
hence IC Exec(i,ss) = IC (IncIC(Exec(i,s),n))
by A1,A21,A27,SCMPDS_2:55;
end;
end;
now
let b;
thus Exec(i, ss).b= ss.b by A21,SCMPDS_2:55
.= s.b by SCMPDS_3:6
.= Exec(i, s).b by A21,SCMPDS_2:55
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
hence thesis by A23,SCMPDS_2:44;
end;
suppose
InsCode i = 5;
then consider a,k1,k2 such that
A28: i = (a,k1)<=0_goto k2 and
A29: n1+k2 >= 0 by A9;
A30: now
per cases;
suppose
A31: s.DataLoc(s.a,k1) <= 0;
then
A32: IC Exec(i,s) =ICplusConst(s,k2) by A28,SCMPDS_2:56;
ss.DataLoc(s.a,k1) <= 0 by A31,SCMPDS_3:6;
then ss.DataLoc(ss.a,k1) <= 0 by SCMPDS_3:6;
hence IC Exec(i, ss) =ICplusConst(ss,k2) by A28,SCMPDS_2:56
.=IEn by A5,A29,A32,SCMPDS_4:27
.= IC (IncIC(Exec(i,s),n)) by FUNCT_4:113;
end;
suppose
A33: s.DataLoc(s.a,k1) > 0;
then ss.DataLoc(s.a,k1) > 0 by SCMPDS_3:6;
then
A34: ss.DataLoc(ss.a,k1) > 0 by SCMPDS_3:6;
IC Exec(i, s) = Nl by A28,A33,SCMPDS_2:56;
hence IC Exec(i,ss) = IC (IncIC(Exec(i,s),n))
by A1,A28,A34,SCMPDS_2:56;
end;
end;
now
let b;
thus Exec(i, ss).b= ss.b by A28,SCMPDS_2:56
.= s.b by SCMPDS_3:6
.= Exec(i, s).b by A28,SCMPDS_2:56
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
hence thesis by A30,SCMPDS_2:44;
end;
suppose
InsCode i = 6;
then consider a,k1,k2 such that
A35: i = (a,k1)>=0_goto k2 and
A36: n1+k2 >= 0 by A9;
A37: now
per cases;
suppose
A38: s.DataLoc(s.a,k1) >= 0;
then
A39: IC Exec(i,s) =ICplusConst(s,k2) by A35,SCMPDS_2:57;
ss.DataLoc(s.a,k1) >= 0 by A38,SCMPDS_3:6;
then ss.DataLoc(ss.a,k1) >= 0 by SCMPDS_3:6;
hence IC Exec(i, ss) =ICplusConst(ss,k2) by A35,SCMPDS_2:57
.=IEn by A5,A36,A39,SCMPDS_4:27
.= IC (IncIC(Exec(i,s),n)) by FUNCT_4:113;
end;
suppose
A40: s.DataLoc(s.a,k1) < 0;
then ss.DataLoc(s.a,k1) < 0 by SCMPDS_3:6;
then
A41: ss.DataLoc(ss.a,k1) < 0 by SCMPDS_3:6;
IC Exec(i, s) = Nl by A35,A40,SCMPDS_2:57;
hence IC Exec(i,ss) = IC (IncIC(Exec(i,s),n))
by A1,A35,A41,SCMPDS_2:57;
end;
end;
now
let b;
thus Exec(i, ss).b= ss.b by A35,SCMPDS_2:57
.= s.b by SCMPDS_3:6
.= Exec(i, s).b by A35,SCMPDS_2:57
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
hence thesis by A37,SCMPDS_2:44;
end;
suppose
InsCode i = 7;
then consider a,k1,k2 such that
A42: i = (a,k1) := k2 by SCMPDS_2:33;
A43: now
let b;
per cases;
suppose
A44: DataLoc(ss.a,k1) = b;
then
A45: DataLoc(s.a,k1) = b by SCMPDS_3:6;
thus Exec(i, ss).b = k2 by A42,A44,SCMPDS_2:46
.= Exec(i,s).b by A42,A45,SCMPDS_2:46
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
suppose
A46: DataLoc(ss.a,k1) <> b;
then
A47: DataLoc(s.a,k1) <> b by SCMPDS_3:6;
thus Exec(i, ss).b = ss.b by A42,A46,SCMPDS_2:46
.= s.b by SCMPDS_3:6
.= Exec(i, s).b by A42,A47,SCMPDS_2:46
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
end;
IC Exec(i, s) = Nl by A42,SCMPDS_2:46;
then IC Exec(i, ss) = IC IncIC(Exec(i,s),n) by A1,A42,SCMPDS_2:46;
hence thesis by A43,SCMPDS_2:44;
end;
suppose
InsCode i = 8;
then consider a,k1,k2 such that
A48: i = AddTo(a,k1,k2) by SCMPDS_2:34;
A49: now
let b;
per cases;
suppose
A50: DataLoc(ss.a,k1) = b;
then
A51: DataLoc(s.a,k1) = b by SCMPDS_3:6;
thus Exec(i, ss).b = ss.b + k2 by A48,A50,SCMPDS_2:48
.= s.b + k2 by SCMPDS_3:6
.= Exec(i, s).b by A48,A51,SCMPDS_2:48
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
suppose
A52: DataLoc(ss.a,k1) <> b;
then
A53: DataLoc(s.a,k1) <> b by SCMPDS_3:6;
thus Exec(i, ss).b = ss.b by A48,A52,SCMPDS_2:48
.= s.b by SCMPDS_3:6
.= Exec(i, s).b by A48,A53,SCMPDS_2:48
.= (IncIC(Exec(i,s),n)).b by SCMPDS_3:6;
end;
end;
IC Exec(i, s) = Nl by A48,SCMPDS_2:48;
then IC Exec(i, ss) = IC IncIC(Exec(i,s),n) by A1,A48,SCMPDS_2:48;
hence thesis by A49,SCMPDS_2:44;
end;
suppose
InsCode i = 9;
then consider a,b,k1,k2 such that
A54: i = AddTo(a,k1,b,k2) by SCMPDS_2:35;
A55: now
let c;
per cases;
suppose
A56: DataLoc(ss.a,k1) = c;
then
A57: DataLoc(s.a,k1) = c by SCMPDS_3:6;
A58: ss.DataLoc(ss.b,k2) =s.DataLoc(ss.b,k2) by SCMPDS_3:6
.=s.DataLoc(s.b,k2) by SCMPDS_3:6;
ss.DataLoc(ss.a,k1) =s.DataLoc(ss.a,k1) by SCMPDS_3:6
.=s.DataLoc(s.a,k1) by SCMPDS_3:6;
hence
Exec(i, ss).c = s.DataLoc(s.a,k1) + s.DataLoc(s.b,k2) by A54,A56,A58,
SCMPDS_2:49
.= Exec(i, s).c by A54,A57,SCMPDS_2:49
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
suppose
A59: DataLoc(ss.a,k1) <> c;
then
A60: DataLoc(s.a,k1) <> c by SCMPDS_3:6;
thus Exec(i, ss).c = ss.c by A54,A59,SCMPDS_2:49
.= s.c by SCMPDS_3:6
.= Exec(i, s).c by A54,A60,SCMPDS_2:49
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
end;
IC Exec(i, s) = Nl by A54,SCMPDS_2:49;
then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n)) by A1,A54,SCMPDS_2:49;
hence thesis by A55,SCMPDS_2:44;
end;
suppose
InsCode i = 10;
then consider a,b,k1,k2 such that
A61: i = SubFrom(a,k1,b,k2) by SCMPDS_2:36;
A62: now
let c;
per cases;
suppose
A63: DataLoc(ss.a,k1) = c;
then
A64: DataLoc(s.a,k1) = c by SCMPDS_3:6;
A65: ss.DataLoc(ss.b,k2) =s.DataLoc(ss.b,k2) by SCMPDS_3:6
.=s.DataLoc(s.b,k2) by SCMPDS_3:6;
ss.DataLoc(ss.a,k1) =s.DataLoc(ss.a,k1) by SCMPDS_3:6
.=s.DataLoc(s.a,k1) by SCMPDS_3:6;
hence
Exec(i, ss).c = s.DataLoc(s.a,k1) - s.DataLoc(s.b,k2) by A61,A63,A65,
SCMPDS_2:50
.= Exec(i, s).c by A61,A64,SCMPDS_2:50
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
suppose
A66: DataLoc(ss.a,k1) <> c;
then
A67: DataLoc(s.a,k1) <> c by SCMPDS_3:6;
thus Exec(i, ss).c = ss.c by A61,A66,SCMPDS_2:50
.= s.c by SCMPDS_3:6
.= Exec(i, s).c by A61,A67,SCMPDS_2:50
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
end;
IC Exec(i, s) = Nl by A61,SCMPDS_2:50;
then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n)) by A1,A61,SCMPDS_2:50;
hence thesis by A62,SCMPDS_2:44;
end;
suppose
InsCode i = 11;
then consider a,b,k1,k2 such that
A68: i = MultBy(a,k1,b,k2) by SCMPDS_2:37;
A69: now
let c;
per cases;
suppose
A70: DataLoc(ss.a,k1) = c;
then
A71: DataLoc(s.a,k1) = c by SCMPDS_3:6;
A72: ss.DataLoc(ss.b,k2) =s.DataLoc(ss.b,k2) by SCMPDS_3:6
.=s.DataLoc(s.b,k2) by SCMPDS_3:6;
ss.DataLoc(ss.a,k1) =s.DataLoc(ss.a,k1) by SCMPDS_3:6
.=s.DataLoc(s.a,k1) by SCMPDS_3:6;
hence Exec(i, ss).c = s.DataLoc(s.a,k1) * s.DataLoc(s.b,k2) by A68,A70
,A72,SCMPDS_2:51
.= Exec(i, s).c by A68,A71,SCMPDS_2:51
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
suppose
A73: DataLoc(ss.a,k1) <> c;
then
A74: DataLoc(s.a,k1) <> c by SCMPDS_3:6;
thus Exec(i, ss).c = ss.c by A68,A73,SCMPDS_2:51
.= s.c by SCMPDS_3:6
.= Exec(i, s).c by A68,A74,SCMPDS_2:51
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
end;
IC Exec(i, s) = Nl by A68,SCMPDS_2:51;
then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n)) by A1,A68,SCMPDS_2:51;
hence thesis by A69,SCMPDS_2:44;
end;
suppose
InsCode i = 12;
then consider a,b,k1,k2 such that
A75: i = Divide(a,k1,b,k2) by SCMPDS_2:38;
A76: now
let c;
A77: ss.DataLoc(ss.a,k1) =s.DataLoc(ss.a,k1) by SCMPDS_3:6
.=s.DataLoc(s.a,k1) by SCMPDS_3:6;
A78: ss.DataLoc(ss.b,k2) =s.DataLoc(ss.b,k2) by SCMPDS_3:6
.=s.DataLoc(s.b,k2) by SCMPDS_3:6;
per cases;
suppose
A79: DataLoc(ss.b,k2) = c;
then
A80: DataLoc(s.b,k2) = c by SCMPDS_3:6;
thus Exec(i, ss).c = s.DataLoc(s.a,k1) mod s.DataLoc(s.b,k2) by A75,A77
,A78,A79,SCMPDS_2:52
.= Exec(i, s).c by A75,A80,SCMPDS_2:52
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
suppose
A81: DataLoc(ss.b,k2) <> c;
then
A82: DataLoc(s.b,k2) <> c by SCMPDS_3:6;
hereby
per cases;
suppose
A83: DataLoc(ss.a,k1) <> c;
then
A84: DataLoc(s.a,k1) <> c by SCMPDS_3:6;
thus Exec(i, ss).c = ss.c by A75,A81,A83,SCMPDS_2:52
.=s.c by SCMPDS_3:6
.=Exec(i,s).c by A75,A82,A84,SCMPDS_2:52
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
suppose
A85: DataLoc(ss.a,k1) = c;
then
A86: DataLoc(s.a,k1) = c by SCMPDS_3:6;
thus Exec(i, ss).c = s.DataLoc(s.a,k1) div s.DataLoc(s.b,k2) by A75
,A77,A78,A81,A85,SCMPDS_2:52
.= Exec(i,s).c by A75,A82,A86,SCMPDS_2:52
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
end;
end;
end;
IC Exec(i, s) = Nl by A75,SCMPDS_2:52;
then IC Exec(i, ss) = IC (IncIC(Exec(i,s),n)) by A1,A75,SCMPDS_2:52;
hence thesis by A76,SCMPDS_2:44;
end;
suppose
InsCode i = 13;
then consider a,b,k1,k2 such that
A87: i = (a,k1):=(b,k2) by SCMPDS_2:39;
A88: now
let c;
per cases;
suppose
A89: DataLoc(ss.a,k1) = c;
then
A90: DataLoc(s.a,k1) = c by SCMPDS_3:6;
thus Exec(i, ss).c = ss.DataLoc(ss.b,k2) by A87,A89,SCMPDS_2:47
.=s.DataLoc(ss.b,k2) by SCMPDS_3:6
.=s.DataLoc(s.b,k2) by SCMPDS_3:6
.=Exec(i,s).c by A87,A90,SCMPDS_2:47
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
suppose
A91: DataLoc(ss.a,k1) <> c;
then
A92: DataLoc(s.a,k1) <> c by SCMPDS_3:6;
thus Exec(i,ss).c = ss.c by A87,A91,SCMPDS_2:47
.=s.c by SCMPDS_3:6
.=Exec(i,s).c by A87,A92,SCMPDS_2:47
.= (IncIC(Exec(i,s),n)).c by SCMPDS_3:6;
end;
end;
IC Exec(i, s) = Nl by A87,SCMPDS_2:47;
then IC Exec(i, ss) = IC IncIC(Exec(i,s),n) by A1,A87,SCMPDS_2:47;
hence thesis by A88,SCMPDS_2:44;
end;
end;
begin :: Computation of two consecutive program blocks
theorem
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,J being
parahalting shiftable Program of SCMPDS,k being Nat st
stop (I ';' J) c= P holds
IncIC(Comput(P +* stop I +* stop J,
Initialize Result(P +* stop I,s),k),card I)
= Comput(P+*stop(I ';' J),s,LifeSpan(P +* stop I,s)+k)
proof
let s be 0-started State of SCMPDS;
let I be parahalting halt-free Program of SCMPDS,J be parahalting
shiftable Program of SCMPDS,k be Nat;
set sIsI = s, PIPI = P +* stop I,
RI = Result(PIPI,sIsI), pJ= stop J,
RIJ = Initialize RI, PRIJ = PIPI +* pJ,
pIJ = stop (I ';' J),
sIsIJ = s, PIPIJ = P +* pIJ;
A1: pJ c= PRIJ by FUNCT_4:25;
stop I c= PIPI by FUNCT_4:25;
then
A2: PIPI halts_on sIsI by SCMPDS_4:def 7;
set s2 = Comput(PIPIJ, sIsIJ,LifeSpan(PIPI,sIsI)+0);
set s1 = RIJ +* Start-At (IC RIJ + card I,SCMPDS);
set m1 = LifeSpan(PIPI,sIsI);
A3: I c= pIJ by Th1;
assume
A4: pIJ c= P;
A5: P +* pIJ = P by A4,FUNCT_4:98;
A6: now
thus IC s1 = IC RIJ + card I by FUNCT_4:113
.= (0+card I) by FUNCT_4:113
.= IC s2 by A4,A3,Th14,A5,XBOOLE_1:1;
hereby
let a be Int_position;
A7: not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At (IC RIJ + card I,SCMPDS) by SCMPDS_4:18;
hence s1.a = RIJ.a by FUNCT_4:11
.= RI.a by A7,FUNCT_4:11
.= Comput(PIPI, sIsI,m1).a by A2,EXTPRO_1:23
.= s2.a by Th18;
end;
end;
defpred X[Nat] means
IncIC(Comput(PRIJ, RIJ,$1), card I)
= Comput(PIPIJ, sIsIJ,LifeSpan(PIPI,sIsI)+$1);
A8: pIJ c= PIPIJ by FUNCT_4:25;
A9: for k being Nat st X[k] holds X[k+1]
proof
let k be Nat;
set k1 = k+1, CRk = Comput(PRIJ, RIJ,k),
PCRk = PRIJ,
CRSk = IncIC(CRk,card I),
CIJk = Comput(PIPIJ, sIsIJ,LifeSpan(PIPI,sIsI)+k),
PCIJk = PIPIJ,
CRk1 = Comput(PRIJ, RIJ,k1
), CRSk1 = CRk1 +* Start-At (IC CRk1 + card I,SCMPDS),
CIJk1 = Comput(PIPIJ, sIsIJ,
LifeSpan(PIPI,sIsI)+k1);
assume
A10: CRSk = CIJk;
A11: CurInstr(PCRk,CRk) = CurInstr(PCIJk,CIJk)
proof
A12: CurInstr(PCIJk,CIJk) = PCIJk.IC CRSk by A10,PBOOLE:143
.= PCIJk.(IC CRk + card I) by FUNCT_4:113;
reconsider n = IC CRk as Nat;
A13: pIJ = I ';' pJ by AFINSQ_1:27;
A14: IC CRk in dom pJ by A1,SCMPDS_4:def 6;
then n < card pJ by AFINSQ_1:66;
then n+card I < card pJ + card I by XREAL_1:6;
then n+card I < card pIJ by A13,AFINSQ_1:17;
then
A15: IC CRk + card I in dom pIJ by AFINSQ_1:66;
A16: PCRk/.IC CRk = PCRk.IC CRk by PBOOLE:143;
pJ c= PCRk by FUNCT_4:25;
hence CurInstr(PCRk,CRk) =pJ.IC CRk by A14,A16,GRFUNC_1:2
.=pIJ.(IC CRk + card I) by A14,A13,AFINSQ_1:def 3
.= CurInstr(PCIJk,CIJk) by A12,A8,A15,GRFUNC_1:2;
end;
A17: Exec(CurInstr(PCIJk,CIJk), CIJk)
= IncIC(Following(PCRk,CRk), card I) by A10,Th19,A11,FUNCT_4:25;
CIJk1 = Comput(PIPIJ, sIsIJ,LifeSpan(PIPI,sIsI)+k+1);
then
A18: CIJk1 = Following(PIPIJ,CIJk) by EXTPRO_1:3;
A19: now
let a be Int_position;
thus CRSk1.a = CRk1.a by SCMPDS_3:6
.= (Following(PRIJ,CRk)).a by EXTPRO_1:3
.= CIJk1.a by A18,A17,SCMPDS_3:6;
end;
IC CRSk1 = IC CRk1 + card I by FUNCT_4:113
.= IC Following(PRIJ,CRk) + card I by EXTPRO_1:3;
then
IC CRSk1 = IC CIJk1 by A18,A17,FUNCT_4:113;
hence thesis by A19,SCMPDS_4:2;
end;
A20: X[0] by A6,SCMPDS_4:2;
for k being Nat holds X[k] from NAT_1:sch 2(A20,A9);
hence thesis;
end;
Lm4:
for I being parahalting halt-free Program of SCMPDS,
J being parahalting shiftable Program of SCMPDS,
s being 0-started State of SCMPDS st stop (I ';' J) c= P & P1= P +* stop I
holds IC Comput(P, s,LifeSpan(P1,s)) = card I &
DataPart Comput(P, s,LifeSpan(P1,s)) =
DataPart (Initialize Comput(P1,s,LifeSpan(P1,s))) &
Shift(stop J,card I) c= P &
LifeSpan(P,s) = LifeSpan(P1,s)
+ LifeSpan(P1 +* stop J,Initialize Result(P1,s))
proof
set D = SCM-Data-Loc;
let I be parahalting halt-free Program of SCMPDS,J be parahalting
shiftable Program of SCMPDS,s be 0-started State of SCMPDS;
set spJ = stop J,
sIJ = stop (I ';' J), m1 = LifeSpan(P1,s),
s3 = Initialize Comput(P1, s, m1),
P3 = P1 +* spJ;
set m3 = LifeSpan(P3,s3);
assume that
A1: sIJ c= P and
A2: P1= P +* stop I;
set s4 = Comput(P,s,m1), P4 = P;
A3: I c= sIJ by Th1;
hence
A4: IC s4 = card I by A1,A2,Th14,XBOOLE_1:1;
reconsider m = m1 + m3 as Nat;
sIJ = I ';' (J ';' Stop SCMPDS) by AFINSQ_1:27
.= I +* Shift(spJ, card I);
then
A5: Shift(spJ, card I) c= sIJ by FUNCT_4:25;
A6: spJ c= P3 by FUNCT_4:25;
then
A7: P3 halts_on s3 by SCMPDS_4:def 7;
A8: DataPart Comput(P1, s,m1) = DataPart s3 by MEMSTR_0:45;
I ';' J c= stop (I ';' J) by AFINSQ_1:74;
then P+*(I ';' J) = P by A1,FUNCT_4:98,XBOOLE_1:1;
hence
A9: DataPart s4 = DataPart s3 by A8,A2,Th17;
A10: Comput(P,s,m1+m3) = Comput(P,Comput(P,s,m1),m3) by EXTPRO_1:4;
thus
A11: Shift(spJ, card I) c= P4 by A5,A1;
then CurInstr(P3,Comput(P3,s3,m3)) = CurInstr(P,Comput(P,s,m1+m3))
by A10,A6,A4,A9,SCMPDS_4:29;
then
A12: CurInstr(P,Comput(P,s,m)) = halt SCMPDS by A7,EXTPRO_1:def 15;
A13: now
let k be Nat;
assume
m1 + k < m;
then
A14: k < m3 by XREAL_1:6;
assume
A15: CurInstr(P,Comput(P,s,m1+k)) = halt SCMPDS;
A16: Comput(P,s,m1+k) =
Comput(P,Comput(P,s,m1),k) by EXTPRO_1:4;
CurInstr(P3,Comput(P3,s3,k))
= halt SCMPDS by A15,A16,A6,A4,A9,A11,SCMPDS_4:29;
hence contradiction by A7,A14,EXTPRO_1:def 15;
end;
now
let k be Nat;
assume
A17: k < m;
per cases;
suppose k < m1;
hence CurInstr(P,Comput(P,s,k)) <> halt SCMPDS
by A2,Th16,A1,A3,XBOOLE_1:1;
end;
suppose
m1 <= k;
then consider kk being Nat such that
A18: m1 + kk = k by NAT_1:10;
thus CurInstr(P,Comput(P,s,k)) <> halt SCMPDS by A13,A17,A18;
end;
end;
then
A19: for k being Nat st CurInstr(P,Comput(P,s,k)) = halt SCMPDS
holds m <= k;
stop I c= P1 by A2,FUNCT_4:25;
then P1 halts_on s by SCMPDS_4:def 7;
then
A20: Result(P1,s) = Comput(P1,s,LifeSpan(P1,s)) by EXTPRO_1:23;
P halts_on s by A1,SCMPDS_4:def 7;
hence thesis by A20,A12,A19,EXTPRO_1:def 15;
end;
theorem Th21:
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,
J being parahalting shiftable Program of SCMPDS holds
LifeSpan(P+*stop(I ';' J), s)
= LifeSpan(P +* stop I,s) +
LifeSpan(P +* stop I +* stop J,Initialize Result(P +* stop I,s))
proof
let s be 0-started State of SCMPDS;
let I be parahalting halt-free Program of SCMPDS,J be parahalting
shiftable Program of SCMPDS;
set sI=stop I, sIJ = stop (I ';' J),
s1= s, s2= s,
P1 = P +* sIJ, P2 = P +* stop I;
A1: sIJ c= P1 by FUNCT_4:25;
set
s3=Initialize Result(P1 +* stop I,s1),
P3 = P1 +* stop I +* stop J,
s4=Initialize Result(P2,s2),
P4 = P2 +* stop J;
A2: stop I c= P2 by FUNCT_4:25;
A3: stop J c= P4 by FUNCT_4:25;
A4: stop J c= P3 by FUNCT_4:25;
A5: stop I c= P1 +* stop I by FUNCT_4:25;
then s4 = s3 by A2,Th6;
then
A6: LifeSpan(P3,s3) = LifeSpan(P4,s4) by A4,A3,Th6;
LifeSpan(P1 +* stop I,s1) =
LifeSpan(P2,s2) by A5,A2,Th6;
hence thesis by A1,A6,Lm4;
end;
theorem Th22:
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,J being
parahalting shiftable Program of SCMPDS holds IExec(I ';' J,P,s)
= IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)
proof
let s be 0-started State of SCMPDS;
let I be parahalting halt-free Program of SCMPDS,J be parahalting
shiftable Program of SCMPDS;
set A = NAT, D = SCM-Data-Loc, sI = stop I,
sIJ = stop (I ';' J), P1 = P +* stop I,
m1 = LifeSpan(P1,s), P2 = P +* stop(I ';' J),
s3 = Initialize Comput(P1,s,m1), P3 = P1 +* stop J,
m3 = LifeSpan(P3,s3);
A1: stop J c= P3 by FUNCT_4:25;
then
A2: P3 halts_on s3 by SCMPDS_4:def 7;
A3: stop J c= P +* stop J by FUNCT_4:25;
A4: stop I c= P1 by FUNCT_4:25;
then
P1 halts_on s by SCMPDS_4:def 7;
then
A5: Initialize Comput(P1,s,m1)
= Initialize IExec(I,P,s) by EXTPRO_1:23;
A6: Result(P +* stop J,Initialize IExec(I,P,s))
= Result(P3,s3) by A1,A3,Th6,A5;
A7: stop I c= P2 +* stop I by FUNCT_4:25;
A8: P2 +* stop I +* sIJ = P2 +* (stop I +* sIJ) by FUNCT_4:14
.= P2 +* sIJ by Th3;
A9: LifeSpan(P2 +* stop I,s) = m1 by A4,A7,Th6;
set S1=s,
E1 = P2 +* stop I;
A10: Comput(P1,s,m1)
= Comput(P1 +* stop(I ';' J), s,m1) by Th8,FUNCT_4:25;
A11: P +* stop I +* sIJ = P +* (stop I +* sIJ) by FUNCT_4:14
.= P +* (sIJ +* sIJ) by Th3
.= P2 +* stop I +* sIJ by A8;
A12: DataPart(Comput(P2 +* stop I,s,m1))
= DataPart Comput(P1, s,m1) by A11,A10,A9,Th8,FUNCT_4:25;
A13: sIJ c= P2 by FUNCT_4:25;
then
A14: DataPart Comput(P2,s,m1)
= DataPart(Initialize Comput(P2 +* stop I,s,m1)) by A9,Lm4
.= DataPart(Comput(P2 +* stop I, s,m1)) by MEMSTR_0:45;
A15: Shift(stop J,card I) c= P2 by A13,A7,Lm4;
A16: IC Comput(P2,s,m1) = card I by A13,A9,Lm4;
A17: DataPart Initialize Comput(P1,s,m1)
= DataPart Comput(P2,s,m1) by A12,A14,MEMSTR_0:45;
then
A18: IC Comput(P2, Comput(P2,s,m1),m3) = IC Comput(P3,s3,m3) + card I
by A15,A1,A16,SCMPDS_4:29;
A19: DataPart Comput(P2, Comput(P2,s,m1),m3) = DataPart Comput(P3,s3,m3)
by A16,A15,A1,A17,SCMPDS_4:29;
A20: P1 halts_on s by A4,SCMPDS_4:def 7;
then
A21: s3 = Initialize Result(P1,s) by EXTPRO_1:23;
set SS1 = Initialize Result(P1,s) +* stop J,
SS2 = Initialize IExec(I,P,s) +* stop J;
A22: IC Result(P1 +* stop J,Initialize Result(P1,s))
= IC Result(P +* stop J,Initialize IExec(I,P,s)) by Th6,A1,A3;
A23: P2 halts_on s
by A13,SCMPDS_4:def 7;
A24: IC IExec(I ';' J,P,s)
= IC Comput(P2,s,LifeSpan(P2,s)) by A23,EXTPRO_1:23
.= IC Comput(P2,s,m1+m3) by A21,Th21
.= IC Comput(P3,s3,m3) + card I by A18,EXTPRO_1:4
.= IC Result(P3,s3) + card I by A2,EXTPRO_1:23
.= IC IExec(J,P,Initialize IExec(I,P,s)) + card I
by A22,A20,EXTPRO_1:23;
IExec(I ';' J,P,s) = Comput(P2,s,LifeSpan(P2,s))
by A23,EXTPRO_1:23
.= Comput(P2,s,m1+m3) by A21,Th21;
then
A25: DataPart IExec(I ';' J,P,s)
= DataPart Comput(P3,s3,m3) by A19,EXTPRO_1:4
.= DataPart IExec(J,P,Initialize IExec(I,P,s))
by A6,A2,EXTPRO_1:23;
hereby
reconsider l = IC IExec(J,P,Initialize IExec(I,P,s)) + card I
as Nat;
A26: dom Start-At(l,SCMPDS) = {IC SCMPDS} by FUNCOP_1:13;
A27: now
let x be object;
assume
A28: x in dom IExec(I ';' J,P,s);
per cases by A28,SCMPDS_4:6;
suppose
A29: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A30: not x in dom Start-At(l,SCMPDS) by A26,TARSKI:def 1;
IExec(I ';' J,P,s).x
= IExec(J,P,Initialize IExec(I,P,s)).x
by A25,A29,SCMPDS_4:8;
hence
IExec(I ';' J,P,s).x
= (IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)).x
by A30,FUNCT_4:11;
end;
suppose
A31: x = IC SCMPDS;
then x in {IC SCMPDS} by TARSKI:def 1;
then
A32: x in dom Start-At(l,SCMPDS) by FUNCOP_1:13;
thus IExec(I ';' J,P,s).x = (Start-At(l,SCMPDS)).IC SCMPDS
by A24,A31,FUNCOP_1:72
.= (IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)).x
by A31,A32,FUNCT_4:13;
end;
end;
dom IExec(I ';' J,P,s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)
by PARTFUN1:def 2;
hence thesis by A27,FUNCT_1:2;
end;
end;
theorem
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,J being
parahalting shiftable Program of SCMPDS holds IExec(I ';' J,P,s).a
= IExec(J,P,Initialize IExec(I,P,s)).a
proof
let s be 0-started State of SCMPDS;
let I be parahalting halt-free Program of SCMPDS,J be parahalting
shiftable Program of SCMPDS;
A1: not a in
dom Start-At(IC IExec(J,P,Initialize IExec(I,P,s)) + card I,SCMPDS)
by SCMPDS_4:18;
IExec(I ';' J,P,s) = IncIC(IExec(J,P,Initialize IExec(I,P,s)),card I)
by Th22;
hence thesis by A1,FUNCT_4:11;
end;
begin :: Computation of the program consisting of a instruction and a block
::$CT
theorem
s1 | (SCM-Data-Loc \/ {IC SCMPDS})
= s2 | (SCM-Data-Loc \/ {IC SCMPDS}) implies s1 = s2
proof
set Y = NAT;
set X = SCM-Data-Loc \/ {IC SCMPDS};
A1: s1 = s1|(Data-Locations SCMPDS \/ {IC SCMPDS})
& s2 = s2|(Data-Locations SCMPDS \/ {IC SCMPDS}) by MEMSTR_0:33;
thus thesis by A1,SCMPDS_2:84;
end;
theorem Th25:
DataPart s1 = DataPart s2 & InsCode i <> 3 implies
DataPart Exec(i,s1) = DataPart Exec(i,s2)
proof
assume that
A1: DataPart s1 = DataPart s2 and
A2: InsCode i <> 3;
InsCode i = 0 or ... or InsCode i = 14 by SCMPDS_2:6;
then per cases by A2;
suppose InsCode i = 0;
then Exec(i,s1) = s1 & Exec(i,s2) = s2 by SCMPDS_2:86;
hence thesis by A1;
end;
suppose
InsCode i = 14;
then
A3: ex k1 st i = goto k1 by SCMPDS_2:26;
now
let a;
thus Exec(i, s1).a = s1.a by A3,SCMPDS_2:54
.=s2.a by A1,SCMPDS_4:8
.=Exec(i, s2).a by A3,SCMPDS_2:54;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 1;
then consider a such that
A4: i = return a by SCMPDS_2:27;
now
let b;
per cases;
suppose
A5: a=b;
hence Exec(i, s1).b= s1.DataLoc(s1.a,RetSP) by A4,SCMPDS_2:58
.=s2.DataLoc(s2.a,RetSP) by A1,SCMPDS_3:2
.=Exec(i,s2).b by A4,A5,SCMPDS_2:58;
end;
suppose
A6: a<>b;
hence Exec(i, s1).b = s1.b by A4,SCMPDS_2:58
.=s2.b by A1,SCMPDS_4:8
.=Exec(i,s2).b by A4,A6,SCMPDS_2:58;
end;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 2;
then consider a,k1 such that
A7: i = a := k1 by SCMPDS_2:28;
now
let b;
per cases;
suppose
A8: a=b;
hence Exec(i, s1).b= k1 by A7,SCMPDS_2:45
.=Exec(i,s2).b by A7,A8,SCMPDS_2:45;
end;
suppose
A9: a<>b;
hence Exec(i,s1).b = s1.b by A7,SCMPDS_2:45
.=s2.b by A1,SCMPDS_4:8
.=Exec(i,s2).b by A7,A9,SCMPDS_2:45;
end;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 4;
then
A10: ex a,k1,k2 st i = (a,k1)<>0_goto k2 by SCMPDS_2:30;
now
let a;
thus Exec(i, s1).a = s1.a by A10,SCMPDS_2:55
.=s2.a by A1,SCMPDS_4:8
.=Exec(i, s2).a by A10,SCMPDS_2:55;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 5;
then
A11: ex a,k1,k2 st i = (a,k1)<=0_goto k2 by SCMPDS_2:31;
now
let a;
thus Exec(i, s1).a = s1.a by A11,SCMPDS_2:56
.=s2.a by A1,SCMPDS_4:8
.=Exec(i, s2).a by A11,SCMPDS_2:56;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 6;
then
A12: ex a,k1,k2 st i = (a,k1)>=0_goto k2 by SCMPDS_2:32;
now
let a;
thus Exec(i, s1).a = s1.a by A12,SCMPDS_2:57
.=s2.a by A1,SCMPDS_4:8
.=Exec(i, s2).a by A12,SCMPDS_2:57;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 7;
then consider a,k1,k2 such that
A13: i = (a,k1) := k2 by SCMPDS_2:33;
now
let b;
per cases;
suppose
A14: DataLoc(s1.a,k1)=b;
then
A15: DataLoc(s2.a,k1)=b by A1,SCMPDS_4:8;
thus Exec(i, s1).b= k2 by A13,A14,SCMPDS_2:46
.=Exec(i,s2).b by A13,A15,SCMPDS_2:46;
end;
suppose
A16: DataLoc(s1.a,k1)<>b;
then
A17: DataLoc(s2.a,k1)<>b by A1,SCMPDS_4:8;
thus Exec(i,s1).b = s1.b by A13,A16,SCMPDS_2:46
.=s2.b by A1,SCMPDS_4:8
.=Exec(i,s2).b by A13,A17,SCMPDS_2:46;
end;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 8;
then consider a,k1,k2 such that
A18: i = AddTo(a,k1,k2) by SCMPDS_2:34;
now
let b;
per cases;
suppose
A19: DataLoc(s1.a,k1)=b;
then
A20: DataLoc(s2.a,k1)=b by A1,SCMPDS_4:8;
thus Exec(i, s1).b= s1.DataLoc(s1.a,k1)+k2 by A18,A19,SCMPDS_2:48
.= s2.DataLoc(s2.a,k1)+k2 by A1,SCMPDS_3:2
.=Exec(i,s2).b by A18,A20,SCMPDS_2:48;
end;
suppose
A21: DataLoc(s1.a,k1)<>b;
then
A22: DataLoc(s2.a,k1)<>b by A1,SCMPDS_4:8;
thus Exec(i,s1).b = s1.b by A18,A21,SCMPDS_2:48
.=s2.b by A1,SCMPDS_4:8
.=Exec(i,s2).b by A18,A22,SCMPDS_2:48;
end;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 9;
then consider a,b,k1,k2 such that
A23: i = AddTo(a,k1,b,k2) by SCMPDS_2:35;
now
let c;
per cases;
suppose
A24: DataLoc(s1.a,k1)=c;
then
A25: DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)+s1.DataLoc(s1.b,k2) by A23,A24
,SCMPDS_2:49
.= s2.DataLoc(s2.a,k1)+s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
.= s2.DataLoc(s2.a,k1)+s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
.=Exec(i,s2).c by A23,A25,SCMPDS_2:49;
end;
suppose
A26: DataLoc(s1.a,k1)<>c;
then
A27: DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
thus Exec(i,s1).c = s1.c by A23,A26,SCMPDS_2:49
.=s2.c by A1,SCMPDS_4:8
.=Exec(i,s2).c by A23,A27,SCMPDS_2:49;
end;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 10;
then consider a,b,k1,k2 such that
A28: i = SubFrom(a,k1,b,k2) by SCMPDS_2:36;
now
let c;
per cases;
suppose
A29: DataLoc(s1.a,k1)=c;
then
A30: DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)-s1.DataLoc(s1.b,k2)
by A28,A29,SCMPDS_2:50
.= s2.DataLoc(s2.a,k1)-s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
.= s2.DataLoc(s2.a,k1)-s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
.=Exec(i,s2).c by A28,A30,SCMPDS_2:50;
end;
suppose
A31: DataLoc(s1.a,k1)<>c;
then
A32: DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
thus Exec(i,s1).c = s1.c by A28,A31,SCMPDS_2:50
.=s2.c by A1,SCMPDS_4:8
.=Exec(i,s2).c by A28,A32,SCMPDS_2:50;
end;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 11;
then consider a,b,k1,k2 such that
A33: i = MultBy(a,k1,b,k2) by SCMPDS_2:37;
now
let c;
per cases;
suppose
A34: DataLoc(s1.a,k1)=c;
then
A35: DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1)*s1.DataLoc(s1.b,k2) by A33,A34
,SCMPDS_2:51
.= s2.DataLoc(s2.a,k1)*s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
.= s2.DataLoc(s2.a,k1)*s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
.=Exec(i,s2).c by A33,A35,SCMPDS_2:51;
end;
suppose
A36: DataLoc(s1.a,k1)<>c;
then
A37: DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
thus Exec(i,s1).c = s1.c by A33,A36,SCMPDS_2:51
.=s2.c by A1,SCMPDS_4:8
.=Exec(i,s2).c by A33,A37,SCMPDS_2:51;
end;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 12;
then consider a,b,k1,k2 such that
A38: i = Divide(a,k1,b,k2) by SCMPDS_2:38;
now
let c;
per cases;
suppose
A39: DataLoc(s1.b,k2)=c;
then
A40: DataLoc(s2.b,k2)=c by A1,SCMPDS_4:8;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) mod s1.DataLoc(s1.b,k2) by A38
,A39,SCMPDS_2:52
.= s2.DataLoc(s2.a,k1) mod s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
.= s2.DataLoc(s2.a,k1) mod s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
.= Exec(i,s2).c by A38,A40,SCMPDS_2:52;
end;
suppose
A41: DataLoc(s1.b,k2)<>c;
then
A42: DataLoc(s2.b,k2)<>c by A1,SCMPDS_4:8;
hereby
per cases;
suppose
A43: DataLoc(s1.a,k1)<>c;
then
A44: DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
thus Exec(i, s1).c = s1.c by A38,A41,A43,SCMPDS_2:52
.=s2.c by A1,SCMPDS_4:8
.=Exec(i,s2).c by A38,A42,A44,SCMPDS_2:52;
end;
suppose
A45: DataLoc(s1.a,k1)=c;
then
A46: DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
thus Exec(i, s1).c = s1.DataLoc(s1.a,k1) div s1.DataLoc(s1.b,k2)
by A38,A41,A45,SCMPDS_2:52
.= s2.DataLoc(s2.a,k1) div s1.DataLoc(s1.b,k2) by A1,SCMPDS_3:2
.= s2.DataLoc(s2.a,k1) div s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
.= Exec(i,s2).c by A38,A42,A46,SCMPDS_2:52;
end;
end;
end;
end;
hence thesis by SCMPDS_4:8;
end;
suppose
InsCode i = 13;
then consider a,b,k1,k2 such that
A47: i = (a,k1):=(b,k2) by SCMPDS_2:39;
now
let c;
per cases;
suppose
A48: DataLoc(s1.a,k1)=c;
then
A49: DataLoc(s2.a,k1)=c by A1,SCMPDS_4:8;
thus Exec(i, s1).c = s1.DataLoc(s1.b,k2) by A47,A48,SCMPDS_2:47
.= s2.DataLoc(s2.b,k2) by A1,SCMPDS_3:2
.=Exec(i,s2).c by A47,A49,SCMPDS_2:47;
end;
suppose
A50: DataLoc(s1.a,k1)<>c;
then
A51: DataLoc(s2.a,k1)<>c by A1,SCMPDS_4:8;
thus Exec(i,s1).c = s1.c by A47,A50,SCMPDS_2:47
.=s2.c by A1,SCMPDS_4:8
.=Exec(i,s2).c by A47,A51,SCMPDS_2:47;
end;
end;
hence thesis by SCMPDS_4:8;
end;
end;
theorem Th26:
for i being shiftable Instruction of SCMPDS holds (DataPart s1 =
DataPart s2 implies DataPart Exec(i,s1) = DataPart Exec(i,s2))
proof
let i be shiftable Instruction of SCMPDS;
InsCode i <> 3 by SCMPDS_4:def 10;
hence thesis by Th25;
end;
theorem Th27:
for s being 0-started State of SCMPDS
for i being parahalting Instruction of SCMPDS
holds Exec(i,s) = IExec(Load i,P,s)
proof
let s be 0-started State of SCMPDS;
let i be parahalting Instruction of SCMPDS;
set Li=Load i, Mi= Macro i;
set PI = P +* Mi;
set IC1 = IC Comput(PI, s,1);
A1: Initialize s = s by MEMSTR_0:44;
Mi c= PI by FUNCT_4:25;
then
A2: PI halts_on s by SCMPDS_4:def 7;
A3: 1 in dom Mi by COMPOS_1:57;
A4: 0 in dom Mi by COMPOS_1:57;
A5: Mi. 1=halt SCMPDS by COMPOS_1:59;
A6: Mi. 0 = i by COMPOS_1:58;
A7: Mi c= PI by FUNCT_4:25;
then
A8: IC1 in dom Mi by SCMPDS_4:def 6;
A9: PI/.IC s = PI.IC s by PBOOLE:143;
A10: Comput(PI, s,0+1) = Following(PI,Comput(PI,s,0)) by EXTPRO_1:3
.= Following(PI,s)
.= Exec(PI. 0, s) by A9,A1,MEMSTR_0:47
.= Exec(i, s) by A4,A6,A7,GRFUNC_1:2;
per cases by A8,COMPOS_1:60;
suppose
A11: IC1 = 0;
set Ni=InsCode i;
IC s + 1 = 0+1 by A1,MEMSTR_0:47;
then
A12: Ni in {0,1,4,5,6,14} by A10,A11,SCMPDS_4:1;
A13: CurInstr(PI,Comput(PI,s,1)) = PI. 0 by A11,PBOOLE:143
.= i by A4,A6,A7,GRFUNC_1:2;
A14: Ni <> 1 by Th10;
hereby
per cases;
suppose
i = halt SCMPDS;
hence thesis by A2,A10,A13,EXTPRO_1:def 9;
end;
suppose
A15: i <> halt SCMPDS;
A16: now
let b;
per cases by A12,A14,ENUMSET1:def 4;
suppose
InsCode i = 0;
hence s.b=Exec(i, s).b by SCMPDS_2:86;
end;
suppose
InsCode i = 14;
then ex k1 st i = goto k1 by SCMPDS_2:26;
hence s.b=Exec(i, s).b by SCMPDS_2:54;
end;
suppose
InsCode i = 4;
then ex a,k1,k2 st i = (a,k1)<>0_goto k2 by SCMPDS_2:30;
hence s.b=Exec(i, s).b by SCMPDS_2:55;
end;
suppose
InsCode i = 5;
then ex a,k1,k2 st i = (a,k1)<=0_goto k2 by SCMPDS_2:31;
hence s.b=Exec(i, s).b by SCMPDS_2:56;
end;
suppose
InsCode i = 6;
then ex a,k1,k2 st i = (a,k1)>=0_goto k2 by SCMPDS_2:32;
hence s.b=Exec(i, s).b by SCMPDS_2:57;
end;
end;
A17: Following(PI,s) = Following(PI,Comput(PI,s,0))
.= Exec(i, s) by A10,EXTPRO_1:3;
A18: IC s = IC Exec(i, s) by A10,A11,A1,MEMSTR_0:47;
then
A19: s = Exec(i, s) by A16,SCMPDS_2:44;
now
let n;
Comput(PI, s,n) = s by A18,A16,A17,EXTPRO_1:27,SCMPDS_2:44
.= Following(PI,Comput(PI,s,0))
by A19,A17
.= Comput(PI, s,0+1) by EXTPRO_1:3;
hence CurInstr(PI,Comput(PI,s,n)) <> halt SCMPDS by A13,A15;
end;
then not PI halts_on s;
hence thesis by A7,SCMPDS_4:def 7;
end;
end;
end;
suppose
A20: IC1 = 1;
CurInstr(PI,Comput(PI,s,1))
= PI. 1 by A20,PBOOLE:143
.= halt SCMPDS by A3,A5,A7,GRFUNC_1:2;
hence thesis by A2,A10,EXTPRO_1:def 9;
end;
end;
theorem Th28:
for s being 0-started State of SCMPDS
for I being parahalting halt-free Program of SCMPDS,
j being parahalting shiftable Instruction of SCMPDS
holds IExec(I ';' j,P,s).a = Exec(j,IExec(I,P,s)).a
proof
let s be 0-started State of SCMPDS;
let I be parahalting halt-free Program of SCMPDS,j be parahalting
shiftable Instruction of SCMPDS;
set Mj = Load j;
set SA = Start-At (IC IExec(Mj,P,Initialize IExec(I,P,s)) + card I,SCMPDS);
A1: not a in dom SA by SCMPDS_4:18;
A2: a in SCM-Data-Loc by AMI_2:def 16;
for a holds (Initialize IExec(I,P,s)).a = IExec(I,P,s).a by Th4;
then
A3: DataPart Initialize IExec(I,P,s) = DataPart IExec(I,P,s) by SCMPDS_4:8;
thus IExec(I ';' j,P,s).a
= IncIC(IExec(Mj,P,Initialize IExec(I,P,s)),card I).a by Th22
.= IExec(Mj,P,Initialize IExec(I,P,s)).a by A1,FUNCT_4:11
.= Exec(j, Initialize IExec(I,P,s)).a by Th27
.= (DataPart Exec(j, Initialize IExec(I,P,s))).a
by A2,FUNCT_1:49,SCMPDS_2:84
.= (DataPart Exec(j, IExec(I,P,s))).a by A3,Th26
.= Exec(j, IExec(I,P,s)).a by A2,FUNCT_1:49,SCMPDS_2:84;
end;
theorem
for s being 0-started State of SCMPDS
for i being No-StopCode parahalting Instruction of SCMPDS,
j being shiftable parahalting Instruction of SCMPDS
holds IExec(i ';' j,P,s).a = Exec(j,Exec(i, s)).a
proof
let s be 0-started State of SCMPDS;
let i be No-StopCode parahalting Instruction of SCMPDS, j be shiftable
parahalting Instruction of SCMPDS;
set Mi = Load i;
thus IExec(i ';' j,P,s).a = IExec(Mi ';' j,P,s).a
.= Exec(j, IExec(Mi,P,s)).a by Th28
.= Exec(j, Exec(i, s)).a by Th27;
end;