:: The Construction and Computation of Conditional Statements 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, AMI_2, RELAT_1,
XBOOLE_0, GRAPHSP, XXREAL_0, CIRCUIT2, ARYTM_3, CARD_1, FUNCT_1, FUNCT_4,
TARSKI, TURING_1, SCMFSA_7, SCMPDS_4, AMISTD_2, COMPLEX1, VALUED_1,
SCMFSA6B, MSUALG_1, SCMPDS_5, SCMFSA8A, AMI_3, ARYTM_1, UNIALG_2,
SCMFSA7B, SCMFSA8B, NAT_1, STRUCT_0, SCMPDS_6, PARTFUN1, EXTPRO_1,
SCMFSA6C, COMPOS_1;
notations TARSKI, XBOOLE_0, SUBSET_1, XCMPLX_0, RELAT_1, FUNCT_1, CARD_1,
PARTFUN1, VALUED_1, ORDINAL1, NUMBERS, COMPLEX1, FUNCT_4, INT_1, NAT_1,
STRUCT_0, MEMSTR_0, COMPOS_0, COMPOS_1, EXTPRO_1, AMI_2, SCMPDS_2,
SCMPDS_4, SCMPDS_5, XXREAL_0;
constructors REAL_1, INT_2, SCMPDS_4, SCMPDS_5, FUNCT_4, PRE_POLY, RELSET_1,
DOMAIN_1;
registrations XXREAL_0, XREAL_0, NAT_1, INT_1, SCMPDS_2, SCMPDS_4, SCMPDS_5,
ORDINAL1, XBOOLE_0, MEMSTR_0, AFINSQ_1, COMPOS_1, FUNCT_4, RELAT_1,
AMI_3, COMPOS_0;
requirements NUMERALS, REAL, SUBSET, ARITHM;
definitions SCMPDS_4;
equalities FUNCOP_1, COMPOS_1, EXTPRO_1, SCMPDS_4, MEMSTR_0, ORDINAL1;
expansions EXTPRO_1, SCMPDS_4;
theorems NAT_1, TARSKI, FUNCT_4, FUNCT_1, INT_1, SCMPDS_2, ABSVALUE, GRFUNC_1,
SCMPDS_4, SCMPDS_5, XBOOLE_1, XREAL_1, ORDINAL1, FUNCOP_1, XXREAL_0,
VALUED_1, PARTFUN1, MEMSTR_0, AFINSQ_1, COMPOS_1, EXTPRO_1, PBOOLE,
RELAT_1;
schemes NAT_1;
begin :: Preliminaries
reserve m,n for Nat,
a for Int_position,
i,j for Instruction of SCMPDS,
s,s1,s2 for State of SCMPDS,
k1 for Integer,
loc for Nat,
I,J,K for Program of SCMPDS;
set A = NAT;
set D = SCM-Data-Loc;
Lm1: (Stop SCMPDS). 0 = halt SCMPDS;
Lm2: 0 in dom Stop SCMPDS by COMPOS_1:3;
reserve P,P1,P2 for Instruction-Sequence of SCMPDS;
::$CT 5
theorem Th1:
card (i ';' I)= card I + 1
proof
thus card (i ';' I) = card (Load i ';' I)
.=card (Load i) + card I by AFINSQ_1:17
.=card I+1 by COMPOS_1:54;
end;
theorem Th2:
(i ';' I). 0=i
proof
i ';' I=Load i ';' I & 0 in dom Load i by COMPOS_1:50;
hence (i ';' I). 0 =(Load i). 0 by AFINSQ_1:def 3
.=i;
end;
::$CT 3
theorem Th3:
CurInstr(P +* stop(i ';' I),Initialize s) = i
proof
set iI=i ';' I, P3 = P +* stop(i ';' I);
A1: 0 in dom Load i by COMPOS_1:50;
card iI=card I +1 by Th1;
then
A2: 0 in dom iI by AFINSQ_1:66;
iI c= stop iI by AFINSQ_1:74;
then dom iI c= dom stop iI by RELAT_1:11;
then
A3: 0 in dom stop iI by A2;
A4: (P +* stop(i ';' I))/.IC (Initialize s)
= (P +* stop(i ';' I)).IC (Initialize s) by PBOOLE:143;
P3.0 = (P +* stop(i ';' I)). 0
.= (stop iI). 0 by A3,FUNCT_4:13
.= iI. 0 by A2,COMPOS_1:63
.=(Load i ';' I). 0
.=(Load i). 0 by A1,AFINSQ_1:def 3
.=i;
hence thesis by A4,MEMSTR_0:47;
end;
theorem Th4:
for s being State of SCMPDS,m1,m2 being Nat st IC s=
m1 holds ICplusConst(s,m2)= m1+m2
proof
let s be State of SCMPDS,m1,m2 be Nat;
ex m being Element of NAT st m = IC s & ICplusConst(s,m2) = |.m+m2.|
by SCMPDS_2:def 18;
hence thesis by ABSVALUE:def 1;
end;
theorem Th5:
for I,J being Program of SCMPDS holds Shift(stop J,card I) c=
stop(I ';' J)
proof
let I,J be Program of SCMPDS;
stop(I ';' J) =I ';' J ';' Stop SCMPDS
.=I ';' (J ';' Stop SCMPDS) by AFINSQ_1:27
.=I ';' (stop J);
then stop(I ';' J) = I +* Shift(stop J, card I);
hence thesis by FUNCT_4:25;
end;
::$CT
theorem
for s being 0-started State of SCMPDS, i being No-StopCode parahalting
Instruction of SCMPDS,J being parahalting shiftable Program of SCMPDS, a being
Int_position
holds IExec(i ';' J,P,s).a = IExec(J,P,Initialize Exec(i,s)).a
proof
let s be 0-started State of SCMPDS,
i be No-StopCode parahalting Instruction of SCMPDS,
J be parahalting shiftable Program of SCMPDS, a be Int_position;
thus IExec(i ';' J,P,s).a = IExec(Load i ';' J,P,s).a
.= IExec(J,P,Initialize IExec(Load i,P,s)).a by SCMPDS_5:35
.= IExec(J,P,Initialize Exec(i,s)).a by SCMPDS_5:40;
end;
theorem
for a being Int_position,k1,k2 being Integer holds (a,k1)
<>0_goto k2 <> halt SCMPDS
proof
InsCode halt SCMPDS = 0 by COMPOS_1:70;
hence thesis by SCMPDS_2:16;
end;
theorem
for a being Int_position,k1,k2 being Integer
holds (a,k1) <=0_goto k2 <> halt SCMPDS
proof
InsCode halt SCMPDS = 0 by COMPOS_1:70;
hence thesis by SCMPDS_2:17;
end;
theorem
for a being Int_position,k1,k2 being Integer
holds (a,k1) >=0_goto k2 <> halt SCMPDS
proof
InsCode halt SCMPDS = 0 by COMPOS_1:70;
hence thesis by SCMPDS_2:18;
end;
definition
let k1 be Integer;
func Goto k1 -> Program of SCMPDS equals
Load goto k1;
coherence;
end;
registration
let n be Nat;
cluster goto (n+1) -> No-StopCode;
correctness by SCMPDS_5:21;
cluster goto -(n+1) -> No-StopCode;
correctness by SCMPDS_5:21;
end;
registration
let n be Nat;
cluster Goto (n+1) -> halt-free;
correctness;
cluster Goto -(n+1) -> halt-free;
correctness;
end;
theorem Th10:
0 in dom Goto k1 & (Goto k1). 0 = goto k1 by AFINSQ_1:65;
begin :: The predicates of is_closed_on and is_halting_on
definition
let I be Program of SCMPDS;
let s be State of SCMPDS;
let P;
pred I is_closed_on s,P means
for k being Nat holds
IC Comput(P+*stop I,Initialize s,k) in dom stop I;
pred I is_halting_on s,P means
P+*stop I halts_on Initialize s;
end;
theorem Th11:
for I being Program of SCMPDS holds I is paraclosed iff
for s being State of SCMPDS, P holds I is_closed_on s,P
proof
let I be Program of SCMPDS;
thus I is paraclosed implies for s be State of SCMPDS,P holds
I is_closed_on s,P by FUNCT_4:25;
assume
A1: for s being State of SCMPDS,P holds I is_closed_on s,P;
let s be 0-started State of SCMPDS;
let k be Nat;
let P;
A2: Initialize s = s by MEMSTR_0:44;
assume stop I c= P;
then
A3: P = P +* stop I by FUNCT_4:98;
I is_closed_on s,P by A1;
hence IC Comput(P,s,k) in dom stop I by A2,A3;
end;
theorem Th12:
for I being Program of SCMPDS holds I is parahalting iff
for s being State of SCMPDS,P holds I is_halting_on s,P
proof
let I be Program of SCMPDS;
thus I is parahalting implies for s be State of SCMPDS, P holds
I is_halting_on s,P by FUNCT_4:25;
assume
A1: for s being State of SCMPDS, P holds I is_halting_on s,P;
let s be 0-started State of SCMPDS, P;
A2: Initialize s = s by MEMSTR_0:44;
assume stop I c= P;
then
A3: P = P +* stop I by FUNCT_4:98;
I is_halting_on s,P by A1;
hence P halts_on s by A3,A2;
end;
theorem Th13:
for s1,s2 being State of SCMPDS, I being Program of SCMPDS st
DataPart s1 = DataPart s2 holds I is_closed_on s1,P1
implies I is_closed_on s2,P2
proof
let s1,s2 be State of SCMPDS,I be Program of SCMPDS;
set pI=stop I, S1 = Initialize s1, S2 = Initialize s2,
E1 = P1 +* pI, E2 = P2 +* pI;
assume
A1: DataPart s1 = DataPart s2;
A2: Comput(E2,S2,0) = Initialize s2 by EXTPRO_1:2;
A3: Comput(E1,S1,0) = Initialize s1 by EXTPRO_1:2;
then
A4: DataPart Comput(E1,S1,0) = DataPart s1 by MEMSTR_0:45
.= DataPart Comput(E2,S2,0) by A1,A2,MEMSTR_0:45;
defpred P[Nat] means IC Comput(E1,S1,$1) = IC Comput(E2,S2,$1)
& CurInstr(E1,Comput(E1,S1,$1)) = CurInstr(E2,Comput(E2,S2,$1))
& DataPart Comput(E1,S1,$1) = DataPart Comput(E2,S2,$1);
A5: 0 in dom pI by COMPOS_1:36;
assume
A6: I is_closed_on s1,P1;
A7: now
let k be Nat;
A8: Comput(E2,S2,k+1) = Following(E2,Comput(E2,S2,k)) by EXTPRO_1:3;
assume
A9: P[k];
then
A10: for a holds Comput(E1,S1,k).a = Comput(E2,S2,k).
a by SCMPDS_4:8;
pI c= P2 +* pI by FUNCT_4:25;
then
A11: pI c= E2;
A12: IC Comput(E1,S1,k+1) in dom pI by A6;
A13: Comput(E1,S1,k+1) = Following(E1,Comput(E1,S1,k)) by EXTPRO_1:3;
Comput(E1,S1,k) = Comput(E2,S2,k) by A9,A10,SCMPDS_4:2;
then
A14: Comput(E1,S1,k+1) = Comput(E2,S2,k+1) by A9,A8,A13;
then
A15: Comput(E1,S1,k+1)
= Comput(E2,S2,k+1);
A16: IC Comput(E1,S1,k+1) = IC Comput(E2,S2,k+1) by A14;
A17
: E1/.IC Comput(E1,S1,k+1)
= E1.IC Comput(E1,S1,k+1) by PBOOLE:143;
A18: E2/.IC Comput(E2,S2,k+1)
= E2.IC Comput(E2,S2,k+1) by PBOOLE:143;
pI c= P1 +* pI by FUNCT_4:25;
then pI c= E1;
then CurInstr(E1,Comput(E1,S1,k+1))
= pI.IC Comput(E1,S1,k+1) by A12,A17,GRFUNC_1:2
.= CurInstr(E2,Comput(E2,S2,k+1))
by A11,A16,A12,A18,GRFUNC_1:2;
hence P[k+1] by A15;
end;
A19: IC Comput(E2,S2,0) = IC S2 by A2
.= 0 by MEMSTR_0:def 11;
A20: E1/.IC Comput(E1,S1,0)
= E1.IC Comput(E1,S1,0) by PBOOLE:143;
A21: E2/.IC Comput(E2,S2,0)
= E2.IC Comput(E2,S2,0) by PBOOLE:143;
A22: IC Comput(E1,S1,0) = IC S1
by A3
.= 0 by MEMSTR_0:def 11;
then CurInstr(E1,Comput(E1,S1,0))
= pI. 0 by A5,A20,FUNCT_4:13
.= CurInstr(E2,Comput(E2,S2,0)) by A19,A5,A21,FUNCT_4:13;
then
A23: P[0] by A22,A19,A4;
now
let k be Nat;
A24: for k being Nat holds P[k] from NAT_1:sch 2(A23,A7);
IC Comput(E1,S1,k) in dom pI by A6;
hence IC Comput(E2,S2,k) in dom pI by A24;
end;
hence thesis;
end;
theorem
for s1,s2 being State of SCMPDS,I being Program of SCMPDS st DataPart
s1 = DataPart s2 holds I is_closed_on s1,P1 & I is_halting_on s1,P1
implies I is_closed_on s2,P2 & I is_halting_on s2,P2
proof
let s1,s2 be State of SCMPDS,I be Program of SCMPDS;
set pI=stop I, S1 = Initialize s1, S2 = Initialize s2,
E1 = P1 +* pI, E2 = P2 +* pI;
defpred P[Nat] means
IC Comput(E1,S1,$1) = IC Comput(E2,S2,$1) &
CurInstr(E1,Comput(E1,S1,$1)) = CurInstr(E2,Comput(E2,S2,$1))
& DataPart
Comput(E1,S1,$1) = DataPart Comput(E2,S2,$1);
A1: Comput(E1,S1,0) = Initialize s1 by EXTPRO_1:2;
A2: Comput(E2,S2,0) = Initialize s2 by EXTPRO_1:2;
assume DataPart s1 = DataPart s2;
then
A3: Comput(E1,S1,0) = Comput(E2,S2,0) by A1,A2,MEMSTR_0:80;
A4: 0 in dom pI by COMPOS_1:36;
assume
A5: I is_closed_on s1,P1;
A6: now
let k be Nat;
A7: Comput(E2,S2,k+1) = Following(E2,Comput(E2,S2,k)) by EXTPRO_1:3;
assume
A8: P[k];
then for a holds Comput(E1,S1,k).a = Comput(E2,S2,k).a by SCMPDS_4:8;
then
A9: Comput(E1,S1,k) = Comput(E2,S2,k) by A8,SCMPDS_4:2;
A10: pI c= E2 by FUNCT_4:25;
A11: IC Comput(E1,S1,k+1) in dom pI by A5;
Comput(E1,S1,k+1) = Following(E1,Comput(E1,S1,k)) by EXTPRO_1:3;
then
A12: Comput(E1,S1,k+1) = Comput(E2,S2,k+1) by A8,A9,A7;
then
A13: IC Comput(E1,S1,k+1) = IC Comput(E2,S2,k+1);
A14: E1/.IC Comput(E1,S1,k+1)
= E1.IC Comput(E1,S1,k+1) by PBOOLE:143;
A15: E2/.IC Comput(E2,S2,k+1)
= E2.IC Comput(E2,S2,k+1) by PBOOLE:143;
pI c= E1 by FUNCT_4:25;
then CurInstr(E1,Comput(E1,S1,k+1))
= pI.IC Comput(E1,S1,k+1) by A11,A14,GRFUNC_1:2
.= CurInstr(E2,Comput(E2,S2,k+1))
by A10,A13,A11,A15,GRFUNC_1:2;
hence P[k+1] by A12;
end;
A16: IC Comput(E2,S2,0) = IC S2 by A2
.= 0 by MEMSTR_0:def 11;
assume
I is_halting_on s1,P1;
then P1 +* pI halts_on Initialize s1;
then consider m such that
A17: CurInstr(E1,Comput(E1,S1,m)) = halt SCMPDS;
A18: E1/.IC Comput(E1,S1,0) = E1.IC Comput(E1,S1,0) by PBOOLE:143;
A19: E2/.IC Comput(E2,S2,0) = E2.IC Comput(E2,S2,0) by PBOOLE:143;
IC Comput(E1,S1,0) = IC S1 by A1
.= 0 by MEMSTR_0:def 11;
then CurInstr(E1,Comput(E1,S1,0))
= pI. 0 by A4,A18,FUNCT_4:13
.= CurInstr(E2,Comput(E2,S2,0)) by A16,A4,A19,FUNCT_4:13;
then
A20: P[0] by A3;
now
let k be Nat;
A21: for k being Nat holds P[k] from NAT_1:sch 2(A20,A6);
IC Comput(E1,S1,k) in dom pI by A5;
hence IC Comput(E2,S2,k) in dom pI by A21;
end;
hence I is_closed_on s2,P2;
for k being Nat holds P[k] from NAT_1:sch 2(A20,A6);
then CurInstr(E2,Comput(E2,S2,m))
= halt SCMPDS by A17;
then P2 +* pI halts_on Initialize s2 by EXTPRO_1:29;
hence thesis;
end;
theorem
for s being State of SCMPDS, I,J being Program of SCMPDS holds I
is_closed_on s,P iff I is_closed_on Initialize s,P+*J
proof
let s be State of SCMPDS,I,J be Program of SCMPDS;
DataPart s = DataPart Initialize s by MEMSTR_0:45;
hence thesis by Th13;
end;
theorem Th16:
for s being 0-started State of SCMPDS
for I,J being Program of SCMPDS
st I is_closed_on s,P & I is_halting_on s,P
holds (for k being Nat
st k <= LifeSpan(P +* stop I,s) holds
IC Comput(P +* stop I,s,k) = IC Comput(P +* stop(I ';' J),s,k)) &
DataPart Comput(P +* stop I,s,LifeSpan(P +* stop I,s)) =
DataPart Comput(P +* stop(I ';' J),s,LifeSpan(P +* stop I,s))
proof
let s be 0-started State of SCMPDS;
let I,J be Program of SCMPDS;
assume
A1: I is_closed_on s,P;
A2: Initialize s = s by MEMSTR_0:44;
set pI=stop I, pIJ=stop (I ';' J), P1 = P +* pI;
defpred X[Nat] means $1 <= LifeSpan(P1,s) implies
Comput(P1, s,$1) = Comput(P1 +* pIJ, s,$1);
assume I is_halting_on s,P;
then
A3: P1 halts_on s by A2;
A4: for m st X[m] holds X[m+1]
proof
set JS=J ';' Stop SCMPDS, E2 = P1 +* pIJ;
let m;
assume
A5: m <= LifeSpan(P1,s) implies Comput(P1, s,m) = Comput(P1 +* pIJ, s,m);
A6: pIJ c= E2 by FUNCT_4:25;
A7: Comput(P1,s,m+1) = Following(P1,Comput(P1,s,m)) by EXTPRO_1:3;
A8: pIJ =I ';' J ';' Stop SCMPDS
.=I ';' JS by AFINSQ_1:27;
dom(I ';' JS) = dom (I +* Shift(JS, card I))
.= dom I \/ dom Shift(JS, card I) by FUNCT_4:def 1;
then
A9: dom I c= dom(I ';' JS) by XBOOLE_1:7;
A10: Comput(E2,s,m+1) = Following(E2,Comput(E2,s,m)) by EXTPRO_1:3;
A11: IC Comput(P1,s,m) in dom pI by A1,A2;
A12: P1/.IC Comput(P1,s,m)
= P1.IC Comput(P1,s,m) by PBOOLE:143;
pI c= P1 by FUNCT_4:25;
then
A13: CurInstr(P1,Comput(P1,s,m))
= pI.IC (Comput(P1,s,m)) by A11,A12,GRFUNC_1:2;
assume
A14: m+1 <= LifeSpan(P1,s);
then m < LifeSpan(P1,s) by NAT_1:13;
then pI.IC(Comput(P1,s,m)) <> halt SCMPDS by A3,A13,EXTPRO_1:def 15;
then
A15: IC Comput(P1,s,m) in dom I by A11,COMPOS_1:51;
A16: E2/.IC Comput(E2,s,m)
= E2.IC Comput(E2,s,m) by PBOOLE:143;
CurInstr(P1,Comput(P1,s,m))
= (I ';' Stop SCMPDS).IC (Comput(P1,s,m)) by A13
.=I.IC (Comput(P1,s,m)) by A15,AFINSQ_1:def 3
.=pIJ.IC(Comput(P1,s,m)) by A15,A8,AFINSQ_1:def 3
.=E2.IC(Comput(P1,s,m)) by A6,A15,A8,A9,GRFUNC_1:2
.= CurInstr(E2,Comput(E2,s,m))
by A5,A14,A16,NAT_1:13;
hence thesis by A5,A14,A7,A10,NAT_1:13;
end;
Comput(P1, s,0) = s &
Comput(P1 +* pIJ, s,0) = s by EXTPRO_1:2;
then
A17: X[0];
A18: for m holds X[m] from NAT_1:sch 2(A17,A4);
A19: P +* pI +* pIJ = P +* (pI +* pIJ) by FUNCT_4:14
.= P +* pIJ by SCMPDS_5:14;
thus for k being Nat st k <= LifeSpan(P1,s)
holds IC Comput(P1,s,k) =IC Comput(P +* pIJ, s,k) by A18,A19;
Comput(P +* stop I, s, LifeSpan(P +* stop I,s)) =
Comput(P +* stop(I ';' J),s,(LifeSpan(P +* stop I,s))) by A19,A18;
hence
DataPart Comput(P +* stop I, s, (LifeSpan(P +* stop I,s))) =
DataPart Comput(P +* stop(I ';' J), s,(LifeSpan(P +* stop I,s)));
end;
theorem Th17:
for I being Program of SCMPDS,k be Nat st I
is_closed_on s,P & I is_halting_on s,P &
k < LifeSpan(P +* stop I,Initialize s)
holds IC Comput(P +* stop I,Initialize s,k) in dom I
proof
let I be Program of SCMPDS,k be Nat;
set ss= Initialize s, PP = P +* stop I,
m=LifeSpan(PP,ss), Sp =Stop SCMPDS;
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P and
A3: k < m;
set Sk= Comput(PP, ss,k), Ik=IC Sk;
A4: Ik in dom stop(I) by A1;
reconsider n = Ik as Nat;
A5: stop I c= PP by FUNCT_4:25;
A6: PP halts_on ss by A2;
A7: now
A8: PP/.IC Sk = PP.IC Sk by PBOOLE:143;
assume
A9: n = card I;
CurInstr(PP,Sk) =PP.Ik by A8
.=(stop I).(0+n) by A4,A5,GRFUNC_1:2
.=halt SCMPDS by A9,Lm1,Lm2,AFINSQ_1:def 3;
hence contradiction by A3,A6,EXTPRO_1:def 15;
end;
card stop I=card I + 1 by COMPOS_1:55;
then n < card I + 1 by A4,AFINSQ_1:66;
then n <= card I by INT_1:7;
then n < card I by A7,XXREAL_0:1;
hence thesis by AFINSQ_1:66;
end;
theorem Th18:
for I,J being Program of SCMPDS,
s being 0-started State of SCMPDS, k being
Nat st I is_closed_on s,P & I is_halting_on s,P &
k < LifeSpan(P +* stop I,s)
holds CurInstr(P +* stop I, Comput(P +* stop I, s,k)) =
CurInstr(P +* stop(I ';' J),Comput(P +* stop(I ';' J),s,k))
proof
let I,J be Program of SCMPDS,
s be 0-started State of SCMPDS,k be Nat;
set P1 = P +* stop I, P2 = P +* stop(I ';' J);
set s3= Comput(P1, s,k), s4= Comput(P2, s,k),
P3 = P1, P4 = P2,
SS=Stop SCMPDS;
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P & k < LifeSpan(P1,s);
A3: Initialize s = s by MEMSTR_0:44;
then
A4: IC s3 in dom I by A1,A2,Th17;
A5: IC s3= IC s4 by A1,A2,Th16;
A6: IC s3 in dom stop(I) by A1,A3;
A7: dom stop I c= dom stop (I ';' J) & stop (I ';' J) c= P2 by FUNCT_4:25
,SCMPDS_5:13;
A8: stop I c= P1 by FUNCT_4:25;
A9: stop (I ';' J) = I ';' J ';' SS
.=I ';' (J ';' SS) by AFINSQ_1:27;
A10: P3/.IC s3 = P3.IC s3 by PBOOLE:143;
A11: P4/.IC s4 = P4.IC s4 by PBOOLE:143;
thus CurInstr(P1,s3) =P1.IC s3 by A10
.=(stop I).IC s3 by A6,A8,GRFUNC_1:2
.=I.IC s3 by A4,AFINSQ_1:def 3
.=(stop (I ';' J)).IC s3 by A4,A9,AFINSQ_1:def 3
.=P2.IC s4 by A5,A6,A7,GRFUNC_1:2
.=CurInstr(P2,s4) by A11;
end;
theorem Th19: ::SCMPDS_5:32
for I being halt-free Program of SCMPDS,s being State of
SCMPDS, k being Nat st I is_closed_on s,P &
I is_halting_on s,P & k <
LifeSpan(P +* stop I,Initialize s)
holds
CurInstr(P +* stop I,Comput(P +* stop I,Initialize s,k)) <> halt SCMPDS
proof
let I be halt-free Program of SCMPDS,s be State of SCMPDS, k be Nat;
set ss=Initialize s, PP = P +* stop I,
s2= Comput(PP, ss,k), P2 = PP;
assume
I is_closed_on s,P & I is_halting_on s,P & k < LifeSpan(PP,ss);
then
A1: IC s2 in dom I by Th17;
A2: P2/.IC s2 = P2.IC s2 by PBOOLE:143;
A3: stop I c= PP by FUNCT_4:25;
I c= stop I by AFINSQ_1:74;
then I c= PP by A3,XBOOLE_1:1;
then CurInstr(P2,s2)=I.IC s2 by A1,A2,GRFUNC_1:2;
hence thesis by A1,COMPOS_1:def 27;
end;
theorem Th20:
for I being halt-free Program of SCMPDS,s being State of
SCMPDS st I is_closed_on s,P & I is_halting_on s,P
holds IC Comput(P +* stop I, Initialize s,
LifeSpan(P +* stop I,Initialize s)) = card I
proof
let I be halt-free Program of SCMPDS,s be State of SCMPDS;
set s1=Initialize s, P1 = P +* stop I;
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P;
set Css= Comput(P1, s1,LifeSpan(P1,s1));
reconsider n = IC Css as Nat;
A3: stop I c= P1 by FUNCT_4:25;
I c= stop I by AFINSQ_1:74;
then
A4: I c= P1 by A3,XBOOLE_1:1;
A5: P1 halts_on s1 by A2;
now
A6: P1/.IC Css = P1.IC Css by PBOOLE:143;
assume
A7: IC Css in dom I;
then I.IC Css=P1.IC Css by A4,GRFUNC_1:2
.=CurInstr(P1,Css) by A6
.=halt SCMPDS by A5,EXTPRO_1:def 15;
hence contradiction by A7,COMPOS_1:def 27;
end;
then
A8: n >= card I by AFINSQ_1:66;
A9: card stop I =card I + 1 by COMPOS_1:55;
IC Css in dom stop(I) by A1;
then n < card I + 1 by A9,AFINSQ_1:66;
then n <= card I by NAT_1:13;
then IC Comput(P1, s1,LifeSpan(P1,s1)) = card I by A8,XXREAL_0:1;
hence thesis;
end;
Lm3:
for I being halt-free Program of SCMPDS, J being Program of SCMPDS,
s being 0-started State of SCMPDS
st I is_closed_on s,P & I is_halting_on s,P
holds IC Comput(P +* stop (I ';' Goto (card J + 1) ';' J ),
s, (LifeSpan(P +* stop I,s) + 1)) =
(card I + card J + 1) &
DataPart Comput(P +* stop I, s,
(LifeSpan(P +* stop I,s)))
= DataPart Comput(P +* stop (I ';' Goto(card J +
1) ';' J), s,
(LifeSpan(P +* stop I,s) + 1)) &
(for k being Element of
NAT st k <= LifeSpan(P +* stop I,s)
holds CurInstr(P +*stop (I ';' Goto (card J + 1) ';' J ),
Comput(P +*stop (I ';' Goto (card J + 1) ';' J ),
s,k)) <> halt SCMPDS) &
IC Comput(P +* stop (I ';' Goto (card J + 1) ';' J), s,
LifeSpan(P +* stop I,s))
= card I &
P +* stop (I ';' Goto (card J + 1) ';' J)
halts_on s &
LifeSpan(P +* stop (I ';' Goto (
card J + 1) ';' J),s) = LifeSpan(P +* stop I,s) + 1
proof
let I be halt-free Program of SCMPDS, J be Program of SCMPDS,
s be 0-started State of SCMPDS;
assume
A1: I is_closed_on s,P;
set G1=Goto (card J + 1), SS = Stop SCMPDS, J2 = G1 ';' J ';' SS, IJ=I ';'
G1 ';' J, pJ=stop IJ, s1 = s, P1 = P +* stop I,
s2 = s;
reconsider P2 = P +* pJ
as Instruction-Sequence of SCMPDS;
assume
A2: I is_halting_on s,P;
A3: Initialize s = s by MEMSTR_0:44;
set sm= Comput(P2, s2,LifeSpan(P1,s1));
A4: IJ =I ';' (G1 ';' J) by AFINSQ_1:27;
then
A5: IC Comput(P1, s1,LifeSpan(P1,s1)) =IC sm by A1,A2,Th16;
then
A6: IC sm = card I by A1,A2,Th20,A3;
A7: 0 in dom G1 by Th10;
A8: J2. 0 = (G1 ';' (J ';' SS)). 0 by AFINSQ_1:27
.=G1. 0 by A7,AFINSQ_1:def 3
.=goto (card J + 1);
card (G1 ';' J) = card G1 + card J by AFINSQ_1:17
.=1 + card J by COMPOS_1:54;
then
A9: J2. (card J + 1)=J2.(0+card (G1 ';' J))
.=halt SCMPDS by Lm1,Lm2,AFINSQ_1:def 3;
A10: card J2 = card (G1 ';' (J ';' SS)) by AFINSQ_1:27
.=card G1 + card (J ';' SS) by AFINSQ_1:17
.= 1 + card (J ';' SS) by COMPOS_1:54;
then
A11: 0 in dom J2 by AFINSQ_1:66;
A12: pJ =I ';' G1 ';' J ';' SS
.=I ';' (G1 ';' J) ';' SS by AFINSQ_1:27
.=I ';' J2 by AFINSQ_1:27;
then
A13: card pJ = card I + card J2 by AFINSQ_1:17;
0 < card J2;
then card I + 0 < card pJ by A13,XREAL_1:6;
then
A14: card I in dom pJ by AFINSQ_1:66;
A15: card SS = 1 by AFINSQ_1:34;
A16: card J2 = 1 + (card J + card SS) by A10,AFINSQ_1:17
.= card J + (1 + card SS);
then card J + 1 < card J2 by A15,XREAL_1:6;
then
A17: (card J + 1) in dom J2 by AFINSQ_1:66;
card pJ = card I + card J + 1 + 1 by A13,A16,A15;
then card I + card J + 1 < card pJ by NAT_1:13;
then
A18: (card I + card J + 1) in dom pJ by AFINSQ_1:66;
A19: P2/.IC Comput(P2,s2,LifeSpan(P1,s1))
= P2.IC Comput(P2,s2,LifeSpan(P1,s1)) by PBOOLE:143;
A20: CurInstr(P2,Comput(P2,s2,LifeSpan(P1,s1)))
= P2.card I by A1,A2,A5,Th20,A19,A3
.= P2. card I
.= pJ. card I by A14,FUNCT_4:13
.= (I ';' J2).(0+card I) by A12
.= goto (card J + 1) by A11,A8,AFINSQ_1:def 3;
A21: now
let a;
thus Comput(P2, s2,LifeSpan(P1,s1) + 1).a
= (Following(P2,sm)).a by EXTPRO_1:3
.= sm.a by A20,SCMPDS_2:54;
end;
A22: P2/.IC Comput(P2, s2,LifeSpan(P1,s1) + 1)
= P2.IC Comput(P2, s2,LifeSpan(P1,s1) + 1)
by PBOOLE:143;
thus IC Comput(P +* pJ, s2,LifeSpan(P1,s1) + 1)
= IC Following(P2,sm) by EXTPRO_1:3
.= ICplusConst(sm,card J +1) by A20,SCMPDS_2:54
.= (card I + (card J + 1)) by A6,Th4
.= (card I + card J + 1);
then
A23: CurInstr(P2,
Comput(P2, s2,LifeSpan(P1,s1) + 1))
= P2. (card I + card J
+ 1) by A22
.= pJ. (card I + card J + 1) by A18,FUNCT_4:13
.= (I ';' J2).(card I+(card J+1)) by A12
.= halt SCMPDS by A17,A9,AFINSQ_1:def 3;
DataPart Comput(P1, s1,LifeSpan(P1,s1)) = DataPart
sm by A1,A2,A4,Th16;
hence DataPart Comput(P1, s1,LifeSpan(P1,s1)) =
DataPart Comput(P +* pJ, s2,LifeSpan(P1,s1) + 1)
by A21,SCMPDS_4:8;
thus
A24:
now
let k be Element of NAT;
assume
A25: k <= LifeSpan(P1,s1);
per cases;
suppose
A26: k < LifeSpan(P1,s1);
then CurInstr(P1,Comput(P1,s1,k)) <> halt SCMPDS by A1,A2,Th19,A3;
hence CurInstr(P +* pJ,Comput(P +* pJ,s2,k)) <> halt SCMPDS
by A1,A2,A4,A26,Th18;
end;
suppose
LifeSpan(P1,s1) <= k;
then k = LifeSpan(P1,s1) by A25,XXREAL_0:1;
hence CurInstr(P +* pJ,Comput(P +* pJ,s2,k)) <>
halt SCMPDS by A20;
end;
end;
thus IC Comput(P +* pJ,s2,LifeSpan(P1,s1))
= card I by A1,A2,A5,Th20,A3;
thus
A27: P +* pJ halts_on s2 by A23,EXTPRO_1:29;
now
let k be Nat;
A28: k in NAT by ORDINAL1:def 12;
assume
CurInstr(P2,Comput(P2,s2,k))
= halt SCMPDS;
then LifeSpan(P1,s1) < k by A24,A28;
hence LifeSpan(P1,s1)+1 <= k by INT_1:7;
end;
hence thesis by A23,A27,EXTPRO_1:def 15;
end;
theorem Th21:
for I,J being Program of SCMPDS,
s being 0-started State of SCMPDS st I
is_closed_on s,P & I is_halting_on s,P holds I ';' Goto (card J + 1) ';' J
is_halting_on s,P & I ';' Goto (card J + 1) ';' J is_closed_on s,P
proof
let I,J be Program of SCMPDS,s be 0-started State of SCMPDS;
set G = Goto (card J + 1), IJ = I ';' G ';' J, J2 = I ';' (G ';' J), pJ =
stop J2, pI =stop I, P1 = P +* pI, P2 = P +* pJ,
m=LifeSpan(P1,s), SS=Stop SCMPDS,
s3= Comput(P1, s,m), s4= Comput(P2, s,m),
P3= P1, P4 = P2;
A1: Initialize s = s by MEMSTR_0:44;
A2: IJ=I ';' (G ';' J) by AFINSQ_1:27;
A3: I c= stop I by AFINSQ_1:74;
pI c= P3 by FUNCT_4:25;
then
A4: I c= P3 by A3,XBOOLE_1:1;
A5: dom pI c= dom pJ by SCMPDS_5:13;
set JS=G ';' J ';' SS;
reconsider n = IC s3 as Nat;
A6: card pI=card I + 1 by COMPOS_1:55;
assume
A7: I is_closed_on s,P;
then IC s3 in dom pI by A1;
then n < card I + 1 by A6,AFINSQ_1:66;
then
A8: n <= card I by INT_1:7;
A9: pJ c= P2 by FUNCT_4:25;
A10: pJ =I ';' (G ';' J) ';' SS
.=I ';' JS by AFINSQ_1:27;
then I c= pJ by AFINSQ_1:74;
then I c= P2 by A9,XBOOLE_1:1;
then
A11: I c= P4;
assume
A12: I is_halting_on s,P;
then
A13: P1 halts_on s by A1;
A14: P3/.IC s3
= P3.IC s3 by PBOOLE:143;
A15: P4/.IC s4
= P4.IC s4 by PBOOLE:143;
per cases;
suppose
IC s3 <> card I;
then n < card I by A8,XXREAL_0:1;
then
A16: IC s3 in dom I by AFINSQ_1:66;
A17: halt SCMPDS=CurInstr(P1,s3) by A13,EXTPRO_1:def 15
.=I.IC s3 by A4,A16,A14,GRFUNC_1:2
.=P4.IC s3 by A11,A16,GRFUNC_1:2
.=CurInstr(P4,s4) by A7,A12,Th16,A15;
then
A18: P2 halts_on s by EXTPRO_1:29;
hence IJ is_halting_on s,P by A2,A1;
now
let k be Nat;
set C1k=IC Comput(P1, s,k), C2k=IC Comput(P2
, s,k);
per cases;
suppose
A19: k <= m;
C1k in dom pI by A7,A1;
then C1k in dom pJ by A5;
hence C2k in dom pJ by A7,A12,A19,Th16;
end;
suppose
A20: k > m;
set m2=LifeSpan(P2,s);
A21: m2 <= m by A17,A18,EXTPRO_1:def 15;
then C2k=IC Comput(P2, s,m2) by A18,A20,EXTPRO_1:25,XXREAL_0:2
.=IC Comput(P1, s,m2) by A7,A12,A21,Th16;
then C2k in dom pI by A7,A1;
hence C2k in dom pJ by A5;
end;
end;
hence thesis by A2,A1;
end;
suppose
A22: IC s3 = card I;
then
A23: IC s4= card I by A7,A12,Th16;
A24: 0 in dom G by Th10;
A25: card Stop SCMPDS = 1 by AFINSQ_1:34;
A26: JS =G ';' (J ';' SS) by AFINSQ_1:27;
then
A27: card JS =card G + card (J ';' SS) by AFINSQ_1:17
.= 1 + card (J ';' SS) by COMPOS_1:54
.= card J + 1 + 1 by A25,AFINSQ_1:17;
then
A28: 0 in dom JS by AFINSQ_1:66;
card J + 1 < card JS by A27,NAT_1:13;
then
A29: (card J + 1) in dom JS by AFINSQ_1:66;
card pJ = card I + (card J + (1 + 1)) by A10,A27,AFINSQ_1:17
.= card I + card J + 1 + 1;
then
A30: card I + card J + 1 < card pJ by NAT_1:13;
then
A31: (card I + card J + 1) in dom pJ by AFINSQ_1:66;
A32: P4/.IC s4
= P4.IC s4 by PBOOLE:143;
A33: card pJ = card I + card JS by A10,AFINSQ_1:17;
0 < card JS;
then card I + 0 < card pJ by XREAL_1:6,A33;
then
A34: card I in dom pJ by AFINSQ_1:66;
A35: CurInstr(P4,s4)= P4. card I by A7,A12,A22,Th16,A32
.= P2. card I
.= (I ';' JS).(0+card I) by A10,A9,A34,GRFUNC_1:2
.= JS. 0 by A28,AFINSQ_1:def 3
.=G. 0 by A26,A24,AFINSQ_1:def 3
.=goto (card J + 1);
card (G ';' J) = card G + card J by AFINSQ_1:17
.=1 + card J by COMPOS_1:54;
then
A36: JS. (card J + 1)=JS.(0+card (G ';' J))
.=halt SCMPDS by Lm1,Lm2,AFINSQ_1:def 3;
A37: P2/.IC Comput(P2,s,m+1) = P2.IC Comput(P2,s,m+1) by PBOOLE:143;
A38: IC Comput(P2, s,m + 1) = IC Following(P2,s4) by EXTPRO_1:3
.= ICplusConst(s4,card J +1) by A35,SCMPDS_2:54
.= (card I + (card J + 1)) by A23,Th4
.= (card I + card J + 1);
then
A39: CurInstr(P2,Comput(P2,s,m+1))
= P2. (card I + card J + 1) by A37
.= (I ';' JS).(card I+(card J+1)) by A10,A9,A31,GRFUNC_1:2
.= halt SCMPDS by A29,A36,AFINSQ_1:def 3;
then
A40: P2 halts_on s by EXTPRO_1:29;
hence IJ is_halting_on s,P by A2,A1;
now
let k be Nat;
set C1k=IC Comput(P1, s,k), C2k=IC Comput(P2, s,k);
per cases;
suppose
A41: k <= m;
C1k in dom pI by A7,A1;
then C1k in dom pJ by A5;
hence C2k in dom pJ by A7,A12,A41,Th16;
end;
suppose
A42: k > m;
set m2=LifeSpan(P2,s);
A43: m2 <= m+1 by A39,A40,EXTPRO_1:def 15;
k >= m+1 by A42,INT_1:7;
then C2k=IC Comput(P2, s,m2) by A40,A43,EXTPRO_1:25,XXREAL_0:2
.= (card I + card J + 1) by A38,A40,A43,EXTPRO_1:25;
hence C2k in dom pJ by A30,AFINSQ_1:66;
end;
end;
hence thesis by A2,A1;
end;
end;
theorem Th22:
for s1 being 0-started State of SCMPDS
for I being shiftable Program of SCMPDS
st stop I c= P1 & I is_closed_on s1,P1
for n being Nat st
Shift(stop I,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 s1 be 0-started State of SCMPDS;
let I be shiftable Program of SCMPDS;
set SI=stop I;
assume that
A1: SI c= P1 and
A2: I is_closed_on s1,P1;
A3: Initialize s1 = s1 by MEMSTR_0:44;
let n be Nat;
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);
assume that
A4: Shift(SI,n) c= P2 and
A5: IC s2 = n and
A6: DataPart s1 = DataPart s2;
let i be Nat;
A7: DataPart Comput(P1,s1,0) = DataPart s2 by A6,EXTPRO_1:2
.= DataPart Comput(P2,s2,0) by EXTPRO_1:2;
A8: 0 in dom SI by COMPOS_1:36;
then
A9: (0 + n) in dom Shift(SI,n) by VALUED_1:24;
A10: P1.IC s1 = P1.IC Initialize s1 by A3
.= P1. 0 by MEMSTR_0:def 11
.= SI. 0 by A1,A8,GRFUNC_1:2;
A11: P1= P1 +* SI by A1,FUNCT_4:98;
A12: for k being Nat st P[k] holds P[k + 1]
proof
let k be Nat;
assume
A13: P[k];
reconsider m = IC Comput(P1,s1,k) as Nat;
set i = CurInstr(P1,Comput(P1,s1,k));
A14: Comput(P1,s1,k+1) = Following(P1,Comput(P1,s1,k)) by EXTPRO_1:3;
reconsider l = IC Comput(P1,s1,k+1) as Nat;
A15: IC Comput(P1,s1,k+1) in dom SI by A2,A11,A3;
then
A16: l+n in dom Shift(SI,n) by VALUED_1:24;
A17: Comput(P2,s2,k+1) = Following(P2,Comput(P2,s2,k)) by EXTPRO_1:3;
A18: IC Comput(P1,s1,k) in dom SI by A2,A11,A3;
A19 : P1/.IC Comput(P1,s1,k) = P1.IC Comput(P1,s1,k) by PBOOLE:143;
A20: i = P1.IC Comput(P1,s1,k) by A19
.= SI.IC Comput(P1,s1,k) by A1,A18,GRFUNC_1:2;
then
A21: InsCode i <> 1 & InsCode i <> 3 by A18,SCMPDS_4:def 9;
A22: i valid_at m by A18,A20,SCMPDS_4:def 9;
hence
A23: IC Comput(P1,s1,k+1) + n = IC Comput(P2,s2,k+1)
by A13,A14,A17,A21,SCMPDS_4:28;
A24: P1/.IC Comput(P1,s1,k+1)
= P1.IC Comput(P1,s1,k+1) by PBOOLE:143;
A25: P2/.IC Comput(P2,s2,k+1)
= P2.IC Comput(P2,s2,k+1) by PBOOLE:143;
CurInstr(P1,Comput(P1,s1,k+1)) = P1.l by A24
.= SI.l by A1,A15,GRFUNC_1:2
.= SI.l;
hence CurInstr(P1,Comput(P1,s1,k+1))
= Shift(SI,n).(IC Comput(P2,s2,k+1))
by A23,A15,VALUED_1:def 12
.= P2.IC Comput(P2,s2,k+1) by A4,A23,A16,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s2,k+1))
by A25;
thus thesis by A13,A14,A17,A21,A22,SCMPDS_4:28;
end;
A26: IC Comput(P1,s1,0) = IC s1 by EXTPRO_1:2
.= IC Initialize s1 by A3
.= 0 by MEMSTR_0:def 11;
A27: Comput(P1,s1,0) = s1 by EXTPRO_1:2;
A28: Comput(P2,s2,0) = s2 by EXTPRO_1:2;
A29: P2/.IC s2 = P2.IC s2 by PBOOLE:143;
A30: P1/.IC s1 = P1.IC s1 by PBOOLE:143;
CurInstr(P1,Comput(P1,s1,0))
= CurInstr(P1,s1) by A27
.= Shift(SI,n).(0 + n) by A8,A10,A30,VALUED_1:def 12
.= CurInstr(P2,s2) by A4,A5,A9,A29,GRFUNC_1:2
.= CurInstr(P2,Comput(P2,s2,0))
by A28;
then
A31: P[0] by A5,A26,A7,EXTPRO_1:2;
for k being Nat holds P[k] from NAT_1:sch 2(A31,A12);
hence thesis;
end;
theorem Th23: ::SCMFSA8A:61
for s being 0-started State of SCMPDS,I being halt-free Program of SCMPDS,
J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P
holds IC IExec(I ';' Goto (card J + 1) ';' J,P,s)
= card I + card J + 1
proof
let s be 0-started State of SCMPDS,
I be halt-free Program of SCMPDS, J be Program of
SCMPDS;
set
m= LifeSpan(P +* stop I,Initialize s)+1,
G=Goto (card J + 1),
P2 = P +* stop (I ';' G ';' J);
A1: Initialize s = s by MEMSTR_0:44;
assume
A2: I is_closed_on s,P & I is_halting_on s,P;
then P2 halts_on s & LifeSpan(P2,s) = m by Lm3,A1;
then IC Result(P2,s) = IC Comput(P2, s,m) by EXTPRO_1:23
.= card I + card J + 1 by A2,Lm3,A1;
hence thesis;
end;
theorem Th24: ::SCMFSA8A:62
for s being 0-started State of SCMPDS,I being halt-free Program of
SCMPDS, J being Program of SCMPDS st I is_closed_on s,P & I is_halting_on s,P
holds
IExec(I ';' Goto (card J + 1) ';' J,P,s)
= IExec(I,P,s) +* Start-At((card I + card J + 1),SCMPDS)
proof
let s be 0-started State of SCMPDS,
I be halt-free Program of SCMPDS, J be Program of
SCMPDS;
set P1 = P +* stop I,
m= LifeSpan(P1,s)+1, G=Goto (card J + 1),
P2 = P +* stop (I ';' G ';' J),
l= (card I + card J + 1);
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P;
Initialize s = s by MEMSTR_0:44;
then
A3: P1 halts_on s by A2;
P2 halts_on s & LifeSpan(P2,s) = m
by A1,A2,Lm3;
then
A4: Result(P2,s) = Comput(P2, s,m) by EXTPRO_1:23;
then DataPart Result(P2,s) = DataPart Comput(P1,s,LifeSpan(P1,s))
by A1,A2,Lm3;
then
A5: DataPart Result(P2,s) = DataPart Result(P1,s) by A3,EXTPRO_1:23
.= DataPart(Result(P1,s) +* Start-At(l,SCMPDS)) by MEMSTR_0:79;
IC Result(P2,s) = l by A1,A2,A4,Lm3
.= IC(Result(P1,s) +* Start-At(l,SCMPDS)) by FUNCT_4:113;
then
A6: Result(P2,s) = (Result(P1,s) +* Start-At(l,SCMPDS)) by A5,MEMSTR_0:78;
thus IExec(I ';' G ';' J,P,s) = Result(P2,s)
.= Result(P1,s) +* (Start-At(l,SCMPDS)) by A6
.= IExec(I,P,s) +* Start-At(l,SCMPDS);
end;
theorem Th25:
for s being State of SCMPDS,I being halt-free Program of
SCMPDS st I is_closed_on s,P & I is_halting_on s,P
holds IC IExec(I,P,Initialize s) = card I
proof
let s be State of SCMPDS,I be halt-free Program of SCMPDS;
set s1=Initialize s, P1 = P +* stop I;
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P;
A3: P1 halts_on s1 by A2;
thus IC IExec(I,P,Initialize s) = IC Result(P1,s1)
.= IC Comput(P1, s1,LifeSpan(P1,s1)) by A3,EXTPRO_1:23
.= card I by A1,A2,Th20;
end;
begin :: The construction of conditional statements
definition
let a be Int_position,k be Integer;
let I,J be Program of SCMPDS;
func if=0(a,k,I,J) -> Program of SCMPDS equals
(a,k)<>0_goto (card I +2) ';' I ';' Goto (card J+1) ';' J;
coherence;
func if>0(a,k,I,J) -> Program of SCMPDS equals
(a,k)<=0_goto (card I +2) ';'
I ';' Goto (card J+1) ';' J;
coherence;
func if<0(a,k,I,J) -> Program of SCMPDS equals
(a,k)>=0_goto (card I +2) ';'
I ';' Goto (card J+1) ';' J;
coherence;
end;
definition
let a be Int_position,k be Integer;
let I be Program of SCMPDS;
func if=0(a,k,I) -> Program of SCMPDS equals
(a,k)<>0_goto (card I +1) ';' I;
coherence;
func if<>0(a,k,I) -> Program of SCMPDS equals
(a,k)<>0_goto 2 ';' goto (card
I+1) ';' I;
coherence;
func if>0(a,k,I) -> Program of SCMPDS equals
(a,k)<=0_goto (card I +1) ';' I;
coherence;
func if<=0(a,k,I) -> Program of SCMPDS equals
(a,k)<=0_goto 2 ';' goto (card
I+1) ';' I;
coherence;
func if<0(a,k,I) -> Program of SCMPDS equals
(a,k)>=0_goto (card I +1) ';' I;
coherence;
func if>=0(a,k,I) -> Program of SCMPDS equals
(a,k)>=0_goto 2 ';' goto (card
I+1) ';' I;
coherence;
end;
Lm4: card (i ';' I ';' Goto n ';' J) = card I + card J +2
proof
set G=Goto n;
thus card (i ';' I ';' G ';' J) =card (i ';' I ';' G) + card J by AFINSQ_1:17
.=card (i ';' I) + card G + card J by AFINSQ_1:17
.=card (i ';' I) + 1 + card J by COMPOS_1:54
.=card I +1 +1 +card J by Th1
.=card I + card J +2;
end;
begin :: The computation of "if var=0 then block1 else block2"
theorem
card if=0(a,k1,I,J) = card I + card J + 2 by Lm4;
theorem
0 in dom if=0(a,k1,I,J) & 1 in dom if=0(a,k1,I,J)
proof
set ci=card if=0(a,k1,I,J);
ci=card I + card J +2 by Lm4;
then 2 <= ci by NAT_1:12;
then 1 < ci by XXREAL_0:2;
hence thesis by AFINSQ_1:66;
end;
Lm5: (i ';' I ';' J ';' K). 0=i
proof
A1: 0 in dom Load i by COMPOS_1:50;
i ';' I ';' J ';' K =i ';' (I ';' J) ';' K by SCMPDS_4:14
.=i ';' (I ';' J ';' K) by SCMPDS_4:14
.=Load i ';' (I ';' J ';' K);
hence (i ';' I ';' J ';' K). 0 =(Load i). 0 by A1,AFINSQ_1:def 3
.=i;
end;
theorem
if=0(a,k1,I,J). 0 = (a,k1)<>0_goto (card I + 2) by Lm5;
Lm6: Shift(stop I,1) c= P +* stop(i ';' I)
proof
set pI=stop I, iI=i ';' I, piI=stop iI, P3=P+*piI;
card Load i=1 & iI=(Load i) ';' I by COMPOS_1:54;
then
A1: Shift(pI,1) c= piI by Th5;
piI c= P3 by FUNCT_4:25;
then Shift(pI,1) c= P3 by A1,XBOOLE_1:1;
hence thesis;
end;
Lm7: Shift(stop I,2) c= P+* stop(i ';' j ';' I)
proof
set pI=stop I, pjI=stop (i ';' j ';' I), P3=P+*pjI;
card (i ';' j)=card (Load i ';' Load j)
.=card Load i + card Load j by AFINSQ_1:17
.=1+ card Load j by COMPOS_1:54
.=1+1 by COMPOS_1:54;
then
A1: Shift(pI,2) c= pjI by Th5;
pjI c= P3 by FUNCT_4:25;
then Shift(pI,2) c= P3 by A1,XBOOLE_1:1;
hence thesis;
end;
theorem Th29:
for s being 0-started State of SCMPDS, I,J being shiftable Program of
SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)= 0 & I
is_closed_on s,P & I is_halting_on s,P holds if=0(a,k1,I,J) is_closed_on s,P
& if=0(a,k1,I,J) is_halting_on s,P
proof
let s be 0-started State of SCMPDS, I,J be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b = 0;
set i = (a,k1)<>0_goto (card I + 2);
set G=Goto (card J+1);
set I2 = I ';' G ';' J, IF=if=0(a,k1,I,J), pIF=stop IF,
pI2=stop I2, P2 = P +* pI2, P3 = P +* pIF,
s4 = Comput(P3,s,1),
P4 = P3;
A2: Initialize s = s by MEMSTR_0:44;
then
A3: IC s = 0 by MEMSTR_0:47;
A4: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' I2 by SCMPDS_4:14;
then
A5: Shift(pI2,1) c= P4 by Lm6;
A6: Comput(P3, s,0 + 1) = Following(P3,Comput(P3,s,0)) by EXTPRO_1:3
.= Following(P3,s) by EXTPRO_1:2
.= Exec(i,s) by A4,Th3,A2;
for a holds s.a= s4.a by A6,SCMPDS_2:55;
then
A7: DataPart s = DataPart s4 by SCMPDS_4:8;
s.DataLoc(s.a,k1)=s.b
.=0 by A1;
then
A8: IC s4 = IC s + 1 by A6,SCMPDS_2:55
.= (0+1) by A3;
A9: 0 in dom pIF by COMPOS_1:36;
assume
A10: I is_closed_on s,P;
assume
A11: I is_halting_on s,P;
then I2 is_halting_on s,P by A10,Th21;
then
A12: P2 halts_on s by A2;
A13: I2 is_closed_on s,P by A10,A11,Th21;
then
A14: Start-At(0,SCMPDS) c= s & I2 is_closed_on s,P2 by A2,FUNCT_4:25;
A15: card pIF = card IF +1 by COMPOS_1:55
.= card I2 +1+1 by A4,Th1;
A16: stop I2 c= P2 by FUNCT_4:25;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A17: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s,k1) as Nat;
A18: card pIF = card pI2+1 by A15,COMPOS_1:55;
m in dom pI2 by A13,A2;
then m < card pI2 by AFINSQ_1:66;
then
A19: m+1 < card pIF by A18,XREAL_1:6;
IC Comput(P3,s,k) = IC Comput(P3, s4,k1) by A17,EXTPRO_1:4
.= m + 1 by A14,A5,A8,A7,Th22,A16;
hence IC Comput(P3,s,k) in dom pIF by A19,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s,k) in dom pIF by A9,A3,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P by A2;
A20: Comput(P3,s,LifeSpan(P2,s)+1)
= Comput(P3,Comput(P3,s,1),LifeSpan(P2
,s))
by EXTPRO_1:4;
CurInstr(P3,Comput(P3,s,LifeSpan(P2,s)+1))
=CurInstr(P4,Comput(P4,s4,LifeSpan(P2,s))) by A20
.=CurInstr(P2,Comput(P2,s,LifeSpan(P2,s))) by A14,A5,A8,A7,Th22,A16
.= halt SCMPDS by A12,EXTPRO_1:def 15;
then P3 halts_on s by EXTPRO_1:29;
hence thesis by A2;
end;
theorem Th30:
for s being State of SCMPDS,I being Program of SCMPDS,J being
shiftable Program of SCMPDS,a being Int_position,k1 being Integer st s.DataLoc(
s.a,k1)<> 0 & J is_closed_on s,P & J is_halting_on s,P holds if=0(a,k1,I,J)
is_closed_on s,P & if=0(a,k1,I,J) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, J be shiftable Program of
SCMPDS, a be Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set pJ=stop J, s1 = Initialize s, P1 = P +* pJ,
IF=if=0(a,k1,I,J), pIF=
stop IF, s3 = Initialize s, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)<>0_goto (card I + 2);
set G =Goto (card J+1), iG=i ';' I ';' G;
A1: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' (I ';' G ';' J) by SCMPDS_4:14;
A2: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: IC s3 = 0 by MEMSTR_0:47;
assume
s.b <> 0;
then
A6: IC s4 = ICplusConst(s3,card I + 2) by A2,A4,SCMPDS_2:55
.= (0+(card I + 2)) by A5,Th4;
assume
A7: J is_closed_on s,P;
then
A8: Start-At(0,SCMPDS) c= s1 & J is_closed_on s1,P1 by FUNCT_4:25;
A9: pIF c= P3 by FUNCT_4:25;
A10: card iG = card (i ';' I) + card G by AFINSQ_1:17
.=card (i ';' I) + 1 by COMPOS_1:54
.=card I +1 +1 by Th1
.=card I +(1 +1);
then Shift(pJ,card I+2) c= pIF by Th5;
then
A11: Shift(pJ,card I+2) c= P4 by A9,XBOOLE_1:1;
assume
J is_halting_on s,P;
then
A12: P1 halts_on s1;
for a holds s1.a = s4.a by A2,SCMPDS_2:55;
then
A13: DataPart s1 = DataPart s4 by SCMPDS_4:8;
A14: pJ c= P1 by FUNCT_4:25;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A15: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P1, s1,k1) as Nat;
m in dom pJ by A7;
then m < card pJ by AFINSQ_1:66;
then
A16: m + (card I + 2) < card pJ + (card I + 2) by XREAL_1:6;
A17: card pJ = card J + 1 by COMPOS_1:55;
A18: card pIF = card IF+1 by COMPOS_1:55
.=card I +2 +card J +1 by A10,AFINSQ_1:17
.=card I +2 + card pJ by A17;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A15,EXTPRO_1:4
.= (m + (card I + 2)) by A8,A13,A11,A6,Th22,A14;
hence IC Comput(P3,s3,k) in dom pIF by A18,A16,AFINSQ_1:66;
end;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A5,COMPOS_1:36;
end;
end;
hence IF is_closed_on s,P;
A19: Comput(P3,s3,LifeSpan(P1,s1)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P1,
s1))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P1,s1)+1))
=CurInstr(P4,
Comput(P4,s4,LifeSpan(P1,s1))) by A19
.=CurInstr(P1,
Comput(P1,s1,LifeSpan(P1,s1))) by A8,A13,A11,A6,Th22,A14
.= halt SCMPDS by A12,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th31:
for s being 0-started State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, J being shiftable Program of SCMPDS,a being Int_position,k1
being Integer st s.DataLoc(s.a,k1)= 0 & I is_closed_on s,P &
I is_halting_on s,P
holds IExec(if=0(a,k1,I,J),P,s)
= IExec(I,P,s) +* Start-At((card I + card J+ 2),SCMPDS)
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, J be
shiftable Program of SCMPDS,a be Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b = 0;
set i = (a,k1)<>0_goto (card I + 2);
set G=Goto (card J+1);
set I2 = I ';' G ';' J, IF=if=0(a,k1,I,J), pI2=
stop I2, s2 = s, s3 = s,
P2 = P +* pI2, P3 = P +* stop IF,
s4 = Comput(P3,s3,1), P4 = P3;
A2: Initialize s = s by MEMSTR_0:44;
then
A3: IC s3 = 0 by MEMSTR_0:47;
A4: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' I2 by SCMPDS_4:14;
then
A5: Shift(pI2,1) c= P4 by Lm6;
A6: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A4,Th3,A2;
s3.DataLoc(s3.a,k1)=s3.b
.=0 by A1;
then
A7: IC s4 = IC s3 + 1 by A6,SCMPDS_2:55
.= (0+1) by A3;
for a holds s2.a = s4.a by A6,SCMPDS_2:55;
then
A8: DataPart s2 = DataPart s4 by SCMPDS_4:8;
set SAl= Start-At((card I + card J + 2),SCMPDS);
assume
A9: I is_closed_on s,P;
assume
A10: I is_halting_on s,P;
then I2 is_halting_on s,P by A9,Th21;
then
A11: P2 halts_on s2 by A2;
I2 is_closed_on s,P by A9,A10,Th21;
then
A12: Start-At(0,SCMPDS) c= s2 & I2 is_closed_on s2,P2 by A2,FUNCT_4:25;
A13: stop I2 c= P2 by FUNCT_4:25;
A14: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2,s2))
by EXTPRO_1:4;
A15: CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A14
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A12,A5,A7,A8,Th22,A13
.= halt SCMPDS by A11,EXTPRO_1:def 15;
then
A16: P3 halts_on s3 by EXTPRO_1:29;
A17: CurInstr(P3,s3) = i by A4,Th3,A2;
now
let l be Nat;
assume
A18: l < LifeSpan(P2,s2) + 1;
A19: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l)) =
CurInstr(P3,s3)
by A19;
hence CurInstr(P3,Comput(P3,s3,l)) <>
halt SCMPDS by A17;
end;
suppose
l <> 0;
then consider n be Nat such that
A20: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A21: n < LifeSpan(P2,s2) by A18,A20,XREAL_1:6;
assume
A22: CurInstr(P3,Comput(P3,s3,l)) = halt SCMPDS;
A23: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s2,n))
= CurInstr(P3,Comput(P3,s4,n))
by A12,A5,A7,A8,Th22,A13
.= halt SCMPDS by A20,A22,A23;
hence contradiction by A11,A21,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P2,s2) + 1 <= l;
then
A24: LifeSpan(P3,s3) = LifeSpan(P2,s2) + 1 by A15,A16,EXTPRO_1:def 15;
A25: DataPart Result(P2,s2) = DataPart Comput(P2, s2
,LifeSpan(P2,s2)) by A11,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s2)) by A12,A5,A7,A8,Th22,A13
.= DataPart Comput(P3, s3,LifeSpan(P2,s2) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A16,A24,EXTPRO_1:23;
A26: now
let x be object;
A27: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A28: x in dom IExec(IF,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 SAl by A27,TARSKI:def 1;
thus IExec(IF,P,s).x = (Result(P3,s3)).x
.= (Result(P2,s2)).x by A25,A29,SCMPDS_4:8
.= IExec(I2,P,s).x
.= (IExec(I2,P,s) +* SAl).x by A30,FUNCT_4:11;
end;
suppose
A31: x = IC SCMPDS;
A32: IC Result(P2,s2) = IC IExec(I2,P,s)
.= (card I + card J + 1) by A9,A10,Th23;
A33: x in dom SAl by A27,A31,TARSKI:def 1;
thus IExec(IF,P,s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P2,s2) + 1).x by A16,A24,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s2)) by A31,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 1
by A12,A5,A7,A8,Th22,A13
.= IC Result(P2,s2) + 1 by A11,EXTPRO_1:23
.= IC Start-At ((card I + card J + 1) + 1,SCMPDS)
by A32,FUNCOP_1:72
.= (IExec(I2,P,s) +* SAl).x by A31,A33,FUNCT_4:13;
end;
end;
dom IExec(IF,P,s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I2,P,s) +* SAl) by PARTFUN1:def 2;
hence IExec(IF,P,s) = IExec(I2,P,s) +* SAl by A26,FUNCT_1:2
.= IExec(I,P,s) +* Start-At((card I+card J+1),SCMPDS)
+* Start-At((card I + card J + 2),SCMPDS) by A9,A10,Th24
.= IExec(I,P,s) +* SAl by MEMSTR_0:36;
end;
theorem Th32:
for s being State of SCMPDS,I being Program of SCMPDS,J being
halt-free shiftable Program of SCMPDS,a being Int_position,k1 being Integer
st s.DataLoc(s.a,k1)<> 0 & J is_closed_on s,P & J is_halting_on s,P
holds IExec(if=0(a,k1,I,J),P,Initialize s) = IExec(J,P,Initialize s) +*
Start-At((card I + card J + 2),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS,J be halt-free shiftable
Program of SCMPDS,a be Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set pJ=stop J, s1 = Initialize s, P1 = P +* pJ,
P2 = P +* pJ,
IF=if=0(a,k1,I,J), pIF=
stop IF, s3 = Initialize s, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)<>0_goto (card I + 2);
set G =Goto (card J+1), iG=i ';' I ';' G;
set SAl=Start-At((card I+card J+2),SCMPDS);
A1: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' (I ';' G ';' J) by SCMPDS_4:14;
A2: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: IC s3 = 0 by MEMSTR_0:47;
assume
s.b <> 0;
then
A6: IC s4 = ICplusConst(s3,card I + 2) by A2,A4,SCMPDS_2:55
.= (0+(card I + 2)) by A5,Th4;
for a holds s1.a= s4.a by A2,SCMPDS_2:55;
then
A7: DataPart s1 = DataPart s4 by SCMPDS_4:8;
card iG = card (i ';' I) + card G by AFINSQ_1:17
.=card (i ';' I) + 1 by COMPOS_1:54
.=card I +1 +1 by Th1
.=card I +(1 +1);
then
A8: Shift(pJ,card I+2) c= pIF by Th5;
pIF c= P3 by FUNCT_4:25;
then Shift(pJ,card I+2) c= P3 by A8,XBOOLE_1:1;
then
A9: Shift(pJ,card I+2) c= P4;
assume
A10: J is_closed_on s,P;
then
A11: Start-At(0,SCMPDS) c= s1 & J is_closed_on s1,P1 by FUNCT_4:25;
A12: stop J c= P1 by FUNCT_4:25;
assume
A13: J is_halting_on s,P;
then
A14: P1 halts_on s1;
A15: Comput(P3,s3,LifeSpan(P1,s1)+1) =
Comput(P3,Comput(P3,s3,1),LifeSpan(P1,s1
))
by EXTPRO_1:4;
A16: CurInstr(P3,
Comput(P3,s3,LifeSpan(P1,s1)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P1,s1))) by A15
.=CurInstr(P1,
Comput(P1,s1,LifeSpan(P1,s1))) by A11,A9,A6,A7,Th22,A12
.= halt SCMPDS by A14,EXTPRO_1:def 15;
then
A17: P3 halts_on s3 by EXTPRO_1:29;
A18: CurInstr(P3,s3) = i by A1,Th3;
now
let l be Nat;
assume
A19: l < LifeSpan(P1,s1) + 1;
A20: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A20;
hence CurInstr(P3,Comput(P3,s3,l)) <>
halt SCMPDS by A18;
end;
suppose
l <> 0;
then consider n be Nat such that
A21: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A22: n < LifeSpan(P1,s1) by A19,A21,XREAL_1:6;
assume
A23: CurInstr(P3,Comput(P3,s3,l)) = halt SCMPDS;
A24: Comput(P3,s3,n+1) =
Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P1,Comput(P1,
s1,n))
= CurInstr(P3,
Comput(P3,s4,n)) by A11,A9,A6,A7,Th22,A12
.= halt SCMPDS by A21,A23,A24;
hence contradiction by A14,A22,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P1,s1) + 1 <= l;
then
A25: LifeSpan(P3,s3) = LifeSpan(P1,s1) + 1 by A16,A17,EXTPRO_1:def 15;
A26: DataPart Result(P1,s1) = DataPart Comput(P1, s1
,LifeSpan(P1,s1)) by A14,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P1,s1))
by A11,A9,A6,A7,Th22,A12
.= DataPart Comput(P3, s3,LifeSpan(P1,s1) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A17,A25,EXTPRO_1:23;
A27: now
let x be object;
A28: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A29: x in dom IExec(IF,P,Initialize s);
per cases by A29,SCMPDS_4:6;
suppose
A30: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A31: not x in dom SAl by A28,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= (Result(P1,s1)).x by A26,A30,SCMPDS_4:8
.= IExec(J,P,Initialize s).x
.= (IExec(J,P,Initialize s) +* SAl).x by A31,FUNCT_4:11;
end;
suppose
A32: x = IC SCMPDS;
A33: IC Result(P1,s1) = IC IExec(J,P,Initialize s)
.= (card J) by A10,A13,Th25;
A34: x in dom SAl by A28,A32,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P1,s1) + 1).x by A17,A25,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P1,s1)) by A32,EXTPRO_1:4
.= IC Comput(P1, s1,LifeSpan(P1,s1)) + (card I + 2)
by A11,A9,A6,A7,Th22,A12
.= IC Result(P1,s1) + (card I + 2) by A14,EXTPRO_1:23
.= IC Start-At (card J + (card I + 2),SCMPDS) by A33,FUNCOP_1:72
.= (IExec(J,P,Initialize s) +* SAl).x by A32,A34,FUNCT_4:13;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(J,P,Initialize s) +* SAl) by PARTFUN1:def 2;
hence thesis by A27,FUNCT_1:2;
end;
registration
let I,J be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if=0(a,k1,I,J) -> shiftable parahalting;
correctness
proof
set i = (a,k1)<>0_goto (card I + 2), G =Goto (card J+1);
set IF=if=0(a,k1,I,J);
reconsider IJ=I ';' G ';' J as shiftable Program of SCMPDS;
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume stop IF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
A4: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1)= 0;
then IF is_halting_on s,P by A4,Th29;
hence P halts_on s by A1,A2;
end;
suppose
s.DataLoc(s.a,k1) <> 0;
then IF is_halting_on s,P by A3,Th30;
hence P halts_on s by A1,A2;
end;
end;
end;
registration
let I,J be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if=0(a,k1,I,J) -> halt-free;
coherence;
end;
theorem
for s being 0-started State of SCMPDS,I,J being halt-free shiftable
parahalting Program of SCMPDS,a being Int_position,k1 being Integer holds IC
IExec(if=0(a,k1,I,J),P,s) = card I + card J + 2
proof
let s be 0-started State of SCMPDS,
I,J be halt-free shiftable parahalting Program of
SCMPDS,a be Int_position,k1 be Integer;
set IF=if=0(a,k1,I,J);
A1: J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
A2: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
A3: Initialize s = s by MEMSTR_0:44;
hereby
per cases;
suppose
s.DataLoc(s.a,k1) = 0;
then
IExec(IF,P,s) = IExec(I,P,s) +* Start-At((card I+card J+2),SCMPDS)
by A2,Th31;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) <> 0;
then
IExec(IF,P,s) = IExec(J,P,s) +* Start-At((card I+card J+2),SCMPDS)
by A1,Th32,A3;
hence thesis by FUNCT_4:113;
end;
end;
end;
theorem
for s being 0-started State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,J being shiftable Program of SCMPDS,a,b being Int_position,
k1 being Integer st s.DataLoc(s.a,k1)= 0 holds
IExec(if=0(a,k1,I,J),P,s).b = IExec(I,P,s).b
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable parahalting Program of
SCMPDS,J be shiftable Program of SCMPDS,a,b be Int_position, k1 be Integer;
assume
A1: s.DataLoc(s.a,k1)=0;
A2: not b in dom Start-At((card I+card J+2),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then
IExec(if=0(a,k1,I,J),P,s) = IExec(I,P,s)
+* Start-At((card I + card J + 2),SCMPDS) by A1,Th31;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,J being
halt-free parahalting shiftable Program of SCMPDS,a,b being Int_position,k1
being Integer st s.DataLoc(s.a,k1)<> 0 holds
IExec(if=0(a,k1,I,J),P,Initialize s).b = IExec(J,P,Initialize s).b
proof
let s be State of SCMPDS,I be Program of SCMPDS,J be halt-free parahalting
shiftable Program of SCMPDS,a,b be Int_position, k1 be Integer;
assume
A1: s.DataLoc(s.a,k1)<>0;
A2: not b in dom Start-At((card I+card J+2),SCMPDS) by SCMPDS_4:18;
J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
then
IExec(if=0(a,k1,I,J),P,Initialize s)
= IExec(J,P,Initialize s) +* Start-At((card I + card J
+ 2),SCMPDS) by A1,Th32;
hence thesis by A2,FUNCT_4:11;
end;
begin :: The computation of "if var=0 then block"
theorem
card if=0(a,k1,I) = card I + 1 by Th1;
theorem
0 in dom if=0(a,k1,I)
proof
set ci=card if=0(a,k1,I);
ci=card I + 1 by Th1;
hence thesis by AFINSQ_1:66;
end;
theorem
if=0(a,k1,I). 0 = (a,k1)<>0_goto (card I + 1) by Th2;
theorem Th39:
for s being State of SCMPDS, I being shiftable Program of SCMPDS
, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)= 0 & I
is_closed_on s,P & I is_halting_on s,P holds if=0(a,k1,I) is_closed_on s,P
& if=0(a,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS, I be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b = 0;
set i = (a,k1)<>0_goto (card I + 1);
set IF=if=0(a,k1,I), pIF=stop IF, pI=stop I,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
A2: IC s3 = 0 by MEMSTR_0:47;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
A4: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
for a holds s2.a = s4.a by A4,SCMPDS_2:55;
then
A5: DataPart s2 = DataPart s4 by SCMPDS_4:8;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.=0 by A1,A3,FUNCT_4:11;
then
A6: IC s4 = IC s3 + 1 by A4,SCMPDS_2:55
.= (0+1) by A2;
assume
A7: I is_closed_on s,P;
then
A8: I is_closed_on s2,P2;
assume
I is_halting_on s,P;
then
A9: P2 halts_on s2;
A10: 0 in dom pIF by COMPOS_1:36;
A11: Start-At(0,SCMPDS) c= s2 & Shift(pI,1) c= P4 by Lm6,FUNCT_4:25;
A12: stop I c= P2 by FUNCT_4:25;
A13: card pIF = card IF +1 by COMPOS_1:55
.= card I +1+1 by Th1;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A14: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s2,k1) as Nat;
A15: card pIF = card pI+1 by A13,COMPOS_1:55;
m in dom pI by A7;
then m < card pI by AFINSQ_1:66;
then
A16: m+1 < card pIF by A15,XREAL_1:6;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A14,EXTPRO_1:4
.= (m + 1) by A8,A11,A6,A5,Th22,A12;
hence IC Comput(P3,s3,k) in dom pIF by A16,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s3,k) in dom pIF by A10,A2,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P;
A17: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A17
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A8,A11,A6,A5,Th22,A12
.= halt SCMPDS by A9,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th40:
for s being State of SCMPDS,I being Program of SCMPDS, a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1)<> 0 holds if=0(a,k1,I)
is_closed_on s,P & if=0(a,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, a be Int_position,k1 be
Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b <> 0;
set i = (a,k1)<>0_goto (card I + 1);
set IF=if=0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
A2: IC s3 = 0 by MEMSTR_0:47;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
then
A5: IC s4 = ICplusConst(s3,card I + 1) by A1,A4,SCMPDS_2:55
.= (0+(card I + 1)) by A2,Th4;
A6: card IF=card I+1 by Th1;
then
A7: (card I+1) in dom pIF by COMPOS_1:64;
A8: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
pIF c= P3 by FUNCT_4:25;
then pIF c= P4;
then P4.(card I+1) = pIF.(card I+1) by A7,GRFUNC_1:2
.=halt SCMPDS by A6,COMPOS_1:64;
then
A9: CurInstr(P3,s4) = halt SCMPDS by A5,A8;
now
let k be Nat;
per cases;
suppose
0 < k;
then 1+0 <= k by INT_1:7;
hence IC Comput(P3,s3,k) in dom pIF by A7,A5,A9,EXTPRO_1:5;
end;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A2,COMPOS_1:36;
end;
end;
hence IF is_closed_on s,P;
P3 halts_on s3 by A9,EXTPRO_1:29;
hence thesis;
end;
theorem Th41:
for s being State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)=
0 & I is_closed_on s,P & I is_halting_on s,P holds
IExec(if=0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+1),SCMPDS)
proof
let s be State of SCMPDS,I be halt-free shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b = 0;
set i = (a,k1)<>0_goto (card I + 1);
set IF=if=0(a,k1,I), pI=stop I, pIF = stop IF,
s2 = Initialize s, P2 = P +* pI,
s3 = Initialize s, P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
A2: IC s3 = 0 by MEMSTR_0:47;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
A4: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.=0 by A1,A3,FUNCT_4:11;
then
A5: IC s4 = IC s3 + 1 by A4,SCMPDS_2:55
.= (0+1) by A2;
for a holds s2.a = s4.a by A4,SCMPDS_2:55;
then
A6: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
A7: I is_closed_on s,P;
then
A8: I is_closed_on s2,P2;
set SAl=Start-At((card I+1),SCMPDS);
A9: Start-At(0,SCMPDS) c= s2 & Shift(pI,1) c= P4 by Lm6,FUNCT_4:25;
A10: stop I c= P2 by FUNCT_4:25;
assume
A11: I is_halting_on s,P;
then
A12: P2 halts_on s2;
A13: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
A14: CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A13
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A8,A9,A5,A6,Th22,A10
.= halt SCMPDS by A12,EXTPRO_1:def 15;
then
A15: P3 halts_on s3 by EXTPRO_1:29;
A16: CurInstr(P3,s3) = i by Th3;
now
let l be Nat;
assume
A17: l < LifeSpan(P2,s2) + 1;
A18: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A18;
hence CurInstr(P3,Comput(P3,s3,l)) <>
halt SCMPDS by A16;
end;
suppose
l <> 0;
then consider n be Nat such that
A19: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A20: n < LifeSpan(P2,s2) by A17,A19,XREAL_1:6;
assume
A21: CurInstr(P3,Comput(P3,s3,l)) = halt SCMPDS;
A22: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s2,n)) =
CurInstr(P3,Comput(P3,s4,n)) by A8,A9,A5,A6,Th22,A10
.= halt SCMPDS by A19,A21,A22;
hence contradiction by A12,A20,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P2,s2) + 1 <= l;
then
A23: LifeSpan(P3,s3) = LifeSpan(P2,s2) + 1 by A14,A15,EXTPRO_1:def 15;
A24: DataPart Result(P2,s2) = DataPart Comput(P2, s2
,LifeSpan(P2,s2)) by A12,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s2)) by A8,A9,A5,A6,Th22,A10
.= DataPart Comput(P3, s3,LifeSpan(P2,s2) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A15,A23,EXTPRO_1:23;
A25: now
let x be object;
A26: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A27: x in dom IExec(IF,P,Initialize s);
per cases by A27,SCMPDS_4:6;
suppose
A28: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A29: not x in dom SAl by A26,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= (Result(P2,s2)).x by A24,A28,SCMPDS_4:8
.= IExec(I,P,Initialize s).x
.= (IExec(I,P,Initialize s) +* SAl).x by A29,FUNCT_4:11;
end;
suppose
A30: x = IC SCMPDS;
A31: IC Result(P2,s2) = IC IExec(I,P,Initialize s)
.= card I by A7,A11,Th25;
A32: x in dom SAl by A26,A30,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P2,s2) + 1).x by A15,A23,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s2)) by A30,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 1
by A8,A9,A5,A6,Th22,A10
.= IC Result(P2,s2) + 1 by A12,EXTPRO_1:23
.= IC Start-At((card I+1),SCMPDS) by A31,FUNCOP_1:72
.= (IExec(I,P,Initialize s) +* SAl).x by A30,A32,FUNCT_4:13;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I,P,Initialize s) +* SAl) by PARTFUN1:def 2;
hence thesis by A25,FUNCT_1:2;
end;
theorem Th42:
for s being State of SCMPDS,I being Program of SCMPDS,a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1)<> 0
holds IExec(if=0(a,k1,I),P,Initialize s) = s +* Start-At((card I+1),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS,a be Int_position, k1 be
Integer;
set b=DataLoc(s.a,k1);
set IF=if=0(a,k1,I), pIF=stop IF,
s3 = Initialize s, P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
set i = (a,k1)<>0_goto (card I + 1);
set SAl=Start-At((card I+1),SCMPDS);
A1: IC s3 = 0 by MEMSTR_0:47;
A2: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A3: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A2,FUNCT_4:11;
A4: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
assume
s.b <> 0;
then
A5: IC s4 = ICplusConst(s3,card I + 1) by A4,A3,SCMPDS_2:55
.= (0+(card I + 1)) by A1,Th4;
A6: pIF c= P4 by FUNCT_4:25;
A7: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
A8: card IF=card I+1 by Th1;
then (card I+1) in dom pIF by COMPOS_1:64;
then P4.(card I+1) = pIF.(card I+1) by A6,GRFUNC_1:2
.=halt SCMPDS by A8,COMPOS_1:64;
then
A9: CurInstr(P3,s4) = halt SCMPDS by A5,A7;
then
A10: P3 halts_on s3 by EXTPRO_1:29;
A11: CurInstr(P3,s3) = i by Th3;
now
let l be Nat;
A12: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
assume
l < 1;
then l <1+0;
then l=0 by NAT_1:13;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3) by A12;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A11;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds 1 <= l;
then LifeSpan(P3,s3) = 1 by A9,A10,EXTPRO_1:def 15;
then
A13: s4 = Result(P3,s3) by A10,EXTPRO_1:23;
A14: now
A15: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
let x be object;
assume
A16: x in dom IExec(IF,P,Initialize s);
per cases by A16,SCMPDS_4:6;
suppose
A17: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A18: not x in dom SAl by A15,TARSKI:def 1;
A19: not x in dom Start-At(0,SCMPDS) by A17,SCMPDS_4:18;
thus IExec(IF,P,Initialize s).x = s4.x by A13
.= s3.x by A4,A17,SCMPDS_2:55
.= s.x by A19,FUNCT_4:11
.= (s +* SAl).x by A18,FUNCT_4:11;
end;
suppose
A20: x = IC SCMPDS;
hence IExec(IF,P,Initialize s).x = (card I + 1) by A5,A13
.= (s +* SAl).x by A20,FUNCT_4:113;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (s +* SAl) by PARTFUN1:def 2;
hence thesis by A14,FUNCT_1:2;
end;
registration
let I be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if=0(a,k1,I) -> shiftable parahalting;
correctness
proof
set i = (a,k1)<>0_goto (card I +1);
set IF=if=0(a,k1,I);
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume
stop IF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1)= 0;
then IF is_halting_on s,P by A3,Th39;
hence P halts_on s by A1,A2;
end;
suppose
s.DataLoc(s.a,k1) <> 0;
then IF is_halting_on s,P by Th40;
hence P halts_on s by A1,A2;
end;
end;
end;
registration
let I be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if=0(a,k1,I) -> halt-free;
coherence;
end;
theorem
for s being 0-started State of SCMPDS,
I being halt-free shiftable parahalting Program of SCMPDS,
a being Int_position,k1 being Integer
holds IC IExec(if=0(a,k1,I),P,s) = card I + 1
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable parahalting Program of
SCMPDS,a be Int_position,k1 be Integer;
set IF=if=0(a,k1,I);
A1: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
A2: Initialize s = s by MEMSTR_0:44;
per cases;
suppose
s.DataLoc(s.a,k1) = 0;
then IExec(IF,P,s) =IExec(I,P,s) +* Start-At((card I+1),SCMPDS)
by A1,Th41,A2;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) <> 0;
then IExec(IF,P,s) =s +* Start-At((card I+1),SCMPDS) by Th42,A2;
hence thesis by FUNCT_4:113;
end;
end;
theorem
for s being State of SCMPDS,
I being halt-free shiftable parahalting
Program of SCMPDS,a,b being Int_position,k1 being Integer st s.DataLoc(s.a,k1)=
0 holds IExec(if=0(a,k1,I),P,Initialize s).b = IExec(I,P,Initialize s).b
proof
let s be State of SCMPDS,I be halt-free shiftable parahalting Program of
SCMPDS,a,b be Int_position,k1 be Integer;
assume
A1: s.DataLoc(s.a,k1)=0;
A2: not b in dom Start-At((card I+1),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then IExec(if=0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+1),SCMPDS)
by A1,Th41;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,a,b being
Int_position, k1 being Integer st s.DataLoc(s.a,k1)<> 0
holds IExec(if=0(a,k1,I),P,Initialize s).b = s.b
proof
let s be State of SCMPDS,I be Program of SCMPDS,a,b be Int_position, k1 be
Integer;
assume
s.DataLoc(s.a,k1)<>0;
then
A1: IExec(if=0(a,k1,I),P,Initialize s) = s +* Start-At((card I+1),SCMPDS)
by Th42;
not b in dom Start-At((card I+1),SCMPDS) by SCMPDS_4:18;
hence thesis by A1,FUNCT_4:11;
end;
Lm8: card (i ';' j ';' I)=card I+2
proof
thus card (i ';' j ';' I) =card (i ';' (j ';' I)) by SCMPDS_4:16
.=card (j ';' I)+1 by Th1
.=card I+1+1 by Th1
.=card I+2;
end;
begin :: The computation of "if var<>0 then block"
theorem
card if<>0(a,k1,I) = card I + 2 by Lm8;
Lm9: 0 in dom (i ';' j ';' I) & 1 in dom (i ';' j ';' I)
proof
set ci=card (i ';' j ';' I);
ci=card I + 2 by Lm8;
then 2 <= ci by NAT_1:11;
then 1 < ci by XXREAL_0:2;
hence thesis by AFINSQ_1:66;
end;
theorem
0 in dom if<>0(a,k1,I) & 1 in dom if<>0(a,k1,I) by Lm9;
Lm10: (i ';' j ';' I). 0=i & (i ';' j ';' I). 1=j
proof
set jI=j ';' I;
A1: i ';' j ';' I =i ';' jI by SCMPDS_4:16
.=Load i ';' jI;
0 in dom Load i by COMPOS_1:50;
hence (i ';' j ';' I). 0 =(Load i). 0 by A1,AFINSQ_1:def 3
.=i;
A2: 0 in dom Load j by COMPOS_1:50;
card jI=card I+1 by Th1;
then
A3: card Load i=1 & 0 in dom jI by AFINSQ_1:66,COMPOS_1:54;
thus (i ';' j ';' I). 1 =(Load i ';' jI). (0+1) by A1
.=jI. 0 by A3,AFINSQ_1:def 3
.=(Load j ';' I). 0
.=(Load j). 0 by A2,AFINSQ_1:def 3
.=j;
end;
theorem
if<>0(a,k1,I). 0 = (a,k1)<>0_goto 2 & if<>0(a,k1,I). 1 =
goto (card I + 1) by Lm10;
theorem Th49:
for s being State of SCMPDS, I being shiftable Program of SCMPDS
, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)<>0 & I
is_closed_on s,P & I is_halting_on s,P holds if<>0(a,k1,I) is_closed_on s,P
& if<>0(a
,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS, I be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if<>0(a,k1,I), pIF=stop IF, pI=stop I,
s2 = Initialize s, P2 = P +* pI,
s3 = Initialize s, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)<>0_goto 2, j = goto (card I + 1);
A1: IF = i ';' (j ';' I) by SCMPDS_4:16;
A2: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
for a holds s2.a = s4.a by A2,SCMPDS_2:55;
then
A3: DataPart s2 = DataPart s4 by SCMPDS_4:8;
A4: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A5: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A4,FUNCT_4:11;
A6: IC s3 = 0 by MEMSTR_0:47;
assume
s.b <> 0;
then
A7: IC s4 = ICplusConst(s3,2) by A2,A5,SCMPDS_2:55
.= (0+2) by A6,Th4;
assume
A8: I is_closed_on s,P;
then
A9: I is_closed_on s2,P2;
assume
I is_halting_on s,P;
then
A10: P2 halts_on s2;
A11: Start-At(0,SCMPDS) c= s2 & Shift(pI,2) c= P4 by Lm7,FUNCT_4:25;
A12: stop I c= P2 by FUNCT_4:25;
A13: 0 in dom pIF by COMPOS_1:36;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A14: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s2,k1) as Nat;
A15: card pIF = 1+ card IF by COMPOS_1:55
.= 1+(card I +2) by Lm8
.= 1+card I +2
.=card pI+2 by COMPOS_1:55;
m in dom pI by A8;
then m < card pI by AFINSQ_1:66;
then
A16: m+2 < card pIF by A15,XREAL_1:6;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A14,EXTPRO_1:4
.= (m + 2) by A9,A11,A7,A3,Th22,A12;
hence IC Comput(P3,s3,k) in dom pIF by A16,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s3,k) in dom pIF by A13,A6,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P;
A17: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2,
s2))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A17
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A9,A11,A7,A3,Th22,A12
.= halt SCMPDS by A10,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th50:
for s being State of SCMPDS,I being Program of SCMPDS, a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1)= 0 holds if<>0(a,k1,I)
is_closed_on s,P & if<>0(a,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, a be Int_position,k1 be
Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b = 0;
set IF=if<>0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), s5 = Comput(P3,s3,2), P4 = P3, P5 = P3;
A2: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A3: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.=0 by A1,A2,FUNCT_4:11;
A4: pIF c= P4 by FUNCT_4:25;
set i = (a,k1)<>0_goto 2, j = goto (card I + 1);
A5: IF =i ';' (j ';' I) by SCMPDS_4:16;
A6: IC s3 = 0 by MEMSTR_0:47;
Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A5,Th3;
then
A7: IC s4 = IC s3 + 1 by A3,SCMPDS_2:55
.= (0+1) by A6;
A8: 1 in dom IF by Lm9;
then 1 in dom pIF by COMPOS_1:62;
then
A9: P4. 1 = pIF. 1 by A4,GRFUNC_1:2
.=IF. 1 by A8,COMPOS_1:63
.=j by Lm10;
A10: card IF=card I+2 by Lm8;
then
A11: (card I+2) in dom pIF by COMPOS_1:64;
A12: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
Comput(P3, s3,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(j,s4) by A7,A9,A12;
then
A13: IC s5 = ICplusConst(s4,card I+1) by SCMPDS_2:54
.= (card I+1+1) by A7,Th4
.= (card I+(1+1));
A14: (P3)/.IC s5
= P3.IC s5 by PBOOLE:143;
pIF c= P5 by FUNCT_4:25;
then P5.(card I+2) = pIF.(card I+2) by A11,GRFUNC_1:2
.=halt SCMPDS by A10,COMPOS_1:64;
then
A15: CurInstr(P3,s5) = halt SCMPDS by A13,A14;
now
let k be Nat;
A16: k = 0 or 0 + 1 <= k by INT_1:7;
per cases by A16,XXREAL_0:1;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A6,COMPOS_1:36;
end;
suppose
k = 1;
hence IC Comput(P3,s3,k) in dom pIF by A8,A7,COMPOS_1:62;
end;
suppose
1 < k;
then 1+1 <= k by INT_1:7;
hence IC Comput(P3,s3,k) in dom pIF
by A11,A13,A15,EXTPRO_1:5;
end;
end;
hence IF is_closed_on s,P;
P3 halts_on s3 by A15,EXTPRO_1:29;
hence thesis;
end;
theorem Th51:
for s being State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)
<> 0 & I is_closed_on s,P & I is_halting_on s,P
holds IExec(if<>0(a,k1,I),P,Initialize s) =
IExec(I,P,Initialize s) +* Start-At((card I+2),SCMPDS)
proof
let s be State of SCMPDS,I be halt-free shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if<>0(a,k1,I), pI=stop I, pIF = stop IF,
s2 = Initialize s, P2 = P +* pI,
s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
set i = (a,k1)<>0_goto 2, j = goto (card I + 1);
set SAl=Start-At((card I+2),SCMPDS);
A1: IF=i ';' (j ';' I) by SCMPDS_4:16;
A2: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: IC s3 = 0 by MEMSTR_0:47;
A6: Start-At(0,SCMPDS) c= s2 & Shift(pI,2) c= P4 by Lm7,FUNCT_4:25;
A7: stop I c= P2 by FUNCT_4:25;
for a holds s2.a = s4.a by A2,SCMPDS_2:55;
then
A8: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
s.b <> 0;
then
A9: IC s4 = ICplusConst(s3,2) by A2,A4,SCMPDS_2:55
.= (0+2) by A5,Th4;
assume
A10: I is_closed_on s,P;
then
A11: I is_closed_on s2,P2;
assume
A12: I is_halting_on s,P;
then
A13: P2 halts_on s2;
A14: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
A15: CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A14
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A11,A6,A9,A8,Th22,A7
.= halt SCMPDS by A13,EXTPRO_1:def 15;
then
A16: P3 halts_on s3 by EXTPRO_1:29;
A17: CurInstr(P3,s3) = i by A1,Th3;
now
let l be Nat;
assume
A18: l < LifeSpan(P2,s2) + 1;
A19: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A19;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A17;
end;
suppose
l <> 0;
then consider n be Nat such that
A20: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A21: n < LifeSpan(P2,s2) by A18,A20,XREAL_1:6;
assume
A22: CurInstr(P3,Comput(P3,s3,l)) = halt SCMPDS;
A23: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s2,n)) =
CurInstr(P3,Comput(P3,s4,n)) by A11,A6,A9,A8,Th22,A7
.= halt SCMPDS by A20,A22,A23;
hence contradiction by A13,A21,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P2,s2) + 1 <= l;
then
A24: LifeSpan(P3,s3) = LifeSpan(P2,s2) + 1 by A15,A16,EXTPRO_1:def 15;
A25: DataPart Result(P2,s2) = DataPart Comput(P2, s2
,LifeSpan(P2,s2)) by A13,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s2)) by A11,A6,A9,A8,Th22,A7
.= DataPart Comput(P3, s3,LifeSpan(P2,s2) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A16,A24,EXTPRO_1:23;
A26: now
let x be object;
A27: dom Start-At((card I+2),SCMPDS) = {IC SCMPDS} by FUNCOP_1:13;
assume
A28: x in dom IExec(IF,P,Initialize 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 SAl by A27,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= (Result(P2,s2)).x by A25,A29,SCMPDS_4:8
.= IExec(I,P,Initialize s).x
.= (IExec(I,P,Initialize s) +* SAl).x by A30,FUNCT_4:11;
end;
suppose
A31: x = IC SCMPDS;
A32: IC Result(P2,s2) = IC IExec(I,P,Initialize s)
.= card I by A10,A12,Th25;
A33: x in dom SAl by A27,A31,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P2,s2) + 1).x by A16,A24,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s2)) by A31,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 2
by A11,A6,A9,A8,Th22,A7
.= IC Result(P2,s2) + 2 by A13,EXTPRO_1:23
.= IC SAl by A32,FUNCOP_1:72
.= (IExec(I,P,Initialize s) +* SAl).x by A31,A33,FUNCT_4:13;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I,P,Initialize s) +* Start-At((card I+2),SCMPDS))
by PARTFUN1:def 2;
hence thesis by A26,FUNCT_1:2;
end;
theorem Th52:
for s being State of SCMPDS,I being Program of SCMPDS,a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1)= 0
holds IExec(if<>0(a,k1,I),P,Initialize s) = s +* Start-At((card I+2),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS,a be Int_position, k1 be
Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b = 0;
set SAl=Start-At((card I+2),SCMPDS);
set i = (a,k1)<>0_goto 2, j = goto (card I + 1);
set IF=if<>0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), s5 = Comput(P3,s3,2), P4 = P3, P5 = P3;
A2: IF =i ';' (j ';' I) by SCMPDS_4:16;
A3: pIF c= P3 by FUNCT_4:25;
then
A4: pIF c= P4;
A5: pIF c= P5 by A3;
A6: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
A7: IC s3 = 0 by MEMSTR_0:47;
A8: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A2,Th3;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.=0 by A1,A6,FUNCT_4:11;
then
A9: IC s4 = IC s3 + 1 by A8,SCMPDS_2:55
.= (0+1) by A7;
A10: 1 in dom IF by Lm9;
then 1 in dom pIF by COMPOS_1:62;
then
A11: P4.1 = pIF. 1 by A4,GRFUNC_1:2
.=IF. 1 by A10,COMPOS_1:63
.=j by Lm10;
A12: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
A13: Comput(P3, s3,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(j,s4) by A9,A11,A12;
then
A14: IC s5 = ICplusConst(s4,card I+1) by SCMPDS_2:54
.= (card I+1+1) by A9,Th4
.= (card I+(1+1));
A15: (P3)/.IC s5
= P3.IC s5 by PBOOLE:143;
A16: card IF=card I+2 by Lm8;
then (card I+2) in dom pIF by COMPOS_1:64;
then P5.(card I+2) = pIF.(card I+2) by A5,GRFUNC_1:2
.=halt SCMPDS by A16,COMPOS_1:64;
then
A17: CurInstr(P3,s5) = halt SCMPDS by A14,A15;
then
A18: P3 halts_on s3 by EXTPRO_1:29;
A19: CurInstr(P3,s3) = i by A2,Th3;
now
let l be Nat;
assume
l < 1+1;
then
A20: l <= 1 by NAT_1:13;
A21: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
A22: P3/.IC Comput(P3,s3,l)
= P3.IC Comput(P3,s3,l) by PBOOLE:143;
per cases by A20,NAT_1:25;
suppose
l=0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A21;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A19;
end;
suppose
l=1;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A9,A11,A22;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds 2 <= l;
then LifeSpan(P3,s3) = 2 by A17,A18,EXTPRO_1:def 15;
then
A23: s5 = Result(P3,s3) by A18,EXTPRO_1:23;
A24: now
A25: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
let x be object;
assume
A26: x in dom IExec(IF,P,Initialize s);
per cases by A26,SCMPDS_4:6;
suppose
A27: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A28: not x in dom SAl by A25,TARSKI:def 1;
A29: not x in dom Start-At(0,SCMPDS) by A27,SCMPDS_4:18;
thus IExec(IF,P,Initialize s).x = s5.x by A23
.= s4.x by A13,A27,SCMPDS_2:54
.= s3.x by A8,A27,SCMPDS_2:55
.= s.x by A29,FUNCT_4:11
.= (s +* SAl).x by A28,FUNCT_4:11;
end;
suppose
A30: x = IC SCMPDS;
hence IExec(IF,P,Initialize s).x = (card I + 2) by A14,A23
.= (s +* Start-At((card I+2),SCMPDS)).x by A30,FUNCT_4:113;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (s +* SAl) by PARTFUN1:def 2;
hence thesis by A24,FUNCT_1:2;
end;
registration
let I be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if<>0(a,k1,I) -> shiftable parahalting;
correctness
proof
set i = (a,k1)<>0_goto 2, j = goto (card I + 1);
set IF=if<>0(a,k1,I), pIF = stop IF;
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume pIF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1)<>0;
then IF is_halting_on s,P by A3,Th49;
hence P halts_on s by A1,A2;
end;
suppose
s.DataLoc(s.a,k1) = 0;
then IF is_halting_on s,P by Th50;
hence P halts_on s by A1,A2;
end;
end;
end;
registration
let I be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if<>0(a,k1,I) -> halt-free;
coherence;
end;
theorem
for s being State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,a being Int_position,k1 being Integer
holds IC IExec(if<>0(a,k1,I),P,Initialize s) = card I + 2
proof
let s be State of SCMPDS,I be halt-free shiftable parahalting Program of
SCMPDS,a be Int_position,k1 be Integer;
set IF=if<>0(a,k1,I);
A1: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) <> 0;
then IExec(IF,P,Initialize s) =IExec(I,P,Initialize s)
+* Start-At((card I+2),SCMPDS)
by A1,Th51;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) = 0;
then IExec(IF,P,Initialize s) =s +* Start-At((card I+2),SCMPDS) by Th52;
hence thesis by FUNCT_4:113;
end;
end;
theorem
for s being State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,a,b being Int_position,k1 being Integer st s.DataLoc(s.a,k1)
<> 0 holds IExec(if<>0(a,k1,I),P,Initialize s).b
= IExec(I,P,Initialize s).b
proof
let s be State of SCMPDS,I be halt-free shiftable parahalting Program of
SCMPDS,a,b be Int_position,k1 be Integer;
assume
A1: s.DataLoc(s.a,k1)<>0;
A2: not b in dom Start-At((card I+2),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then IExec(if<>0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+2),SCMPDS)
by A1,Th51;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,a,b being
Int_position, k1 being Integer st s.DataLoc(s.a,k1)= 0
holds IExec(if<>0(a,k1,I),P,Initialize s).b = s.b
proof
let s be State of SCMPDS,I be Program of SCMPDS,a,b be Int_position, k1 be
Integer;
assume
s.DataLoc(s.a,k1)=0;
then
A1: IExec(if<>0(a,k1,I),P,Initialize s)
= s +* Start-At((card I+2),SCMPDS) by Th52;
not b in dom Start-At((card I+2),SCMPDS) by SCMPDS_4:18;
hence thesis by A1,FUNCT_4:11;
end;
begin :: The computation of "if var>0 then block1 else block2"
theorem
card if>0(a,k1,I,J) = card I + card J + 2 by Lm4;
theorem
0 in dom if>0(a,k1,I,J) & 1 in dom if>0(a,k1,I,J)
proof
set ci=card if>0(a,k1,I,J);
ci=card I + card J +2 by Lm4;
then 2 <= ci by NAT_1:12;
then 1 < ci by XXREAL_0:2;
hence thesis by AFINSQ_1:66;
end;
theorem
if>0(a,k1,I,J). 0 = (a,k1)<=0_goto (card I + 2) by Lm5;
theorem Th59:
for s being 0-started State of SCMPDS, I,J being shiftable Program of
SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)>0 & I
is_closed_on s,P & I is_halting_on s,P holds if>0(a,k1,I,J) is_closed_on s,P
& if>0(a,k1,I,J) is_halting_on s,P
proof
let s be 0-started State of SCMPDS, I,J be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set G=Goto (card J+1);
set I2 = I ';' G ';' J, IF=if>0(a,k1,I,J), pIF=stop IF,
pI2=stop I2, s2 = Initialize s, P2 = P +* pI2,
P3 = P +* pIF,
s4 = Comput(P3,s,1), P4 = P3;
set i = (a,k1)<=0_goto (card I + 2);
A1: 0 in dom pIF by COMPOS_1:36;
A2: Initialize s = s by MEMSTR_0:44;
then
A3: IC s = 0 by MEMSTR_0:47;
A4: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' I2 by SCMPDS_4:14;
then
A5: Shift(pI2,1) c= P4 by Lm6;
A6: Comput(P3, s,0 + 1) = Following(P3,Comput(P3,s,0)) by EXTPRO_1:3
.= Following(P3,s) by EXTPRO_1:2
.= Exec(i,s) by A4,Th3,A2;
for a holds s2.a = s4.a by A6,A2,SCMPDS_2:56;
then
A7: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
s.b > 0;
then
A8: IC s4 = IC s + 1 by A6,SCMPDS_2:56
.= (0+1) by A3;
assume
A9: I is_closed_on s,P;
assume
A10: I is_halting_on s,P;
then
A11: I2 is_closed_on s,P by A9,Th21;
then
A12: Start-At(0,SCMPDS) c= s2 & I2 is_closed_on s2,P2 by FUNCT_4:25;
A13: stop I2 c= P2 by FUNCT_4:25;
I2 is_halting_on s,P by A9,A10,Th21;
then
A14: P2 halts_on s2;
A15: card pIF = card IF +1 by COMPOS_1:55
.= card I2 +1+1 by A4,Th1;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A16: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s2,k1) as Nat;
A17: card pIF = card pI2+1 by A15,COMPOS_1:55;
m in dom pI2 by A11;
then m < card pI2 by AFINSQ_1:66;
then
A18: m+1 < card pIF by A17,XREAL_1:6;
IC Comput(P3,s,k) = IC Comput(P3, s4,k1) by A16,EXTPRO_1:4
.= (m + 1) by A12,A5,A8,A7,Th22,A13;
hence IC Comput(P3,s,k) in dom pIF by A18,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s,k) in dom pIF by A1,A3,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P by A2;
A19: Comput(P3,s,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s,1),LifeSpan(P2,s2)) by EXTPRO_1:4;
CurInstr(P3,Comput(P3,s,LifeSpan(P2,s2)+1))
=CurInstr(P3,Comput(P3,s4,LifeSpan(P2,s2))) by A19
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A12,A5,A8,A7,Th22,A13
.= halt SCMPDS by A14,EXTPRO_1:def 15;
then P3 halts_on s by EXTPRO_1:29;
hence thesis by A2;
end;
theorem Th60:
for s being State of SCMPDS,I being Program of SCMPDS,J being
shiftable Program of SCMPDS,a being Int_position,k1 being Integer st s.DataLoc(
s.a,k1) <= 0 & J is_closed_on s,P & J is_halting_on s,P holds if>0(a,k1,I,J)
is_closed_on s,P & if>0(a,k1,I,J) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, J be shiftable Program of
SCMPDS, a be Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set pJ=stop J, s1 = Initialize s, P1 = P +* pJ,
IF=if>0(a,k1,I,J), pIF=
stop IF, s3 = Initialize s, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)<=0_goto (card I + 2);
set G =Goto (card J+1), iG=i ';' I ';' G;
A1: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' (I ';' G ';' J) by SCMPDS_4:14;
A2: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: IC s3 = 0 by MEMSTR_0:47;
assume
s.b <= 0;
then
A6: IC s4 = ICplusConst(s3,card I + 2) by A2,A4,SCMPDS_2:56
.= (0+(card I + 2)) by A5,Th4;
assume
A7: J is_closed_on s,P;
then
A8: Start-At(0,SCMPDS) c= s1 & J is_closed_on s1,P1 by FUNCT_4:25;
A9: stop J c= P1 by FUNCT_4:25;
A10: pIF c= P3 by FUNCT_4:25;
A11: card iG = card (i ';' I) + card G by AFINSQ_1:17
.=card (i ';' I) + 1 by COMPOS_1:54
.=card I +1 +1 by Th1
.=card I +(1 +1);
then Shift(pJ,card I+2) c= pIF by Th5;
then
A12: Shift(pJ,card I+2) c= P4 by A10,XBOOLE_1:1;
assume
J is_halting_on s,P;
then
A13: P1 halts_on s1;
for a holds s1.a = s4.a by A2,SCMPDS_2:56;
then
A14: DataPart s1 = DataPart s4 by SCMPDS_4:8;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A15: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P1, s1,k1) as Nat;
m in dom pJ by A7;
then m < card pJ by AFINSQ_1:66;
then
A16: m + (card I + 2) < card pJ + (card I + 2) by XREAL_1:6;
A17: card pJ = card J + 1 by COMPOS_1:55;
A18: card pIF = card IF+1 by COMPOS_1:55
.=card I +2 +card J +1 by A11,AFINSQ_1:17
.=card I +2 + card pJ by A17;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A15,EXTPRO_1:4
.= (m + (card I + 2)) by A8,A14,A12,A6,Th22,A9;
hence IC Comput(P3,s3,k) in dom pIF by A18,A16,AFINSQ_1:66;
end;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A5,COMPOS_1:36;
end;
end;
hence IF is_closed_on s,P;
A19: Comput(P3,s3,LifeSpan(P1,s1)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P1
,s1))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P1,s1)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P1,s1))) by A19
.=CurInstr(P1,
Comput(P1,s1,LifeSpan(P1,s1))) by A8,A14,A12,A6,Th22,A9
.= halt SCMPDS by A13,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th61:
for s being 0-started State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, J being shiftable Program of SCMPDS,a being Int_position,k1
being Integer st s.DataLoc(s.a,k1) > 0 & I is_closed_on s,P &
I is_halting_on s,P
holds IExec(if>0(a,k1,I,J),P,s) = IExec(I,P,s)
+* Start-At((card I + card J + 2),SCMPDS)
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, J be
shiftable Program of SCMPDS,a be Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set G=Goto (card J+1);
set I2 = I ';' G ';' J, IF=if>0(a,k1,I,J), pIF = stop IF,
pI2= stop I2, P2 = P +* pI2,
P3 = P +* pIF, s4 = Comput(P3,s,1), P4 = P3;
set i = (a,k1)<=0_goto (card I + 2);
set SAl= Start-At((card I+card J+2),SCMPDS);
A1: Initialize s = s by MEMSTR_0:44;
then
A2: IC s = 0 by MEMSTR_0:47;
A3: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' I2 by SCMPDS_4:14;
then
A4: Shift(pI2,1) c= P4 by Lm6;
A5: Comput(P3, s,0 + 1) = Following(P3,Comput(P3,s,0)) by EXTPRO_1:3
.= Following(P3,s) by EXTPRO_1:2
.= Exec(i,s) by A3,Th3,A1;
assume
s.b > 0;
then
A6: IC s4 = IC s + 1 by A5,SCMPDS_2:56
.= (0+1) by A2;
for a holds s.a = s4.a by A5,SCMPDS_2:56;
then
A7: DataPart s = DataPart s4 by SCMPDS_4:8;
assume
A8: I is_closed_on s,P;
assume
A9: I is_halting_on s,P;
then I2 is_halting_on s,P by A8,Th21;
then
A10: P2 halts_on s by A1;
I2 is_closed_on s,P by A8,A9,Th21;
then
A11: Start-At(0,SCMPDS) c= s & I2 is_closed_on s,P2 by A1,FUNCT_4:25;
A12: stop I2 c= P2 by FUNCT_4:25;
A13: Comput(P3,s,LifeSpan(P2,s)+1)
= Comput(P3,Comput(P3,s,1),LifeSpan(P2,
s))
by EXTPRO_1:4;
A14: CurInstr(P3,
Comput(P3,s,LifeSpan(P2,s)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s))) by A13
.=CurInstr(P2,
Comput(P2,s,LifeSpan(P2,s))) by A11,A4,A6,A7,Th22,A12
.= halt SCMPDS by A10,EXTPRO_1:def 15;
then
A15: P3 halts_on s by EXTPRO_1:29;
A16: CurInstr(P3,s) = i by A3,Th3,A1;
now
let l be Nat;
assume
A17: l < LifeSpan(P2,s) + 1;
A18: Comput(P3,s,0) = s by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s,l))
= CurInstr(P3,s)
by A18;
hence CurInstr(P3,Comput(P3,s,l))
<> halt SCMPDS by A16;
end;
suppose
l <> 0;
then consider n be Nat such that
A19: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A20: n < LifeSpan(P2,s) by A17,A19,XREAL_1:6;
assume
A21: CurInstr(P3,Comput(P3,s,l)) = halt SCMPDS;
A22: Comput(P3,s,n+1)
= Comput(P3,Comput(P3,s,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s,n)) =
CurInstr(P3,Comput(P3,s4,n)) by A11,A4,A6,A7,Th22,A12
.= halt SCMPDS by A19,A21,A22;
hence contradiction by A10,A20,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s,l)) = halt SCMPDS
holds LifeSpan(P2,s) + 1 <= l;
then
A23: LifeSpan(P3,s) = LifeSpan(P2,s) + 1 by A14,A15,EXTPRO_1:def 15;
A24: DataPart Result(P2,s) = DataPart Comput(P2, s
,LifeSpan(P2,s)) by A10,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s))
by A11,A4,A6,A7,Th22,A12
.= DataPart Comput(P3, s,LifeSpan(P2,s) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s) by A15,A23,EXTPRO_1:23;
A25: now
let x be object;
A26: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A27: x in dom IExec(IF,P,s);
per cases by A27,SCMPDS_4:6;
suppose
A28: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A29: not x in dom SAl by A26,TARSKI:def 1;
thus IExec(IF,P,s).x = (Result(P3,s)).x
.= (Result(P2,s)).x by A24,A28,SCMPDS_4:8
.= IExec(I2,P,s).x
.= (IExec(I2,P,s) +* SAl).x by A29,FUNCT_4:11;
end;
suppose
A30: x = IC SCMPDS;
A31: IC Result(P2,s) = IC IExec(I2,P,s)
.= (card I + card J + 1) by A8,A9,Th23;
A32: x in dom SAl by A26,A30,TARSKI:def 1;
thus IExec(IF,P,s).x = (Result(P3,s)).x
.= Comput(P3, s,LifeSpan(P2,s) + 1).x by A15,A23,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s)) by A30,EXTPRO_1:4
.= IC Comput(P2, s,LifeSpan(P2,s)) + 1 by A11,A4,A6,A7,Th22,A12
.= IC Result(P2,s) + 1 by A10,EXTPRO_1:23
.= IC Start-At(((card I + card J + 1) + 1),SCMPDS) by A31,FUNCOP_1:72
.= (IExec(I2,P,s) +* SAl).x by A30,A32,FUNCT_4:13;
end;
end;
dom IExec(IF,P,s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I2,P,s) +* SAl) by PARTFUN1:def 2;
hence IExec(IF,P,s) = IExec(I2,P,s) +* SAl
by A25,FUNCT_1:2
.= IExec(I,P,s) +* Start-At((card I + card J + 1),SCMPDS) +*
Start-At(
(card I + card J + 2),SCMPDS) by A8,A9,Th24
.= IExec(I,P,s) +* SAl by MEMSTR_0:36;
end;
theorem Th62:
for s being 0-started State of SCMPDS,I being Program of SCMPDS,J being
halt-free shiftable Program of SCMPDS,a being Int_position,k1 being Integer
st s.DataLoc(s.a,k1) <= 0 & J is_closed_on s,P & J is_halting_on s,P
holds IExec(if>0(a,k1,I,J),P,s)
= IExec(J,P,s) +* Start-At((card I+card J+2),SCMPDS)
proof
let s be 0-started State of SCMPDS,I be Program of SCMPDS,
J be halt-free shiftable
Program of SCMPDS,a be Int_position,k1 be Integer;
A1: Initialize s = s by MEMSTR_0:44;
set b=DataLoc(s.a,k1);
set pJ=stop J, s1 = s, P1 = P +* pJ,
IF=if>0(a,k1,I,J), pIF=
stop IF, s3 = s, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)<=0_goto (card I + 2);
set G =Goto (card J+1), iG=i ';' I ';' G;
set SAl=Start-At((card I+card J+2),SCMPDS);
A2: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' (I ';' G ';' J) by SCMPDS_4:14;
A3: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A2,Th3,A1;
A4: IC s3 = 0 by A1,MEMSTR_0:47;
assume
s.b <= 0;
then
A5: IC s4 = ICplusConst(s3,card I + 2) by A3,SCMPDS_2:56
.= (0+(card I + 2)) by A4,Th4;
for a holds s1.a= s4.a by A3,SCMPDS_2:56;
then
A6: DataPart s1 = DataPart s4 by SCMPDS_4:8;
card iG = card (i ';' I) + card G by AFINSQ_1:17
.=card (i ';' I) + 1 by COMPOS_1:54
.=card I +1 +1 by Th1
.=card I +(1 +1);
then
A7: Shift(pJ,card I+2) c= pIF by Th5;
pIF c= P3 by FUNCT_4:25;
then
A8: Shift(pJ,card I+2) c= P4 by A7,XBOOLE_1:1;
assume
A9: J is_closed_on s,P;
then
A10: Start-At(0,SCMPDS) c= s1 & J is_closed_on s1,P1 by A1,FUNCT_4:25;
A11: stop J c= P1 by FUNCT_4:25;
assume
A12: J is_halting_on s,P;
then
A13: P1 halts_on s1 by A1;
A14: Comput(P3,s3,LifeSpan(P1,s1)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P1
,s1))
by EXTPRO_1:4;
A15: CurInstr(P3,
Comput(P3,s3,LifeSpan(P1,s1)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P1,s1))) by A14
.=CurInstr(P1,
Comput(P1,s1,LifeSpan(P1,s1))) by A10,A8,A5,A6,Th22,A11
.= halt SCMPDS by A13,EXTPRO_1:def 15;
then
A16: P3 halts_on s3 by EXTPRO_1:29;
A17: CurInstr(P3,s3) = i by A2,Th3,A1;
now
let l be Nat;
assume
A18: l < LifeSpan(P1,s1) + 1;
A19: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A19;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A17;
end;
suppose
l <> 0;
then consider n be Nat such that
A20: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A21: n < LifeSpan(P1,s1) by A18,A20,XREAL_1:6;
assume
A22: CurInstr(P3,Comput(P3,s3,l)) = halt SCMPDS;
A23: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P1,Comput(P1,s1,n))
= CurInstr(P3,
Comput(P3,s4,n)) by A10,A8,A5,A6,Th22,A11
.= halt SCMPDS by A20,A22,A23;
hence contradiction by A13,A21,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P1,s1) + 1 <= l;
then
A24: LifeSpan(P3,s3) = LifeSpan(P1,s1) + 1 by A15,A16,EXTPRO_1:def 15;
A25: DataPart Result(P1,s1) = DataPart Comput(P1, s1
,LifeSpan(P1,s1)) by A13,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P1,s1))
by A10,A8,A5,A6,Th22,A11
.= DataPart Comput(P3, s3,LifeSpan(P1,s1) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A16,A24,EXTPRO_1:23;
A26: now
let x be object;
A27: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A28: x in dom IExec(IF,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 SAl by A27,TARSKI:def 1;
thus IExec(IF,P,s).x = (Result(P3,s3)).x
.= (Result(P1,s1)).x by A25,A29,SCMPDS_4:8
.= IExec(J,P,s).x
.= (IExec(J,P,s) +* SAl).x by A30,FUNCT_4:11;
end;
suppose
A31: x = IC SCMPDS;
A32: IC Result(P1,s1) = IC IExec(J,P,s)
.= (card J) by A9,A12,Th25,A1;
A33: x in dom SAl by A27,A31,TARSKI:def 1;
thus IExec(IF,P,s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P1,s1) + 1).x by A16,A24,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P1,s1)) by A31,EXTPRO_1:4
.= IC Comput(P1, s1,LifeSpan(P1,s1)) + (card
I + 2) by A10,A8,A5,A6,Th22,A11
.= IC Result(P1,s1) + (card I + 2) by A13,EXTPRO_1:23
.= IC Start-At (card J + (card I + 2),SCMPDS) by A32,FUNCOP_1:72
.= (IExec(J,P,s) +* SAl).x by A31,A33,FUNCT_4:13;
end;
end;
dom IExec(IF,P,s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(J,P,s) +* SAl) by PARTFUN1:def 2;
hence thesis by A26,FUNCT_1:2;
end;
registration
let I,J be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if>0(a,k1,I,J) -> shiftable parahalting;
correctness
proof
set i = (a,k1)<=0_goto (card I + 2), G =Goto (card J+1);
set IF=if>0(a,k1,I,J), pIF = stop IF;
reconsider IJ=I ';' G ';' J as shiftable Program of SCMPDS;
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume pIF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
A4: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) > 0;
then IF is_halting_on s,P by A4,Th59;
hence P halts_on s by A1,A2;
end;
suppose
s.DataLoc(s.a,k1) <= 0;
then IF is_halting_on s,P by A3,Th60;
hence P halts_on s by A1,A2;
end;
end;
end;
registration
let I,J be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if>0(a,k1,I,J) -> halt-free;
coherence;
end;
theorem
for s being 0-started State of SCMPDS,I,J being halt-free shiftable
parahalting Program of SCMPDS,a being Int_position,k1 being Integer holds IC
IExec(if>0(a,k1,I,J),P,s) = card I + card J + 2
proof
let s be 0-started State of SCMPDS,
I,J be halt-free shiftable parahalting Program of SCMPDS,
a be Int_position,k1 be Integer;
set IF=if>0(a,k1,I,J);
A1: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
A2: J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) > 0;
then IExec(IF,P,s) = IExec(I,P,s) +* Start-At((card I+card J+2),SCMPDS)
by A1,Th61;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) <= 0;
then IExec(IF,P,s) = IExec(J,P,s) +* Start-At((card I+card J+2),SCMPDS)
by A2,Th62;
hence thesis by FUNCT_4:113;
end;
end;
theorem
for s being 0-started State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,J being shiftable Program of SCMPDS,a,b being Int_position,
k1 being Integer st s.DataLoc(s.a,k1)>0 holds
IExec(if>0(a,k1,I,J),P,s).b = IExec(I,P,s).b
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable parahalting Program of
SCMPDS,J be shiftable Program of SCMPDS,a,b be Int_position, k1 be Integer;
assume
A1: s.DataLoc(s.a,k1)>0;
A2: not b in dom Start-At((card I+card J+2),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then
IExec(if>0(a,k1,I,J),P,s) = IExec(I,P,s)
+* Start-At((card I + card J + 2),SCMPDS) by A1,Th61;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being 0-started State of SCMPDS,I being Program of SCMPDS,J being
halt-free parahalting shiftable Program of SCMPDS,a,b being Int_position,k1
being Integer st s.DataLoc(s.a,k1) <= 0 holds
IExec(if>0(a,k1,I,J),P,s).b = IExec(J,P,s).b
proof
let s be 0-started State of SCMPDS,I be Program of SCMPDS,
J be halt-free parahalting
shiftable Program of SCMPDS,a,b be Int_position, k1 be Integer;
set IF=if>0(a,k1,I,J);
assume
A1: s.DataLoc(s.a,k1) <= 0;
A2: not b in dom Start-At((card I+card J+2),SCMPDS) by SCMPDS_4:18;
J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
then IExec(IF,P,s) =IExec(J,P,s) +* Start-At((card I+card J+2),SCMPDS)
by A1,Th62;
hence thesis by A2,FUNCT_4:11;
end;
begin :: The computation of "if var>0 then block"
theorem
card if>0(a,k1,I) = card I + 1 by Th1;
theorem
0 in dom if>0(a,k1,I)
proof
set ci=card if>0(a,k1,I);
ci=card I + 1 by Th1;
hence thesis by AFINSQ_1:66;
end;
theorem
if>0(a,k1,I). 0 = (a,k1)<=0_goto (card I + 1) by Th2;
theorem Th69:
for s being State of SCMPDS, I being shiftable Program of SCMPDS
, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)> 0 & I
is_closed_on s,P & I is_halting_on s,P holds if>0(a,k1,I) is_closed_on s,P
& if>0(a,
k1,I) is_halting_on s,P
proof
let s be State of SCMPDS, I be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if>0(a,k1,I), pIF=stop IF, pI=stop I,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)<=0_goto (card I + 1);
A1: 0 in dom pIF by COMPOS_1:36;
A2: IC s3 = 0 by MEMSTR_0:47;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
for a holds s2.a = s4.a by A5,SCMPDS_2:56;
then
A6: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
s.b > 0;
then
A7: IC s4 = IC s3 + 1 by A5,A4,SCMPDS_2:56
.= (0+1) by A2;
assume
A8: I is_closed_on s,P;
then
A9: I is_closed_on s2,P2;
assume
I is_halting_on s,P;
then
A10: P2 halts_on s2;
A11: Start-At(0,SCMPDS) c= s2 & Shift(pI,1) c= P4 by Lm6,FUNCT_4:25;
A12: stop I c= P2 by FUNCT_4:25;
A13: card pIF = card IF +1 by COMPOS_1:55
.= card I +1+1 by Th1;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A14: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s2,k1) as Nat;
A15: card pIF = card pI+1 by A13,COMPOS_1:55;
m in dom pI by A8;
then m < card pI by AFINSQ_1:66;
then
A16: m+1 < card pIF by A15,XREAL_1:6;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A14,EXTPRO_1:4
.= (m + 1) by A9,A11,A7,A6,Th22,A12;
hence IC Comput(P3,s3,k) in dom pIF by A16,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s3,k) in dom pIF by A1,A2,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P;
A17: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,Comput(P3,s4,LifeSpan(P2,s2))) by A17
.=CurInstr(P2,Comput(P2,s2,LifeSpan(P2,s2))) by A9,A11,A7,A6,Th22,A12
.= halt SCMPDS by A10,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th70:
for s being State of SCMPDS,I being Program of SCMPDS, a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) <= 0 holds if>0(a,k1,I)
is_closed_on s,P & if>0(a,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, a be Int_position,k1 be
Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b <= 0;
set i = (a,k1)<=0_goto (card I + 1);
set IF=if>0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
A2: IC s3 = 0 by MEMSTR_0:47;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
then
A5: IC s4 = ICplusConst(s3,card I + 1) by A1,A4,SCMPDS_2:56
.= (0+(card I + 1)) by A2,Th4;
A6: card IF=card I+1 by Th1;
then
A7: (card I+1) in dom pIF by COMPOS_1:64;
A8: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
pIF c= P3 by FUNCT_4:25;
then pIF c= P4;
then P4.(card I+1) = pIF.(card I+1) by A7,GRFUNC_1:2
.=halt SCMPDS by A6,COMPOS_1:64;
then
A9: CurInstr(P3,s4) = halt SCMPDS by A5,A8;
now
let k be Nat;
per cases;
suppose
0 < k;
then 1+0 <= k by INT_1:7;
hence IC Comput(P3,s3,k) in dom pIF by A7,A5,A9,EXTPRO_1:5;
end;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A2,COMPOS_1:36;
end;
end;
hence IF is_closed_on s,P;
P3 halts_on s3 by A9,EXTPRO_1:29;
hence thesis;
end;
theorem Th71:
for s being State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)>
0 & I is_closed_on s,P & I is_halting_on s,P
holds IExec(if>0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+1),SCMPDS)
proof
let s be State of SCMPDS,I be halt-free shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if>0(a,k1,I), pI=stop I, pIF = stop IF,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
set i = (a,k1)<=0_goto (card I + 1);
set SAl=Start-At((card I+1),SCMPDS);
A1: IC s3 = 0 by MEMSTR_0:47;
A2: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A3: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A2,FUNCT_4:11;
A4: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
assume
s.b > 0;
then
A5: IC s4 = IC s3 + 1 by A4,A3,SCMPDS_2:56
.= (0+1) by A1;
for a holds s2.a = s4.a by A4,SCMPDS_2:56;
then
A6: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
A7: I is_closed_on s,P;
then
A8: I is_closed_on s2,P2;
A9: Start-At(0,SCMPDS) c= s2 & Shift(pI,1) c= P4 by Lm6,FUNCT_4:25;
A10: stop I c= P2 by FUNCT_4:25;
assume
A11: I is_halting_on s,P;
then
A12: P2 halts_on s2;
A13: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2,s2))
by EXTPRO_1:4;
A14: CurInstr(P3,Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,Comput(P3,s4,LifeSpan(P2,s2))) by A13
.=CurInstr(P2,Comput(P2,s2,LifeSpan(P2,s2))) by A8,A9,A5,A6,Th22,A10
.= halt SCMPDS by A12,EXTPRO_1:def 15;
then
A15: P3 halts_on s3 by EXTPRO_1:29;
A16: CurInstr(P3,s3) = i by Th3;
now
let l be Nat;
assume
A17: l < LifeSpan(P2,s2) + 1;
A18: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A18;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A16;
end;
suppose
l <> 0;
then consider n be Nat such that
A19: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A20: n < LifeSpan(P2,s2) by A17,A19,XREAL_1:6;
assume
A21: CurInstr(P3,Comput(P3,
s3,l)) = halt SCMPDS;
A22: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s2,n)) =
CurInstr(P3,Comput(P3,s4,n)) by A8,A9,A5,A6,Th22,A10
.= halt SCMPDS by A19,A21,A22;
hence contradiction by A12,A20,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P2,s2) + 1 <= l;
then
A23: LifeSpan(P3,s3) = LifeSpan(P2,s2) + 1 by A14,A15,EXTPRO_1:def 15;
A24: DataPart Result(P2,s2) = DataPart Comput(P2,s2,
LifeSpan(P2,s2)) by A12,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s2)) by A8,A9,A5,A6,Th22,A10
.= DataPart Comput(P3, s3,LifeSpan(P2,s2) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A15,A23,EXTPRO_1:23;
A25: now
let x be object;
A26: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A27: x in dom IExec(IF,P,Initialize s);
per cases by A27,SCMPDS_4:6;
suppose
A28: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A29: not x in dom SAl by A26,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= (Result(P2,s2)).x by A24,A28,SCMPDS_4:8
.= IExec(I,P,Initialize s).x
.= (IExec(I,P,Initialize s) +* SAl).x by A29,FUNCT_4:11;
end;
suppose
A30: x = IC SCMPDS;
A31: IC Result(P2,s2) = IC IExec(I,P,Initialize s)
.= card I by A7,A11,Th25;
A32: x in dom SAl by A26,A30,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P2,s2) + 1).x by A15,A23,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s2)) by A30,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 1
by A8,A9,A5,A6,Th22,A10
.= IC Result(P2,s2) + 1 by A12,EXTPRO_1:23
.= IC SAl by A31,FUNCOP_1:72
.= (IExec(I,P,Initialize s) +* SAl).x by A30,A32,FUNCT_4:13;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I,P,Initialize s) +* SAl) by PARTFUN1:def 2;
hence thesis by A25,FUNCT_1:2;
end;
theorem Th72:
for s being State of SCMPDS,I being Program of SCMPDS,a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) <= 0
holds IExec(if>0(a,k1,I),P,Initialize s) = s +* Start-At((card I+1),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS,a be Int_position, k1 be
Integer;
set b=DataLoc(s.a,k1);
set IF=if>0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
set i = (a,k1)<=0_goto (card I + 1);
set SAl=Start-At((card I+1),SCMPDS);
A1: IC s3 = 0 by MEMSTR_0:47;
A2: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A3: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A2,FUNCT_4:11;
A4: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
assume
s.b <= 0;
then
A5: IC s4 = ICplusConst(s3,card I + 1) by A4,A3,SCMPDS_2:56
.= (0+(card I + 1)) by A1,Th4;
pIF c= P3 by FUNCT_4:25;
then
A6: pIF c= P4;
A7: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
A8: card IF=card I+1 by Th1;
then (card I+1) in dom pIF by COMPOS_1:64;
then P4.(card I+1) = pIF.(card I+1) by A6,GRFUNC_1:2
.=halt SCMPDS by A8,COMPOS_1:64;
then
A9: CurInstr(P3,s4) = halt SCMPDS by A5,A7;
then
A10: P3 halts_on s3 by EXTPRO_1:29;
A11: CurInstr(P3,s3) = i by Th3;
now
let l be Nat;
A12: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
assume
l < 1;
then l <1+0;
then l=0 by NAT_1:13;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3) by A12;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A11;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds 1 <= l;
then LifeSpan(P3,s3) = 1 by A9,A10,EXTPRO_1:def 15;
then
A13: s4 = Result(P3,s3) by A10,EXTPRO_1:23;
A14: now
A15: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
let x be object;
assume
A16: x in dom IExec(IF,P,Initialize s);
per cases by A16,SCMPDS_4:6;
suppose
A17: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A18: not x in dom SAl by A15,TARSKI:def 1;
A19: not x in dom Start-At(0,SCMPDS) by A17,SCMPDS_4:18;
thus IExec(IF,P,Initialize s).x = s4.x by A13
.= s3.x by A4,A17,SCMPDS_2:56
.= s.x by A19,FUNCT_4:11
.= (s +* SAl).x by A18,FUNCT_4:11;
end;
suppose
A20: x = IC SCMPDS;
hence IExec(IF,P,Initialize s).x = (card I + 1) by A5,A13
.= (s +* SAl).x by A20,FUNCT_4:113;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (s +* SAl) by PARTFUN1:def 2;
hence thesis by A14,FUNCT_1:2;
end;
registration
let I be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if>0(a,k1,I) -> shiftable parahalting;
correctness
proof
set i = (a,k1)<=0_goto (card I +1);
set IF=if>0(a,k1,I), pIF = stop IF;
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume pIF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) > 0;
then IF is_halting_on s,P by A3,Th69;
hence P halts_on s by A2,A1;
end;
suppose
s.DataLoc(s.a,k1) <= 0;
then IF is_halting_on s,P by Th70;
hence P halts_on s by A2,A1;
end;
end;
end;
registration
let I be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if>0(a,k1,I) -> halt-free;
coherence;
end;
theorem
for s being 0-started State of SCMPDS,
I being halt-free shiftable parahalting Program of SCMPDS,
a being Int_position,k1 being Integer
holds IC IExec(if>0(a,k1,I),P,s) = card I + 1
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable parahalting Program of
SCMPDS,a be Int_position,k1 be Integer;
set IF=if>0(a,k1,I);
A1: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
A2: Initialize s = s by MEMSTR_0:44;
per cases;
suppose
s.DataLoc(s.a,k1) > 0;
then IExec(IF,P,s) =IExec(I,P,s) +* Start-At((card I+1),SCMPDS)
by A1,Th71,A2;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) <= 0;
then IExec(IF,P,s) =s +* Start-At((card I+1),SCMPDS) by Th72,A2;
hence thesis by FUNCT_4:113;
end;
end;
theorem
for s being State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,a,b being Int_position,k1 being Integer st s.DataLoc(s.a,k1)>
0 holds IExec(if>0(a,k1,I),P,Initialize s).b = IExec(I,P,Initialize s).b
proof
let s be State of SCMPDS,I be halt-free shiftable parahalting Program of
SCMPDS,a,b be Int_position,k1 be Integer;
assume
A1: s.DataLoc(s.a,k1) > 0;
A2: not b in dom Start-At((card I+1),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then IExec(if>0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+1),SCMPDS)
by A1,Th71;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,a,b being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) <= 0
holds IExec(if>0(a,k1,I),P,Initialize s).b = s.b
proof
let s be State of SCMPDS,I be Program of SCMPDS,a,b be Int_position, k1 be
Integer;
assume
s.DataLoc(s.a,k1) <= 0;
then
A1: IExec(if>0(a,k1,I),P,Initialize s) = s +* Start-At((card I+1),SCMPDS)
by Th72;
not b in dom Start-At((card I+1),SCMPDS) by SCMPDS_4:18;
hence thesis by A1,FUNCT_4:11;
end;
begin :: The computation of "if var<=0 then block"
theorem
card if<=0(a,k1,I) = card I + 2 by Lm8;
theorem
0 in dom if<=0(a,k1,I) & 1 in dom if<=0(a,k1,I) by Lm9;
theorem
if<=0(a,k1,I). 0 = (a,k1)<=0_goto 2 & if<=0(a,k1,I). 1 =
goto (card I + 1) by Lm10;
theorem Th79:
for s being State of SCMPDS, I being shiftable Program of
SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1) <= 0 & I
is_closed_on s,P & I is_halting_on s,P holds if<=0(a,k1,I) is_closed_on s,P
& if<=0(a
,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS, I be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if<=0(a,k1,I), pIF=stop IF, pI=stop I,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)<=0_goto 2, j = goto (card I + 1);
A1: stop I c= P2 by FUNCT_4:25;
A2: IF = i ';' (j ';' I) by SCMPDS_4:16;
A3: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A2,Th3;
for a holds s2.a = s4.a by A3,SCMPDS_2:56;
then
A4: DataPart s2 = DataPart s4 by SCMPDS_4:8;
A5: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A6: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A5,FUNCT_4:11;
A7: IC s3 = 0 by MEMSTR_0:47;
assume
s.b <= 0;
then
A8: IC s4 = ICplusConst(s3,2) by A3,A6,SCMPDS_2:56
.= (0+2) by A7,Th4;
assume
A9: I is_closed_on s,P;
then
A10: I is_closed_on s2,P2;
assume
I is_halting_on s,P;
then
A11: P2 halts_on s2;
A12: Start-At(0,SCMPDS) c= s2 & Shift(pI,2) c= P4 by Lm7,FUNCT_4:25;
A13: 0 in dom pIF by COMPOS_1:36;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A14: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s2,k1) as Nat;
A15: card pIF = 1+ card IF by COMPOS_1:55
.= 1+(card I +2) by Lm8
.= 1+card I +2
.=card pI+2 by COMPOS_1:55;
m in dom pI by A9;
then m < card pI by AFINSQ_1:66;
then
A16: m+2 < card pIF by A15,XREAL_1:6;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A14,EXTPRO_1:4
.= (m + 2) by A10,A12,A8,A4,Th22,A1;
hence IC Comput(P3,s3,k) in dom pIF by A16,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s3,k) in dom pIF by A13,A7,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P;
A17: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A17
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A10,A12,A8,A4,Th22,A1
.= halt SCMPDS by A11,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th80:
for s being State of SCMPDS,I being Program of SCMPDS, a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) > 0 holds if<=0(a,k1,I)
is_closed_on s,P & if<=0(a,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, a be Int_position,k1 be
Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b > 0;
set i = (a,k1)<=0_goto 2, j = goto (card I + 1);
set IF=if<=0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), s5 = Comput(P3,s3,2), P4 = P3, P5 = P3;
A2: IF =i ';' (j ';' I) by SCMPDS_4:16;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: IC s3 = 0 by MEMSTR_0:47;
Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A2,Th3;
then
A6: IC s4 = IC s3 + 1 by A1,A4,SCMPDS_2:56
.= (0+1) by A5;
A7: pIF c= P3 by FUNCT_4:25;
then
A8: pIF c= P4;
A9: 1 in dom IF by Lm9;
then 1 in dom pIF by COMPOS_1:62;
then
A10: P4. 1 = pIF. 1 by A8,GRFUNC_1:2
.=IF. 1 by A9,COMPOS_1:63
.=j by Lm10;
A11: card IF=card I+2 by Lm8;
then
A12: (card I+2) in dom pIF by COMPOS_1:64;
A13: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
Comput(P3, s3,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(j,s4) by A6,A10,A13;
then
A14: IC s5 = ICplusConst(s4,card I+1) by SCMPDS_2:54
.= (card I+1+1) by A6,Th4
.= (card I+(1+1));
A15: (P3)/.IC s5
= P3.IC s5 by PBOOLE:143;
pIF c= P5 by A7;
then P5.(card I+2) = pIF.(card I+2) by A12,GRFUNC_1:2
.=halt SCMPDS by A11,COMPOS_1:64;
then
A16: CurInstr(P3,s5) = halt SCMPDS by A14,A15;
now
let k be Nat;
A17: k = 0 or 0 + 1 <= k by INT_1:7;
per cases by A17,XXREAL_0:1;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A5,COMPOS_1:36;
end;
suppose
k = 1;
hence IC Comput(P3,s3,k) in dom pIF by A9,A6,COMPOS_1:62;
end;
suppose
1 < k;
then 1+1 <= k by INT_1:7;
hence IC Comput(P3,s3,k) in dom pIF
by A12,A14,A16,EXTPRO_1:5;
end;
end;
hence IF is_closed_on s,P;
P3 halts_on s3 by A16,EXTPRO_1:29;
hence thesis;
end;
theorem Th81:
for s being State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)
<= 0 & I is_closed_on s,P & I is_halting_on s,P
holds IExec(if<=0(a,k1,I),P,Initialize s) =
IExec(I,P,Initialize s) +* Start-At((card I+2),SCMPDS)
proof
let s be State of SCMPDS,I be halt-free shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if<=0(a,k1,I), pIF = stop IF, pI = stop I,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
set i = (a,k1)<=0_goto 2, j = goto (card I + 1);
set SAl=Start-At((card I+2),SCMPDS);
A1: stop I c= P2 by FUNCT_4:25;
A2: IF=i ';' (j ';' I) by SCMPDS_4:16;
A3: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A2,Th3;
A4: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A5: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A4,FUNCT_4:11;
A6: IC s3 = 0 by MEMSTR_0:47;
A7: Start-At(0,SCMPDS) c= s2 & Shift(pI,2) c= P4 by Lm7,FUNCT_4:25;
for a holds s2.a = s4.a by A3,SCMPDS_2:56;
then
A8: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
s.b <= 0;
then
A9: IC s4 = ICplusConst(s3,2) by A3,A5,SCMPDS_2:56
.= (0+2) by A6,Th4;
assume
A10: I is_closed_on s,P;
then
A11: I is_closed_on s2,P2;
assume
A12: I is_halting_on s,P;
then
A13: P2 halts_on s2;
A14: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
A15: CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A14
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A11,A7,A9,A8,Th22,A1
.= halt SCMPDS by A13,EXTPRO_1:def 15;
then
A16: P3 halts_on s3 by EXTPRO_1:29;
A17: CurInstr(P3,s3) = i by A2,Th3;
now
let l be Nat;
assume
A18: l < LifeSpan(P2,s2) + 1;
A19: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A19;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A17;
end;
suppose
l <> 0;
then consider n be Nat such that
A20: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A21: n < LifeSpan(P2,s2) by A18,A20,XREAL_1:6;
assume
A22: CurInstr(P3,Comput(P3,s3,l)) = halt SCMPDS;
A23: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s2,n)) =
CurInstr(P3,Comput(P3,s4,n))
by A11,A7,A9,A8,Th22,A1
.= halt SCMPDS by A20,A22,A23;
hence contradiction by A13,A21,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P2,s2) + 1 <= l;
then
A24: LifeSpan(P3,s3) = LifeSpan(P2,s2) + 1 by A15,A16,EXTPRO_1:def 15;
A25: DataPart Result(P2,s2) = DataPart Comput(P2,s2,
LifeSpan(P2,s2)) by A13,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s2)) by A11,A7,A9,A8,Th22,A1
.= DataPart Comput(P3, s3,LifeSpan(P2,s2) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A16,A24,EXTPRO_1:23;
A26: now
let x be object;
A27: dom Start-At((card I+2),SCMPDS) = {IC SCMPDS} by FUNCOP_1:13;
assume
A28: x in dom IExec(IF,P,Initialize 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 SAl by A27,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= (Result(P2,s2)).x by A25,A29,SCMPDS_4:8
.= IExec(I,P,Initialize s).x
.= (IExec(I,P,Initialize s) +* SAl).x by A30,FUNCT_4:11;
end;
suppose
A31: x = IC SCMPDS;
A32: IC Result(P2,s2) = IC IExec(I,P,Initialize s)
.= card I by A10,A12,Th25;
A33: x in dom SAl by A27,A31,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P2,s2) + 1).x by A16,A24,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s2)) by A31,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 2
by A11,A7,A9,A8,Th22,A1
.= IC Result(P2,s2) + 2 by A13,EXTPRO_1:23
.= IC SAl by A32,FUNCOP_1:72
.= (IExec(I,P,Initialize s) +* SAl).x by A31,A33,FUNCT_4:13;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I,P,Initialize s)
+* Start-At((card I+2),SCMPDS)) by PARTFUN1:def 2;
hence thesis by A26,FUNCT_1:2;
end;
theorem Th82:
for s being State of SCMPDS,I being Program of SCMPDS,a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) > 0
holds IExec(if<=0(a,k1,I),P,Initialize s)
= s +* Start-At((card I+2),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS,a be Int_position, k1 be
Integer;
set b=DataLoc(s.a,k1);
set IF=if<=0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), s5 = Comput(P3,s3,2), P4 = P3, P5 = P3;
set i = (a,k1)<=0_goto 2, j = goto (card I + 1);
set SAl=Start-At((card I+2),SCMPDS);
A1: IF =i ';' (j ';' I) by SCMPDS_4:16;
A2: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A3: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A2,FUNCT_4:11;
A4: IC s3 = 0 by MEMSTR_0:47;
A5: pIF c= P3 by FUNCT_4:25;
then
A6: pIF c= P4;
A7: pIF c= P5 by A5;
A8: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
assume
s.b > 0;
then
A9: IC s4 = IC s3 + 1 by A8,A3,SCMPDS_2:56
.= (0+1) by A4;
A10: 1 in dom IF by Lm9;
then 1 in dom pIF by COMPOS_1:62;
then
A11: P4.1 = pIF. 1 by A6,GRFUNC_1:2
.=IF. 1 by A10,COMPOS_1:63
.=j by Lm10;
A12: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
A13: Comput(P3, s3,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(j,s4) by A9,A11,A12;
then
A14: IC s5 = ICplusConst(s4,card I+1) by SCMPDS_2:54
.= (card I+1+1) by A9,Th4
.= (card I+(1+1));
A15: (P3)/.IC s5
= P3.IC s5 by PBOOLE:143;
A16: card IF=card I+2 by Lm8;
then (card I+2) in dom pIF by COMPOS_1:64;
then P5.(card I+2) = pIF.(card I+2) by A7,GRFUNC_1:2
.=halt SCMPDS by A16,COMPOS_1:64;
then
A17: CurInstr(P3,s5) = halt SCMPDS by A14,A15;
then
A18: P3 halts_on s3 by EXTPRO_1:29;
A19: CurInstr(P3,s3) = i by A1,Th3;
now
let l be Nat;
assume
l < 1+1;
then
A20: l <= 1 by NAT_1:13;
A21: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
A22: P3/.IC Comput(P3,s3,l)
= P3.IC Comput(P3,s3,l) by PBOOLE:143;
per cases by A20,NAT_1:25;
suppose
l=0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A21;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A19;
end;
suppose
l=1;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A9,A11,A22;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds 2 <= l;
then LifeSpan(P3,s3) = 2 by A17,A18,EXTPRO_1:def 15;
then
A23: s5 = Result(P3,s3) by A18,EXTPRO_1:23;
A24: now
A25: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
let x be object;
assume
A26: x in dom IExec(IF,P,Initialize s);
per cases by A26,SCMPDS_4:6;
suppose
A27: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A28: not x in dom SAl by A25,TARSKI:def 1;
A29: not x in dom Start-At(0,SCMPDS) by A27,SCMPDS_4:18;
thus IExec(IF,P,Initialize s).x = s5.x by A23
.= s4.x by A13,A27,SCMPDS_2:54
.= s3.x by A8,A27,SCMPDS_2:56
.= s.x by A29,FUNCT_4:11
.= (s +* SAl).x by A28,FUNCT_4:11;
end;
suppose
A30: x = IC SCMPDS;
hence IExec(IF,P,Initialize s).x = (card I + 2) by A14,A23
.= (s +* Start-At((card I+2),SCMPDS)).x by A30,FUNCT_4:113;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (s +* SAl) by PARTFUN1:def 2;
hence thesis by A24,FUNCT_1:2;
end;
registration
let I be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if<=0(a,k1,I) -> shiftable parahalting;
correctness
proof
set i = (a,k1)<=0_goto 2, j = goto (card I + 1);
set IF=if<=0(a,k1,I), pIF = stop IF;
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume pIF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) <= 0;
then IF is_halting_on s,P by A3,Th79;
hence P halts_on s by A2,A1;
end;
suppose
s.DataLoc(s.a,k1) > 0;
then IF is_halting_on s,P by Th80;
hence P halts_on s by A2,A1;
end;
end;
end;
registration
let I be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if<=0(a,k1,I) -> halt-free;
coherence;
end;
theorem
for s being 0-started State of SCMPDS,
I being halt-free shiftable parahalting
Program of SCMPDS,a being Int_position,k1 being Integer
holds IC IExec(if<=0(a,k1,I),P,s) = card I + 2
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable parahalting Program of
SCMPDS,a be Int_position,k1 be Integer;
set IF=if<=0(a,k1,I);
A1: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
A2: Initialize s = s by MEMSTR_0:44;
per cases;
suppose
s.DataLoc(s.a,k1) <= 0;
then IExec(IF,P,s) =IExec(I,P,s) +* Start-At((card I+2),SCMPDS)
by A1,Th81,A2;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) > 0;
then IExec(IF,P,s) =s +* Start-At((card I+2),SCMPDS) by Th82,A2;
hence thesis by FUNCT_4:113;
end;
end;
theorem
for s being State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,a,b being Int_position,k1 being Integer st s.DataLoc(s.a,k1)
<= 0 holds IExec(if<=0(a,k1,I),P,Initialize s).b = IExec(I,P,Initialize s).b
proof
let s be State of SCMPDS,I be halt-free shiftable parahalting Program of
SCMPDS,a,b be Int_position,k1 be Integer;
assume
A1: s.DataLoc(s.a,k1) <= 0;
A2: not b in dom Start-At((card I+2),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then IExec(if<=0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+2),SCMPDS)
by A1,Th81;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,a,b being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) > 0
holds IExec(if<=0(a,k1,I),P,Initialize s).b = s.b
proof
let s be State of SCMPDS,I be Program of SCMPDS,a,b be Int_position, k1 be
Integer;
assume
s.DataLoc(s.a,k1) > 0;
then
A1: IExec(if<=0(a,k1,I),P,Initialize s) = s +* Start-At((card I+2),SCMPDS)
by Th82;
not b in dom Start-At((card I+2),SCMPDS) by SCMPDS_4:18;
hence thesis by A1,FUNCT_4:11;
end;
begin :: The computation of "if var<0 then block1 else block2"
theorem
card if<0(a,k1,I,J) = card I + card J + 2 by Lm4;
theorem
0 in dom if<0(a,k1,I,J) & 1 in dom if<0(a,k1,I,J)
proof
set ci=card if<0(a,k1,I,J);
ci=card I + card J +2 by Lm4;
then 2 <= ci by NAT_1:12;
then 1 < ci by XXREAL_0:2;
hence thesis by AFINSQ_1:66;
end;
theorem
if<0(a,k1,I,J). 0 = (a,k1)>=0_goto (card I + 2) by Lm5;
theorem Th89:
for s being 0-started State of SCMPDS, I,J being shiftable Program of
SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)<0 & I
is_closed_on s,P & I is_halting_on s,P holds if<0(a,k1,I,J) is_closed_on s,P
& if<0(a
,k1,I,J) is_halting_on s,P
proof
let s be 0-started State of SCMPDS, I,J be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set G=Goto (card J+1);
set I2 = I ';' G ';' J, IF=if<0(a,k1,I,J), pIF=stop IF,
pI2=stop I2, P2 = P +* pI2, P3 = P +* pIF,
s4 = Comput(P3,s,1), P4 = P3;
set i = (a,k1)>=0_goto (card I + 2);
A1: 0 in dom pIF by COMPOS_1:36;
A2: Initialize s = s by MEMSTR_0:44;
then
A3: IC s = 0 by MEMSTR_0:47;
A4: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' I2 by SCMPDS_4:14;
then
A5: Shift(pI2,1) c= P4 by Lm6;
A6: Comput(P3, s,0 + 1) = Following(P3,Comput(P3,s,0)) by EXTPRO_1:3
.= Following(P3,s) by EXTPRO_1:2
.= Exec(i,s) by A4,Th3,A2;
for a holds s.a = s4.a by A6,SCMPDS_2:57;
then
A7: DataPart s = DataPart s4 by SCMPDS_4:8;
assume
s.b < 0;
then
A8: IC s4 = IC s + 1 by A6,SCMPDS_2:57
.= (0+1) by A3;
assume
A9: I is_closed_on s,P;
assume
A10: I is_halting_on s,P;
then
A11: I2 is_closed_on s,P by A9,Th21;
then
A12: Start-At(0,SCMPDS) c= s & I2 is_closed_on s,P2 by A2,FUNCT_4:25;
A13: stop I2 c= P2 by FUNCT_4:25;
I2 is_halting_on s,P by A9,A10,Th21;
then
A14: P2 halts_on s by A2;
A15: card pIF = card IF +1 by COMPOS_1:55
.= card I2 +1+1 by A4,Th1;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A16: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s,k1) as Nat;
A17: card pIF = card pI2+1 by A15,COMPOS_1:55;
m in dom pI2 by A11,A2;
then m < card pI2 by AFINSQ_1:66;
then
A18: m+1 < card pIF by A17,XREAL_1:6;
IC Comput(P3,s,k) = IC Comput(P3, s4,k1) by A16,EXTPRO_1:4
.= (m + 1) by A12,A5,A8,A7,Th22,A13;
hence IC Comput(P3,s,k) in dom pIF by A18,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s,k) in dom pIF by A1,A3,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P by A2;
A19: Comput(P3,s,LifeSpan(P2,s)+1)
= Comput(P3,Comput(P3,s,1),LifeSpan(P2,s))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s,LifeSpan(P2,s)+1))
=CurInstr(P3,Comput(P3,s4,LifeSpan(P2,s))) by A19
.=CurInstr(P2,Comput(P2,s,LifeSpan(P2,s))) by A12,A5,A8,A7,Th22,A13
.= halt SCMPDS by A14,EXTPRO_1:def 15;
then P3 halts_on s by EXTPRO_1:29;
hence thesis by A2;
end;
theorem Th90:
for s being State of SCMPDS,I being Program of SCMPDS,J being
shiftable Program of SCMPDS,a being Int_position,k1 being Integer st s.DataLoc(
s.a,k1) >= 0 & J is_closed_on s,P & J is_halting_on s,P holds if<0(a,k1,I,J)
is_closed_on s,P & if<0(a,k1,I,J) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, J be shiftable Program of
SCMPDS, a be Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set pJ=stop J, s1 = Initialize s, P1 = P +* pJ,
IF=if<0(a,k1,I,J), pIF=
stop IF, s3 = Initialize s, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)>=0_goto (card I + 2);
set G =Goto (card J+1), iG=i ';' I ';' G;
A1: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' (I ';' G ';' J) by SCMPDS_4:14;
A2: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: IC s3 = 0 by MEMSTR_0:47;
assume
s.b >= 0;
then
A6: IC s4 = ICplusConst(s3,card I + 2) by A2,A4,SCMPDS_2:57
.= (0+(card I + 2)) by A5,Th4;
assume
A7: J is_closed_on s,P;
then
A8: Start-At(0,SCMPDS) c= s1 & J is_closed_on s1,P1 by FUNCT_4:25;
A9: stop J c= P1 by FUNCT_4:25;
A10: pIF c= P3 by FUNCT_4:25;
A11: card iG = card (i ';' I) + card G by AFINSQ_1:17
.=card (i ';' I) + 1 by COMPOS_1:54
.=card I +1 +1 by Th1
.=card I +(1 +1);
then Shift(pJ,card I+2) c= pIF by Th5;
then Shift(pJ,card I+2) c= P3 by A10,XBOOLE_1:1;
then
A12: Shift(pJ,card I+2) c= P4;
assume
J is_halting_on s,P;
then
A13: P1 halts_on s1;
for a holds s1.a = s4.a by A2,SCMPDS_2:57;
then
A14: DataPart s1 = DataPart s4 by SCMPDS_4:8;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A15: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P1, s1,k1) as Nat;
m in dom pJ by A7;
then m < card pJ by AFINSQ_1:66;
then
A16: m + (card I + 2) < card pJ + (card I + 2) by XREAL_1:6;
A17: card pJ = card J + 1 by COMPOS_1:55;
A18: card pIF = card IF+1 by COMPOS_1:55
.=card I +2 +card J +1 by A11,AFINSQ_1:17
.=card I +2 + card pJ by A17;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A15,EXTPRO_1:4
.= (m + (card I + 2)) by A8,A14,A12,A6,Th22,A9;
hence IC Comput(P3,s3,k) in dom pIF by A18,A16,AFINSQ_1:66;
end;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A5,COMPOS_1:36;
end;
end;
hence IF is_closed_on s,P;
A19: Comput(P3,s3,LifeSpan(P1,s1)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P1,s1)) by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P1,s1)+1))
=CurInstr(P3,Comput(P3,s4,LifeSpan(P1,s1))) by A19
.=CurInstr(P1,Comput(P1,s1,LifeSpan(P1,s1))) by A8,A14,A12,A6,Th22,A9
.= halt SCMPDS by A13,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th91:
for s being 0-started State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, J being shiftable Program of SCMPDS,a being Int_position,k1
being Integer st s.DataLoc(s.a,k1) < 0 & I is_closed_on s,P
& I is_halting_on s,P
holds IExec(if<0(a,k1,I,J),P,s) = IExec(I,P,s)
+* Start-At((card I + card J+ 2),SCMPDS)
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable Program of SCMPDS, J be
shiftable Program of SCMPDS,a be Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set G=Goto (card J+1);
set I2 = I ';' G ';' J, IF=if<0(a,k1,I,J), pIF = stop IF,
pI2=stop I2, P2 = P +* pI2, P3 = P +* pIF,
s4 = Comput(P3,s,1), P4 = P3;
set i = (a,k1)>=0_goto (card I + 2);
set SAl= Start-At((card I+card J+2),SCMPDS);
A1: Initialize s = s by MEMSTR_0:44;
then
A2: IC s = 0 by MEMSTR_0:47;
A3: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' I2 by SCMPDS_4:14;
then
A4: Shift(pI2,1) c= P4 by Lm6;
A5: Comput(P3, s,0 + 1) = Following(P3,Comput(P3,s,0)) by EXTPRO_1:3
.= Following(P3,s) by EXTPRO_1:2
.= Exec(i,s) by A3,Th3,A1;
assume
s.b < 0;
then
A6: IC s4 = IC s + 1 by A5,SCMPDS_2:57
.= (0+1) by A2;
for a holds s.a = s4.a by A5,SCMPDS_2:57;
then
A7: DataPart s = DataPart s4 by SCMPDS_4:8;
assume
A8: I is_closed_on s,P;
assume
A9: I is_halting_on s,P;
then I2 is_halting_on s,P by A8,Th21;
then
A10: P2 halts_on s by A1;
I2 is_closed_on s,P by A8,A9,Th21;
then
A11: Start-At(0,SCMPDS) c= s & I2 is_closed_on s,P2 by A1,FUNCT_4:25;
A12: stop I2 c= P2 by FUNCT_4:25;
A13: Comput(P3,s,LifeSpan(P2,s)+1)
= Comput(P3,Comput(P3,s,1),LifeSpan(P2
,s))
by EXTPRO_1:4;
A14: CurInstr(P3,Comput(P3,s,LifeSpan(P2,s)+1))
=CurInstr(P3,Comput(P3,s4,LifeSpan(P2,s))) by A13
.=CurInstr(P2,Comput(P2,s,LifeSpan(P2,s))) by A11,A4,A6,A7,Th22,A12
.= halt SCMPDS by A10,EXTPRO_1:def 15;
then
A15: P3 halts_on s by EXTPRO_1:29;
A16: CurInstr(P3,s) = i by A3,Th3,A1;
now
let l be Nat;
assume
A17: l < LifeSpan(P2,s) + 1;
A18: Comput(P3,s,0) = s by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s,l))
= CurInstr(P3,s)
by A18;
hence CurInstr(P3,Comput(P3,s,l))
<> halt SCMPDS by A16;
end;
suppose
l <> 0;
then consider n be Nat such that
A19: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A20: n < LifeSpan(P2,s) by A17,A19,XREAL_1:6;
assume
A21: CurInstr(P3,Comput(P3,s,l)) = halt SCMPDS;
A22: Comput(P3,s,n+1)
= Comput(P3,Comput(P3,s,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s,n)) =
CurInstr(P3,Comput(P3,s4,n)) by A11,A4,A6,A7,Th22,A12
.= halt SCMPDS by A19,A21,A22;
hence contradiction by A10,A20,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s,l)) = halt SCMPDS
holds LifeSpan(P2,s) + 1 <= l;
then
A23: LifeSpan(P3,s) = LifeSpan(P2,s) + 1 by A14,A15,EXTPRO_1:def 15;
A24: DataPart Result(P2,s) = DataPart Comput(P2,s,
LifeSpan(P2,s)) by A10,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s))
by A11,A4,A6,A7,Th22,A12
.= DataPart Comput(P3, s,LifeSpan(P2,s) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s) by A15,A23,EXTPRO_1:23;
A25: now
let x be object;
A26: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A27: x in dom IExec(IF,P,s);
per cases by A27,SCMPDS_4:6;
suppose
A28: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A29: not x in dom SAl by A26,TARSKI:def 1;
thus IExec(IF,P,s).x = (Result(P3,s)).x
.= (Result(P2,s)).x by A24,A28,SCMPDS_4:8
.= IExec(I2,P,s).x
.= (IExec(I2,P,s) +* SAl).x by A29,FUNCT_4:11;
end;
suppose
A30: x = IC SCMPDS;
A31: IC Result(P2,s) = IC IExec(I2,P,s)
.= (card I + card J + 1) by A8,A9,Th23;
A32: x in dom SAl by A26,A30,TARSKI:def 1;
thus IExec(IF,P,s).x = (Result(P3,s)).x
.= Comput(P3, s,LifeSpan(P2,s) + 1).x by A15,A23,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s)) by A30,EXTPRO_1:4
.= IC Comput(P2, s,LifeSpan(P2,s)) + 1 by A11,A4,A6,A7,Th22,A12
.= IC Result(P2,s) + 1 by A10,EXTPRO_1:23
.= IC Start-At ((card I + card J + 1) + 1,SCMPDS)
by A31,FUNCOP_1:72
.= (IExec(I2,P,s) +* SAl).x by A30,A32,FUNCT_4:13;
end;
end;
dom IExec(IF,P,s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I2,P,s) +* SAl) by PARTFUN1:def 2;
hence IExec(IF,P,s) = IExec(I2,P,s) +* SAl
by A25,FUNCT_1:2
.= IExec(I,P,s) +* Start-At((card I + card J + 1),SCMPDS) +*
Start-At(
(card I + card J + 2),SCMPDS) by A8,A9,Th24
.= IExec(I,P,s) +* SAl by MEMSTR_0:36;
end;
theorem Th92:
for s being State of SCMPDS,I being Program of SCMPDS,J being
halt-free shiftable Program of SCMPDS,a being Int_position,k1 being Integer
st s.DataLoc(s.a,k1) >= 0 & J is_closed_on s,P & J is_halting_on s,P
holds IExec(if<0(a,k1,I,J),P,Initialize s)
= IExec(J,P,Initialize s) +* Start-At((card I+card J+2),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS,J be halt-free shiftable
Program of SCMPDS,a be Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set pJ=stop J, s1 = Initialize s, P1 = P +* pJ,
IF=if<0(a,k1,I,J), pIF=
stop IF, s3 = Initialize s, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)>=0_goto (card I + 2);
set G =Goto (card J+1), iG=i ';' I ';' G;
set SAl=Start-At((card I+card J+2),SCMPDS);
A1: IF = i ';' (I ';' G) ';' J by SCMPDS_4:14
.= i ';' (I ';' G ';' J) by SCMPDS_4:14;
A2: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: IC s3 = 0 by MEMSTR_0:47;
assume
s.b >= 0;
then
A6: IC s4 = ICplusConst(s3,card I + 2) by A2,A4,SCMPDS_2:57
.= (0+(card I + 2)) by A5,Th4;
for a holds s1.a = s4.a by A2,SCMPDS_2:57;
then
A7: DataPart s1 = DataPart s4 by SCMPDS_4:8;
card iG = card (i ';' I) + card G by AFINSQ_1:17
.=card (i ';' I) + 1 by COMPOS_1:54
.=card I +1 +1 by Th1
.=card I +(1 +1);
then
A8: Shift(pJ,card I+2) c= pIF by Th5;
pIF c= P3 by FUNCT_4:25;
then Shift(pJ,card I+2) c= P3 by A8,XBOOLE_1:1;
then
A9: Shift(pJ,card I+2) c= P4;
assume
A10: J is_closed_on s,P;
then
A11: Start-At(0,SCMPDS) c= s1 & J is_closed_on s1,P1 by FUNCT_4:25;
A12: stop J c= P1 by FUNCT_4:25;
assume
A13: J is_halting_on s,P;
then
A14: P1 halts_on s1;
A15: Comput(P3,s3,LifeSpan(P1,s1)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P1
,s1))
by EXTPRO_1:4;
A16: CurInstr(P3,Comput(P3,s3,LifeSpan(P1,s1)+1))
=CurInstr(P3,Comput(P3,s4,LifeSpan(P1,s1))) by A15
.=CurInstr(P1,Comput(P1,s1,LifeSpan(P1,s1))) by A11,A9,A6,A7,Th22,A12
.= halt SCMPDS by A14,EXTPRO_1:def 15;
then
A17: P3 halts_on s3 by EXTPRO_1:29;
A18: CurInstr(P3,s3) = i by A1,Th3;
now
let l be Nat;
assume
A19: l < LifeSpan(P1,s1) + 1;
A20: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A20;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A18;
end;
suppose
l <> 0;
then consider n be Nat such that
A21: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A22: n < LifeSpan(P1,s1) by A19,A21,XREAL_1:6;
assume
A23: CurInstr(P3,Comput(P3,s3,l)) = halt SCMPDS;
A24: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P1,Comput(P1,s1,n))
= CurInstr(P3,
Comput(P3,s4,n)) by A11,A9,A6,A7,Th22,A12
.= halt SCMPDS by A21,A23,A24;
hence contradiction by A14,A22,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P1,s1) + 1 <= l;
then
A25: LifeSpan(P3,s3) = LifeSpan(P1,s1) + 1 by A16,A17,EXTPRO_1:def 15;
A26: DataPart Result(P1,s1) = DataPart Comput(P1, s1
,LifeSpan(P1,s1)) by A14,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P1,s1))
by A11,A9,A6,A7,Th22,A12
.= DataPart Comput(P3, s3,LifeSpan(P1,s1) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A17,A25,EXTPRO_1:23;
A27: now
let x be object;
A28: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A29: x in dom IExec(IF,P,Initialize s);
per cases by A29,SCMPDS_4:6;
suppose
A30: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A31: not x in dom SAl by A28,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= (Result(P1,s1)).x by A26,A30,SCMPDS_4:8
.= IExec(J,P,Initialize s).x
.= (IExec(J,P,Initialize s) +* SAl).x by A31,FUNCT_4:11;
end;
suppose
A32: x = IC SCMPDS;
A33: IC Result(P1,s1) = IC IExec(J,P,Initialize s)
.= (card J) by A10,A13,Th25;
A34: x in dom SAl by A28,A32,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P1,s1) + 1).x by A17,A25,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P1,s1)) by A32,EXTPRO_1:4
.= IC Comput(P1, s1,LifeSpan(P1,s1)) + (card
I + 2) by A11,A9,A6,A7,Th22,A12
.= IC Result(P1,s1) + (card I + 2) by A14,EXTPRO_1:23
.= IC Start-At (card J + (card I + 2),SCMPDS) by A33,FUNCOP_1:72
.= (IExec(J,P,Initialize s) +* SAl).x by A32,A34,FUNCT_4:13;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(J,P,Initialize s) +* SAl) by PARTFUN1:def 2;
hence thesis by A27,FUNCT_1:2;
end;
registration
let I,J be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if<0(a,k1,I,J) -> shiftable parahalting;
correctness
proof
set i = (a,k1)>=0_goto (card I + 2), G =Goto (card J+1);
set IF=if<0(a,k1,I,J), pIF = stop IF;
reconsider IJ=I ';' G ';' J as shiftable Program of SCMPDS;
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume pIF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
A4: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) < 0;
then IF is_halting_on s,P by A4,Th89;
hence P halts_on s by A2,A1;
end;
suppose
s.DataLoc(s.a,k1) >= 0;
then IF is_halting_on s,P by A3,Th90;
hence P halts_on s by A2,A1;
end;
end;
end;
registration
let I,J be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if<0(a,k1,I,J) -> halt-free;
coherence;
end;
theorem
for s being 0-started State of SCMPDS,I,J being halt-free shiftable
parahalting Program of SCMPDS,a being Int_position,k1 being Integer holds IC
IExec(if<0(a,k1,I,J),P,s) = card I + card J + 2
proof
let s be 0-started State of SCMPDS,
I,J be halt-free shiftable parahalting Program of
SCMPDS,a be Int_position,k1 be Integer;
set IF=if<0(a,k1,I,J);
A1: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
A2: J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
A3: Initialize s = s by MEMSTR_0:44;
per cases;
suppose
s.DataLoc(s.a,k1) < 0;
then IExec(IF,P,s) = IExec(I,P,s) +* Start-At((card I+card J+2),SCMPDS)
by A1,Th91;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) >= 0;
then IExec(IF,P,s) = IExec(J,P,s) +* Start-At((card I+card J+2),SCMPDS)
by A2,Th92,A3;
hence thesis by FUNCT_4:113;
end;
end;
theorem
for s being 0-started State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,J being shiftable Program of SCMPDS,a,b being Int_position,
k1 being Integer st s.DataLoc(s.a,k1)<0
holds IExec(if<0(a,k1,I,J),P,s).b
= IExec(I,P,s).b
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable parahalting Program of
SCMPDS,J be shiftable Program of SCMPDS,a,b be Int_position, k1 be Integer;
assume
A1: s.DataLoc(s.a,k1)<0;
A2: not b in dom Start-At((card I+card J+2),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then
IExec(if<0(a,k1,I,J),P,s) = IExec(I,P,s)
+* Start-At((card I + card J + 2),SCMPDS) by A1,Th91;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,J being
halt-free parahalting shiftable Program of SCMPDS,a,b being Int_position,k1
being Integer st s.DataLoc(s.a,k1) >= 0
holds IExec(if<0(a,k1,I,J),P,Initialize s).b = IExec(J,P,Initialize s).b
proof
let s be State of SCMPDS,I be Program of SCMPDS,J be halt-free parahalting
shiftable Program of SCMPDS,a,b be Int_position, k1 be Integer;
set IF=if<0(a,k1,I,J);
assume
A1: s.DataLoc(s.a,k1) >= 0;
A2: not b in dom Start-At((card I+card J+2),SCMPDS) by SCMPDS_4:18;
J is_closed_on s,P & J is_halting_on s,P by Th11,Th12;
then IExec(IF,P,Initialize s) =IExec(J,P,Initialize s)
+* Start-At((card I+card J+2),SCMPDS)
by A1,Th92;
hence thesis by A2,FUNCT_4:11;
end;
begin :: The computation of "if var<0 then block"
theorem
card if<0(a,k1,I) = card I + 1 by Th1;
theorem
0 in dom if<0(a,k1,I)
proof
set ci=card if<0(a,k1,I);
ci=card I + 1 by Th1;
hence thesis by AFINSQ_1:66;
end;
theorem
if<0(a,k1,I). 0 = (a,k1)>=0_goto (card I + 1) by Th2;
theorem Th99:
for s being State of SCMPDS, I being shiftable Program of
SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1) < 0 & I
is_closed_on s,P & I is_halting_on s,P holds if<0(a,k1,I) is_closed_on s,P
& if<0(a,
k1,I) is_halting_on s,P
proof
let s be State of SCMPDS, I be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if<0(a,k1,I), pIF=stop IF, pI=stop I,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)>=0_goto (card I + 1);
A1: stop I c= P2 by FUNCT_4:25;
A2: 0 in dom pIF by COMPOS_1:36;
A3: IC s3 = 0 by MEMSTR_0:47;
A4: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A5: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A4,FUNCT_4:11;
A6: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
for a holds s2.a = s4.a by A6,SCMPDS_2:57;
then
A7: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
s.b < 0;
then
A8: IC s4 = IC s3 + 1 by A6,A5,SCMPDS_2:57
.= (0+1) by A3;
assume
A9: I is_closed_on s,P;
then
A10: I is_closed_on s2,P2;
assume
I is_halting_on s,P;
then
A11: P2 halts_on s2;
A12: Start-At(0,SCMPDS) c= s2 & Shift(pI,1) c= P4 by Lm6,FUNCT_4:25;
A13: card pIF = card IF +1 by COMPOS_1:55
.= card I +1+1 by Th1;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A14: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s2,k1) as Nat;
A15: card pIF = card pI+1 by A13,COMPOS_1:55;
m in dom pI by A9;
then m < card pI by AFINSQ_1:66;
then
A16: m+1 < card pIF by A15,XREAL_1:6;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A14,EXTPRO_1:4
.= (m + 1) by A10,A12,A8,A7,Th22,A1;
hence IC Comput(P3,s3,k) in dom pIF by A16,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s3,k) in dom pIF by A2,A3,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P;
A17: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A17
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A10,A12,A8,A7,Th22,A1
.= halt SCMPDS by A11,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th100:
for s being State of SCMPDS,I being Program of SCMPDS, a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) >= 0 holds if<0(a,k1,I)
is_closed_on s,P & if<0(a,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, a be Int_position,k1 be
Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b >= 0;
set i = (a,k1)>=0_goto (card I + 1);
set IF=if<0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
A2: IC s3 = 0 by MEMSTR_0:47;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
then
A5: IC s4 = ICplusConst(s3,card I + 1) by A1,A4,SCMPDS_2:57
.= (0+(card I + 1)) by A2,Th4;
A6: card IF=card I+1 by Th1;
then
A7: (card I+1) in dom pIF by COMPOS_1:64;
A8: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
pIF c= P3 by FUNCT_4:25;
then pIF c= P4;
then P4.(card I+1) = pIF.(card I+1) by A7,GRFUNC_1:2
.=halt SCMPDS by A6,COMPOS_1:64;
then
A9: CurInstr(P3,s4) = halt SCMPDS by A5,A8;
now
let k be Nat;
per cases;
suppose
0 < k;
then 1+0 <= k by INT_1:7;
hence IC Comput(P3,s3,k) in dom pIF by A7,A5,A9,EXTPRO_1:5;
end;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A2,COMPOS_1:36;
end;
end;
hence IF is_closed_on s,P;
P3 halts_on s3 by A9,EXTPRO_1:29;
hence thesis;
end;
theorem Th101:
for s being State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1) <
0 & I is_closed_on s,P & I is_halting_on s,P
holds IExec(if<0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+1),SCMPDS)
proof
let s be State of SCMPDS,I be halt-free shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if<0(a,k1,I), pIF = stop IF, pI=stop I,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
set i = (a,k1)>=0_goto (card I + 1);
set SAl=Start-At((card I+1),SCMPDS);
A1: stop I c= P2 by FUNCT_4:25;
A2: IC s3 = 0 by MEMSTR_0:47;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
assume
s.b < 0;
then
A6: IC s4 = IC s3 + 1 by A5,A4,SCMPDS_2:57
.= (0+1) by A2;
for a holds s2.a = s4.a by A5,SCMPDS_2:57;
then
A7: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
A8: I is_closed_on s,P;
then
A9: I is_closed_on s2,P2;
A10: Start-At(0,SCMPDS) c= s2 & Shift(pI,1) c= P4 by Lm6,FUNCT_4:25;
assume
A11: I is_halting_on s,P;
then
A12: P2 halts_on s2;
A13: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2,
s2))
by EXTPRO_1:4;
A14: CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A13
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A9,A10,A6,A7,Th22,A1
.= halt SCMPDS by A12,EXTPRO_1:def 15;
then
A15: P3 halts_on s3 by EXTPRO_1:29;
A16: CurInstr(P3,s3) = i by Th3;
now
let l be Nat;
assume
A17: l < LifeSpan(P2,s2) + 1;
A18: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A18;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A16;
end;
suppose
l <> 0;
then consider n be Nat such that
A19: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A20: n < LifeSpan(P2,s2) by A17,A19,XREAL_1:6;
assume
A21: CurInstr(P3,Comput(P3,s3,l)) = halt SCMPDS;
A22: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s2,n)) =
CurInstr(P3,Comput(P3,s4,n)) by A9,A10,A6,A7,Th22,A1
.= halt SCMPDS by A19,A21,A22;
hence contradiction by A12,A20,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P2,s2) + 1 <= l;
then
A23: LifeSpan(P3,s3) = LifeSpan(P2,s2) + 1 by A14,A15,EXTPRO_1:def 15;
A24: DataPart Result(P2,s2) = DataPart Comput(P2,s2,
LifeSpan(P2,s2)) by A12,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s2)) by A9,A10,A6,A7,Th22,A1
.= DataPart Comput(P3, s3,LifeSpan(P2,s2) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A15,A23,EXTPRO_1:23;
A25: now
let x be object;
A26: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
assume
A27: x in dom IExec(IF,P,Initialize s);
per cases by A27,SCMPDS_4:6;
suppose
A28: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A29: not x in dom SAl by A26,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= (Result(P2,s2)).x by A24,A28,SCMPDS_4:8
.= IExec(I,P,Initialize s).x
.= (IExec(I,P,Initialize s) +* SAl).x by A29,FUNCT_4:11;
end;
suppose
A30: x = IC SCMPDS;
A31: IC Result(P2,s2) = IC IExec(I,P,Initialize s)
.= card I by A8,A11,Th25;
A32: x in dom SAl by A26,A30,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P2,s2) + 1).x by A15,A23,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s2)) by A30,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 1
by A9,A10,A6,A7,Th22,A1
.= IC Result(P2,s2) + 1 by A12,EXTPRO_1:23
.= IC SAl by A31,FUNCOP_1:72
.= (IExec(I,P,Initialize s) +* SAl).x by A30,A32,FUNCT_4:13;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I,P,Initialize s) +* SAl) by PARTFUN1:def 2;
hence thesis by A25,FUNCT_1:2;
end;
theorem Th102:
for s being State of SCMPDS,I being Program of SCMPDS,a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) >= 0
holds IExec(if<0(a,k1,I),P,Initialize s) = s +* Start-At((card I+1),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS,a be Int_position, k1 be
Integer;
set b=DataLoc(s.a,k1);
set IF=if<0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
set i = (a,k1)>=0_goto (card I + 1);
set SAl=Start-At((card I+1),SCMPDS);
A1: IC s3 = 0 by MEMSTR_0:47;
A2: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A3: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A2,FUNCT_4:11;
A4: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by Th3;
assume
s.b >= 0;
then
A5: IC s4 = ICplusConst(s3,card I + 1) by A4,A3,SCMPDS_2:57
.= (0+(card I + 1)) by A1,Th4;
pIF c= P3 by FUNCT_4:25;
then
A6: pIF c= P4;
A7: P3/.IC s4
= P3.IC s4 by PBOOLE:143;
A8: card IF=card I+1 by Th1;
then (card I+1) in dom pIF by COMPOS_1:64;
then P4.(card I+1) = pIF.(card I+1) by A6,GRFUNC_1:2
.=halt SCMPDS by A8,COMPOS_1:64;
then
A9: CurInstr(P3,s4) = halt SCMPDS by A5,A7;
then
A10: P3 halts_on s3 by EXTPRO_1:29;
A11: CurInstr(P3,s3) = i by Th3;
now
let l be Nat;
A12: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
assume
l < 1;
then l <1+0;
then l=0 by NAT_1:13;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3) by A12;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A11;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds 1 <= l;
then LifeSpan(P3,s3) = 1 by A9,A10,EXTPRO_1:def 15;
then
A13: s4 = Result(P3,s3) by A10,EXTPRO_1:23;
A14: now
A15: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
let x be object;
assume
A16: x in dom IExec(IF,P,Initialize s);
per cases by A16,SCMPDS_4:6;
suppose
A17: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A18: not x in dom SAl by A15,TARSKI:def 1;
A19: not x in dom Start-At(0,SCMPDS) by A17,SCMPDS_4:18;
thus IExec(IF,P,Initialize s).x = s4.x by A13
.= s3.x by A4,A17,SCMPDS_2:57
.= s.x by A19,FUNCT_4:11
.= (s +* SAl).x by A18,FUNCT_4:11;
end;
suppose
A20: x = IC SCMPDS;
hence IExec(IF,P,Initialize s).x = (card I + 1) by A5,A13
.= (s +* SAl).x by A20,FUNCT_4:113;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (s +* SAl) by PARTFUN1:def 2;
hence thesis by A14,FUNCT_1:2;
end;
registration
let I be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if<0(a,k1,I) -> shiftable parahalting;
correctness
proof
set i = (a,k1)>=0_goto (card I +1);
set IF=if<0(a,k1,I), pIF = stop IF;
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume pIF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) < 0;
then IF is_halting_on s,P by A3,Th99;
hence P halts_on s by A2,A1;
end;
suppose
s.DataLoc(s.a,k1) >= 0;
then IF is_halting_on s,P by Th100;
hence P halts_on s by A2,A1;
end;
end;
end;
registration
let I be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if<0(a,k1,I) -> halt-free;
coherence;
end;
theorem
for s being State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,a being Int_position,k1 being Integer
holds IC IExec(if<0(a,k1,I),P,Initialize s) = card I + 1
proof
let s be State of SCMPDS,I be halt-free shiftable parahalting Program of
SCMPDS,a be Int_position,k1 be Integer;
set IF=if<0(a,k1,I);
A1: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) < 0;
then IExec(IF,P,Initialize s) =IExec(I,P,Initialize s)
+* Start-At((card I+1),SCMPDS)
by A1,Th101;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) >= 0;
then IExec(IF,P,Initialize s) =s +* Start-At((card I+1),SCMPDS) by Th102;
hence thesis by FUNCT_4:113;
end;
end;
theorem
for s being State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,a,b being Int_position,k1 being Integer st s.DataLoc(s.a,k1)
< 0 holds IExec(if<0(a,k1,I),P,Initialize s).b = IExec(I,P,Initialize s).b
proof
let s be State of SCMPDS,I be halt-free shiftable parahalting Program of
SCMPDS,a,b be Int_position,k1 be Integer;
assume
A1: s.DataLoc(s.a,k1) < 0;
A2: not b in dom Start-At((card I+1),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then IExec(if<0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+1),SCMPDS)
by A1,Th101;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,a,b being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) >= 0
holds IExec(if<0(a,k1,I),P,Initialize s).b = s.b
proof
let s be State of SCMPDS,I be Program of SCMPDS,a,b be Int_position, k1 be
Integer;
assume
s.DataLoc(s.a,k1) >= 0;
then
A1: IExec(if<0(a,k1,I),P,Initialize s) = s +* Start-At((card I+1),SCMPDS)
by Th102;
not b in dom Start-At((card I+1),SCMPDS) by SCMPDS_4:18;
hence thesis by A1,FUNCT_4:11;
end;
begin :: The computation of "if var>=0 then block"
theorem
card if>=0(a,k1,I) = card I + 2 by Lm8;
theorem
0 in dom if>=0(a,k1,I) & 1 in dom if>=0(a,k1,I) by Lm9;
theorem
if>=0(a,k1,I). 0 = (a,k1)>=0_goto 2 & if>=0(a,k1,I). 1 =
goto (card I + 1) by Lm10;
theorem Th109:
for s being State of SCMPDS, I being shiftable Program of
SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1) >= 0 & I
is_closed_on s,P & I is_halting_on s,P holds if>=0(a,k1,I) is_closed_on s,P
& if>=0(a
,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS, I be shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if>=0(a,k1,I), pIF=stop IF, pI=stop I,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3,s3,1), P4 = P3;
set i = (a,k1)>=0_goto 2, j = goto (card I + 1);
A1: stop I c= P2 by FUNCT_4:25;
A2: IF = i ';' (j ';' I) by SCMPDS_4:16;
A3: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A2,Th3;
for a holds s2.a = s4.a by A3,SCMPDS_2:57;
then
A4: DataPart s2 = DataPart s4 by SCMPDS_4:8;
A5: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A6: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A5,FUNCT_4:11;
A7: IC s3 = 0 by MEMSTR_0:47;
assume
s.b >= 0;
then
A8: IC s4 = ICplusConst(s3,2) by A3,A6,SCMPDS_2:57
.= (0+2) by A7,Th4;
assume
A9: I is_closed_on s,P;
then
A10: I is_closed_on s2,P2;
assume
I is_halting_on s,P;
then
A11: P2 halts_on s2;
A12: Start-At(0,SCMPDS) c= s2 & Shift(pI,2) c= P4 by Lm7,FUNCT_4:25;
A13: 0 in dom pIF by COMPOS_1:36;
now
let k be Nat;
per cases;
suppose
0 < k;
then consider k1 being Nat such that
A14: k1 + 1 = k by NAT_1:6;
reconsider k1 as Nat;
reconsider m = IC Comput(P2, s2,k1) as Nat;
A15: card pIF = 1+ card IF by COMPOS_1:55
.= 1+(card I +2) by Lm8
.= 1+card I +2
.=card pI+2 by COMPOS_1:55;
m in dom pI by A9;
then m < card pI by AFINSQ_1:66;
then
A16: m+2 < card pIF by A15,XREAL_1:6;
IC Comput(P3,s3,k) = IC Comput(P3, s4,k1) by A14,EXTPRO_1:4
.= (m + 2) by A10,A12,A8,A4,Th22,A1;
hence IC Comput(P3,s3,k) in dom pIF by A16,AFINSQ_1:66;
end;
suppose
k = 0;
hence IC Comput(P3,s3,k) in dom pIF by A13,A7,EXTPRO_1:2;
end;
end;
hence IF is_closed_on s,P;
A17: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A17
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2))) by A10,A12,A8,A4,Th22,A1
.= halt SCMPDS by A11,EXTPRO_1:def 15;
then P3 halts_on s3 by EXTPRO_1:29;
hence thesis;
end;
theorem Th110:
for s being State of SCMPDS,I being Program of SCMPDS, a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) < 0 holds if>=0(a,k1,I)
is_closed_on s,P & if>=0(a,k1,I) is_halting_on s,P
proof
let s be State of SCMPDS,I be Program of SCMPDS, a be Int_position,k1 be
Integer;
set b=DataLoc(s.a,k1);
assume
A1: s.b < 0;
set i = (a,k1)>=0_goto 2, j = goto (card I + 1);
set IF=if>=0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), s5 = Comput(P3,s3,2), P4 = P3, P5 = P3;
A2: IF =i ';' (j ';' I) by SCMPDS_4:16;
A3: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A4: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A3,FUNCT_4:11;
A5: IC s3 = 0 by MEMSTR_0:47;
Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A2,Th3;
then
A6: IC s4 = IC s3 + 1 by A1,A4,SCMPDS_2:57
.= (0+1) by A5;
A7: pIF c= P3 by FUNCT_4:25;
then
A8: pIF c= P4;
A9: 1 in dom IF by Lm9;
then 1 in dom pIF by COMPOS_1:62;
then
A10: P4.1 = pIF. 1 by A8,GRFUNC_1:2
.=IF. 1 by A9,COMPOS_1:63
.=j by Lm10;
A11: card IF=card I+2 by Lm8;
then
A12: (card I+2) in dom pIF by COMPOS_1:64;
A13: P3/.IC s4 = P3.IC s4 by PBOOLE:143;
Comput(P3, s3,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(j,s4) by A6,A10,A13;
then
A14: IC s5 = ICplusConst(s4,card I+1) by SCMPDS_2:54
.= (card I+1+1) by A6,Th4
.= (card I+(1+1));
A15: (P3)/.IC s5
= P3.IC s5 by PBOOLE:143;
pIF c= P5 by A7;
then P5.(card I+2) = pIF.(card I+2) by A12,GRFUNC_1:2
.=halt SCMPDS by A11,COMPOS_1:64;
then
A16: CurInstr(P3,s5) = halt SCMPDS by A14,A15;
now
let k be Nat;
A17: k = 0 or 0 + 1 <= k by INT_1:7;
per cases by A17,XXREAL_0:1;
suppose
k = 0;
then Comput(P3,s3,k) = s3 by EXTPRO_1:2;
hence IC Comput(P3,s3,k) in dom pIF by A5,COMPOS_1:36;
end;
suppose
k = 1;
hence IC Comput(P3,s3,k) in dom pIF by A9,A6,COMPOS_1:62;
end;
suppose
1 < k;
then 1+1 <= k by INT_1:7;
hence IC Comput(P3,s3,k) in dom pIF
by A12,A14,A16,EXTPRO_1:5;
end;
end;
hence IF is_closed_on s,P;
P3 halts_on s3 by A16,EXTPRO_1:29;
hence thesis;
end;
theorem Th111:
for s being State of SCMPDS,I being halt-free shiftable
Program of SCMPDS, a being Int_position,k1 being Integer st s.DataLoc(s.a,k1)
>= 0 & I is_closed_on s,P & I is_halting_on s,P
holds IExec(if>=0(a,k1,I),P,Initialize s) =
IExec(I,P,Initialize s) +* Start-At((card I+2),SCMPDS)
proof
let s be State of SCMPDS,I be halt-free shiftable Program of SCMPDS, a be
Int_position,k1 be Integer;
set b=DataLoc(s.a,k1);
set IF=if>=0(a,k1,I), pIF = stop IF, pI=stop I,
s2 = Initialize s, s3 = Initialize s,
P2 = P +* pI, P3 = P +* pIF,
s4 = Comput(P3, s3,1), P4 = P3;
set i = (a,k1)>=0_goto 2, j = goto (card I + 1);
set SAl=Start-At((card I+2),SCMPDS);
A1: IF=i ';' (j ';' I) by SCMPDS_4:16;
A2: stop I c= P2 by FUNCT_4:25;
A3: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
A4: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A5: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A4,FUNCT_4:11;
A6: IC s3 = 0 by MEMSTR_0:47;
A7: Start-At(0,SCMPDS) c= s2 & Shift(pI,2) c= P4 by Lm7,FUNCT_4:25;
for a holds s2.a = s4.a by A3,SCMPDS_2:57;
then
A8: DataPart s2 = DataPart s4 by SCMPDS_4:8;
assume
s.b >= 0;
then
A9: IC s4 = ICplusConst(s3,2) by A3,A5,SCMPDS_2:57
.= (0+2) by A6,Th4;
assume
A10: I is_closed_on s,P;
then
A11: I is_closed_on s2,P2;
assume
A12: I is_halting_on s,P;
then
A13: P2 halts_on s2;
A14: Comput(P3,s3,LifeSpan(P2,s2)+1)
= Comput(P3,Comput(P3,s3,1),LifeSpan(P2
,s2))
by EXTPRO_1:4;
A15: CurInstr(P3,
Comput(P3,s3,LifeSpan(P2,s2)+1))
=CurInstr(P3,
Comput(P3,s4,LifeSpan(P2,s2))) by A14
.=CurInstr(P2,
Comput(P2,s2,LifeSpan(P2,s2)))
by A11,A7,A9,A8,Th22,A2
.= halt SCMPDS by A13,EXTPRO_1:def 15;
then
A16: P3 halts_on s3 by EXTPRO_1:29;
A17: CurInstr(P3,s3) = i by A1,Th3;
now
let l be Nat;
assume
A18: l < LifeSpan(P2,s2) + 1;
A19: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
per cases;
suppose
l = 0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A19;
hence CurInstr(P3,Comput(
P3,s3,l))
<> halt SCMPDS by A17;
end;
suppose
l <> 0;
then consider n be Nat such that
A20: l = n + 1 by NAT_1:6;
reconsider n as Nat;
A21: n < LifeSpan(P2,s2) by A18,A20,XREAL_1:6;
assume
A22: CurInstr(P3,Comput(P3,
s3,l)) = halt SCMPDS;
A23: Comput(P3,s3,n+1)
= Comput(P3,Comput(P3,s3,1),n) by EXTPRO_1:4;
CurInstr(P2,Comput(P2,s2,n))
= CurInstr(P3,Comput(P3,s4,n))
by A11,A7,A9,A8,Th22,A2
.= halt SCMPDS by A20,A22,A23;
hence contradiction by A13,A21,EXTPRO_1:def 15;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds LifeSpan(P2,s2) + 1 <= l;
then
A24: LifeSpan(P3,s3) = LifeSpan(P2,s2) + 1 by A15,A16,EXTPRO_1:def 15;
A25: DataPart Result(P2,s2) = DataPart Comput(P2,s2,
LifeSpan(P2,s2)) by A13,EXTPRO_1:23
.= DataPart Comput(P3, s4,LifeSpan(P2,s2)) by A11,A7,A9,A8,Th22,A2
.= DataPart Comput(P3, s3,LifeSpan(P2,s2) + 1)
by EXTPRO_1:4
.= DataPart Result(P3,s3) by A16,A24,EXTPRO_1:23;
A26: now
let x be object;
A27: dom Start-At((card I+2),SCMPDS) = {IC SCMPDS} by FUNCOP_1:13;
assume
A28: x in dom IExec(IF,P,Initialize 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 SAl by A27,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= (Result(P2,s2)).x by A25,A29,SCMPDS_4:8
.= IExec(I,P,Initialize s).x
.= (IExec(I,P,Initialize s) +* SAl).x by A30,FUNCT_4:11;
end;
suppose
A31: x = IC SCMPDS;
A32: IC Result(P2,s2) = IC IExec(I,P,Initialize s)
.= card I by A10,A12,Th25;
A33: x in dom SAl by A27,A31,TARSKI:def 1;
thus IExec(IF,P,Initialize s).x = (Result(P3,s3)).x
.= Comput(P3, s3,LifeSpan(P2,s2) + 1).x by A16,A24,EXTPRO_1:23
.= IC Comput(P3, s4,LifeSpan(P2,s2)) by A31,EXTPRO_1:4
.= IC Comput(P2, s2,LifeSpan(P2,s2)) + 2
by A11,A7,A9,A8,Th22,A2
.= IC Result(P2,s2) + 2 by A13,EXTPRO_1:23
.= IC SAl by A32,FUNCOP_1:72
.= (IExec(I,P,Initialize s) +* SAl).x by A31,A33,FUNCT_4:13;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (IExec(I,P,Initialize s)
+* Start-At((card I+2),SCMPDS)) by PARTFUN1:def 2;
hence thesis by A26,FUNCT_1:2;
end;
theorem Th112:
for s being State of SCMPDS,I being Program of SCMPDS,a being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) < 0
holds IExec(if>=0(a,k1,I),P,Initialize s) = s +* Start-At((card I+2),SCMPDS)
proof
let s be State of SCMPDS,I be Program of SCMPDS,a be Int_position, k1 be
Integer;
set b=DataLoc(s.a,k1);
set IF=if>=0(a,k1,I), pIF=stop IF, s3 = Initialize s,
P3 = P +* pIF,
s4 = Comput(P3,s3,1), s5 = Comput(P3,s3,2), P4 = P3, P5 = P3;
set i = (a,k1)>=0_goto 2, j = goto (card I + 1);
set SAl=Start-At((card I+2),SCMPDS);
A1: IF =i ';' (j ';' I) by SCMPDS_4:16;
A2: not b in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
not a in dom Start-At(0,SCMPDS) by SCMPDS_4:18;
then
A3: s3.DataLoc(s3.a,k1)=s3.b by FUNCT_4:11
.= s.b by A2,FUNCT_4:11;
A4: IC s3 = 0 by MEMSTR_0:47;
A5: pIF c= P3 by FUNCT_4:25;
then
A6: pIF c= P4;
A7: pIF c= P5 by A5;
A8: Comput(P3, s3,0 + 1) = Following(P3,Comput(P3,s3,0)) by EXTPRO_1:3
.= Following(P3,s3) by EXTPRO_1:2
.= Exec(i,s3) by A1,Th3;
assume
s.b < 0;
then
A9: IC s4 = IC s3 + 1 by A8,A3,SCMPDS_2:57
.= (0+1) by A4;
A10: 1 in dom IF by Lm9;
then 1 in dom pIF by COMPOS_1:62;
then
A11: P4.1 = pIF. 1 by A6,GRFUNC_1:2
.=IF. 1 by A10,COMPOS_1:63
.=j by Lm10;
A12: P3/.IC s4 = P3.IC s4 by PBOOLE:143;
A13: Comput(P3, s3,1 + 1) = Following(P3,s4) by EXTPRO_1:3
.= Exec(j,s4) by A9,A11,A12;
then
A14: IC s5 = ICplusConst(s4,card I+1) by SCMPDS_2:54
.= (card I+1+1) by A9,Th4
.= (card I+(1+1));
A15: (P3)/.IC s5
= P3.IC s5 by PBOOLE:143;
A16: card IF=card I+2 by Lm8;
then (card I+2) in dom pIF by COMPOS_1:64;
then P5.(card I+2) = pIF.(card I+2) by A7,GRFUNC_1:2
.=halt SCMPDS by A16,COMPOS_1:64;
then
A17: CurInstr(P3,s5) = halt SCMPDS by A14,A15;
then
A18: P3 halts_on s3 by EXTPRO_1:29;
A19: CurInstr(P3,s3) = i by A1,Th3;
now
let l be Nat;
assume
l < 1+1;
then
A20: l <= 1 by NAT_1:13;
A21: Comput(P3,s3,0) = s3 by EXTPRO_1:2;
A22: P3/.IC Comput(P3,s3,l)
= P3.IC Comput(P3,s3,l) by PBOOLE:143;
per cases by A20,NAT_1:25;
suppose
l=0;
then CurInstr(P3,Comput(P3,s3,l))
= CurInstr(P3,s3)
by A21;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A19;
end;
suppose
l=1;
hence CurInstr(P3,Comput(P3,s3,l))
<> halt SCMPDS by A9,A11,A22;
end;
end;
then for l be Nat st CurInstr(P3,
Comput(P3,s3,l)) = halt SCMPDS
holds 2 <= l;
then LifeSpan(P3,s3) = 2 by A17,A18,EXTPRO_1:def 15;
then
A23: s5 = Result(P3,s3) by A18,EXTPRO_1:23;
A24: now
A25: dom SAl = {IC SCMPDS} by FUNCOP_1:13;
let x be object;
assume
A26: x in dom IExec(IF,P,Initialize s);
per cases by A26,SCMPDS_4:6;
suppose
A27: x is Int_position;
then x <> IC SCMPDS by SCMPDS_2:43;
then
A28: not x in dom SAl by A25,TARSKI:def 1;
A29: not x in dom Start-At(0,SCMPDS) by A27,SCMPDS_4:18;
thus IExec(IF,P,Initialize s).x = s5.x by A23
.= s4.x by A13,A27,SCMPDS_2:54
.= s3.x by A8,A27,SCMPDS_2:57
.= s.x by A29,FUNCT_4:11
.= (s +* SAl).x by A28,FUNCT_4:11;
end;
suppose
A30: x = IC SCMPDS;
hence IExec(IF,P,Initialize s).x = (card I + 2) by A14,A23
.= (s +* Start-At((card I+2),SCMPDS)).x by A30,FUNCT_4:113;
end;
end;
dom IExec(IF,P,Initialize s) = the carrier of SCMPDS by PARTFUN1:def 2
.= dom (s +* SAl) by PARTFUN1:def 2;
hence thesis by A24,FUNCT_1:2;
end;
registration
let I be shiftable parahalting Program of SCMPDS, a be Int_position,k1 be
Integer;
cluster if>=0(a,k1,I) -> shiftable parahalting;
correctness
proof
set i = (a,k1)>=0_goto 2, j = goto (card I + 1);
set IF=if>=0(a,k1,I), pIF = stop IF;
thus IF is shiftable;
let s be 0-started State of SCMPDS;
let P be Instruction-Sequence of SCMPDS;
A1: Initialize s = s by MEMSTR_0:44;
assume pIF c= P;
then
A2: P = P +* stop IF by FUNCT_4:98;
A3: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
per cases;
suppose
s.DataLoc(s.a,k1) >= 0;
then IF is_halting_on s,P by A3,Th109;
hence P halts_on s by A2,A1;
end;
suppose
s.DataLoc(s.a,k1) < 0;
then IF is_halting_on s,P by Th110;
hence P halts_on s by A2,A1;
end;
end;
end;
registration
let I be halt-free Program of SCMPDS, a be Int_position,k1 be Integer;
cluster if>=0(a,k1,I) -> halt-free;
coherence;
end;
theorem
for s being 0-started State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,a being Int_position,k1 being Integer
holds IC IExec(if>=0(a,k1,I),P,s) = card I + 2
proof
let s be 0-started State of SCMPDS,
I be halt-free shiftable parahalting Program of
SCMPDS,a be Int_position,k1 be Integer;
set IF=if>=0(a,k1,I);
A1: I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
A2: Initialize s = s by MEMSTR_0:44;
per cases;
suppose
s.DataLoc(s.a,k1) >= 0;
then IExec(IF,P,s) =IExec(I,P,s) +* Start-At((card I+2),SCMPDS)
by A1,Th111,A2;
hence thesis by FUNCT_4:113;
end;
suppose
s.DataLoc(s.a,k1) < 0;
then IExec(IF,P,s) =s +* Start-At((card I+2),SCMPDS) by Th112,A2;
hence thesis by FUNCT_4:113;
end;
end;
theorem
for s being State of SCMPDS,I being halt-free shiftable parahalting
Program of SCMPDS,a,b being Int_position,k1 being Integer st s.DataLoc(s.a,k1)
>= 0 holds IExec(if>=0(a,k1,I),P,Initialize s).b = IExec(I,P,Initialize s).b
proof
let s be State of SCMPDS,I be halt-free shiftable parahalting Program of
SCMPDS,a,b be Int_position,k1 be Integer;
assume
A1: s.DataLoc(s.a,k1) >= 0;
A2: not b in dom Start-At((card I+2),SCMPDS) by SCMPDS_4:18;
I is_closed_on s,P & I is_halting_on s,P by Th11,Th12;
then IExec(if>=0(a,k1,I),P,Initialize s) = IExec(I,P,Initialize s)
+* Start-At((card I+2),SCMPDS)
by A1,Th111;
hence thesis by A2,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS,a,b being
Int_position, k1 being Integer st s.DataLoc(s.a,k1) < 0
holds IExec(if>=0(a,k1,I),P,Initialize s).b = s.b
proof
let s be State of SCMPDS,I be Program of SCMPDS,a,b be Int_position, k1 be
Integer;
assume
s.DataLoc(s.a,k1) < 0;
then
A1: IExec(if>=0(a,k1,I),P,Initialize s) = s +* Start-At((card I+2),SCMPDS)
by Th112;
not b in dom Start-At((card I+2),SCMPDS) by SCMPDS_4:18;
hence thesis by A1,FUNCT_4:11;
end;
theorem
for s being State of SCMPDS,I being Program of SCMPDS
holds I is_closed_on s,P iff I is_closed_on Initialize s,P;
theorem
for s being State of SCMPDS,I being Program of SCMPDS
holds I is_halting_on s,P iff I is_halting_on Initialize s,P;