let P be Instruction-Sequence of SCMPDS; :: thesis:
let s be 0 -started State of SCMPDS; :: thesis:
let I be halt-free shiftable Program of SCMPDS; :: thesis:
let a be Int_position; :: thesis:
let i be Integer; :: thesis:
let X be set ; :: thesis:
A1: Initialize s = s by MEMSTR_0:44;
set b = DataLoc ((s . a),i);
set WHL = while<0 (a,i,I);
set pWHL = stop (while<0 (a,i,I));
set P1 = P +* (stop (while<0 (a,i,I)));
set i1 = (a,i) >=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
assume A2: s . (DataLoc ((s . a),i)) < 0 ; :: thesis:
set Es = IExec (I,P,s);
set bj = DataLoc (((Initialize (IExec (I,P,s))) . a),i);
set EP = P;
set PI = P +* (stop I);
set m1 = (LifeSpan ((P +* (stop I)),s)) + 2;
set s2 = Initialize (IExec (I,P,s));
set P2 = P +* (stop (while<0 (a,i,I)));
set m2 = LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))));
assume A3: for t being 0 -started State of SCMPDS
for Q being Instruction-Sequence of SCMPDS st ( for x being Int_position st x in X holds
t . x = s . x ) & t . a = s . a & t . (DataLoc ((s . a),i)) < 0 holds
( (IExec (I,Q,t)) . a = t . a & (IExec (I,Q,t)) . (DataLoc ((s . a),i)) > t . (DataLoc ((s . a),i)) & I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) ; :: thesis:
then while<0 (a,i,I) is_halting_on s,P by Th13;
then A4: P +* (stop (while<0 (a,i,I))) halts_on s by A1, SCMPDS_6:def 3;
A5: stop I c= P +* (stop I) by FUNCT_4:25;
A6: for x being Int_position st x in X holds
s . x = s . x ;
then I is_halting_on s,P by A2, A3;
then A7: P +* (stop I) halts_on s by A1, SCMPDS_6:def 3;
(P +* (stop I)) +* (stop I) halts_on s by A7;
then A8: I is_halting_on s,P +* (stop I) by A1, SCMPDS_6:def 3;
A9: (Initialize (IExec (I,P,s))) . a = (IExec (I,P,s)) . a by SCMPDS_5:15
.= s . a by A2, A3, A6 ;

now :: thesis:

let t be 0 -started State of SCMPDS; :: thesis:
let Q be Instruction-Sequence of SCMPDS; :: thesis:
assume that
A10: for x being Int_position st x in X holds
t . x = (Initialize (IExec (I,P,s))) . x and
A11: ( t . a = (Initialize (IExec (I,P,s))) . a & t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) < 0 ) ; :: thesis:

A12: now :: thesis:

let x be Int_position; :: thesis:
assume A13: x in X ; :: thesis:
hence t . x = (Initialize (IExec (I,P,s))) . x by A10
.= (IExec (I,P,s)) . x by SCMPDS_5:15
.= s . x by A2, A3, A6, A13 ;
:: thesis:

end;

hence (IExec (I,Q,t)) . a = t . a by A3, A9, A11; :: thesis:
thus (IExec (I,Q,t)) . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) > t . (DataLoc (((Initialize (IExec (I,P,s))) . a),i)) by A3, A9, A11, A12; :: thesis:
thus ( I is_closed_on t,Q & I is_halting_on t,Q & ( for x being Int_position st x in X holds
(IExec (I,Q,t)) . x = t . x ) ) by A3, A9, A11, A12; :: thesis:

end;

then while<0 (a,i,I) is_halting_on Initialize (IExec (I,P,s)),P by Th13;
then A14: P +* (stop (while<0 (a,i,I))) halts_on Initialize (Initialize (IExec (I,P,s))) by SCMPDS_6:def 3;
set m0 = LifeSpan ((P +* (stop (while<0 (a,i,I)))),s);
set s4 = Comput ((P +* (stop (while<0 (a,i,I)))),s,1);
set P4 = P +* (stop (while<0 (a,i,I)));
A15: IC s = 0 by MEMSTR_0:def 11;
A16: while<0 (a,i,I) = ((a,i) >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:15;
A17: Comput ((P +* (stop (while<0 (a,i,I)))),s,(0 + 1)) = Following ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,0))) by EXTPRO_1:3
.= Following ((P +* (stop (while<0 (a,i,I)))),s)
.= Exec (((a,i) >=0_goto ((card I) + 2)),s) by A16, A1, SCMPDS_6:11 ;
A18: IC (Comput ((P +* (stop (while<0 (a,i,I)))),s,1)) = (IC s) + 1 by A2, A17, SCMPDS_2:57
.= 0 + 1 by A15 ;
set mI = LifeSpan ((P +* (stop I)),s);
set s5 = Comput ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)));
set P5 = P +* (stop (while<0 (a,i,I)));
set l1 = (card I) + 1;
for a being Int_position holds s . a = (Comput ((P +* (stop (while<0 (a,i,I)))),s,1)) . a by A17, SCMPDS_2:57;
then A19: DataPart s = DataPart (Comput ((P +* (stop (while<0 (a,i,I)))),s,1)) by SCMPDS_4:8;
set m3 = (LifeSpan ((P +* (stop I)),s)) + 1;
set s6 = Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1));
set P6 = P +* (stop (while<0 (a,i,I)));
(card I) + 1 < (card I) + 2 by XREAL_1:6;
then A20: (card I) + 1 in dom (while<0 (a,i,I)) by Th5;
set s7 = Comput ((P +* (stop (while<0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1));
A21: while<0 (a,i,I) c= stop (while<0 (a,i,I)) by AFINSQ_1:74;
stop (while<0 (a,i,I)) c= P +* (stop (while<0 (a,i,I))) by FUNCT_4:25;
then A22: while<0 (a,i,I) c= P +* (stop (while<0 (a,i,I))) by A21, XBOOLE_1:1;
Shift (I,1) c= while<0 (a,i,I) by Lm2;
then A23: Shift (I,1) c= P +* (stop (while<0 (a,i,I))) by A22, XBOOLE_1:1;
A24: I is_closed_on s,P +* (stop I) by A2, A3, A6;
then A25: IC (Comput ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) = (card I) + 1 by A5, A8, A18, A19, A23, SCMPDS_7:18;
A26: (P +* (stop (while<0 (a,i,I)))) /. (IC (Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (while<0 (a,i,I)))) . (IC (Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by PBOOLE:143;
A27: Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)) = Comput ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s))) by EXTPRO_1:4;
then A28: CurInstr ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (while<0 (a,i,I)))) . ((card I) + 1) by A5, A8, A24, A18, A19, A23, A26, SCMPDS_7:18
.= (while<0 (a,i,I)) . ((card I) + 1) by A20, A22, GRFUNC_1:2
.= goto (- ((card I) + 1)) by Th6 ;
A29: Comput ((P +* (stop (while<0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1)) = Following ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card I) + 1))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by A28 ;
then IC (Comput ((P +* (stop (while<0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) = ICplusConst ((Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 1))),(0 - ((card I) + 1))) by SCMPDS_2:54
.= 0 by A25, A27, SCMPDS_7:1 ;
then A30: IC (Initialize (IExec (I,P,s))) = IC (Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2))) by MEMSTR_0:def 11;
A31: DataPart (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) = DataPart (Comput ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) by A5, A8, A24, A18, A19, A23, SCMPDS_7:18;

now :: thesis:

let x be Int_position; :: thesis:
A32: not x in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
(Comput ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,1)),(LifeSpan ((P +* (stop I)),s)))) . x = (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) . x by A31, SCMPDS_4:8
.= (Result ((P +* (stop I)),s)) . x by A7, EXTPRO_1:23
.= (IExec (I,P,s)) . x by SCMPDS_4:def 5 ;
hence (Comput ((P +* (stop (while<0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) . x = (IExec (I,P,s)) . x by A27, A29, SCMPDS_2:54
.= (Initialize (IExec (I,P,s))) . x by A32, FUNCT_4:11 ;
:: thesis:

end;

then A33: DataPart (Comput ((P +* (stop (while<0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 1) + 1))) = DataPart (Initialize (IExec (I,P,s))) by SCMPDS_4:8;
A34: Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2)) = Initialize (IExec (I,P,s)) by A33, A30, MEMSTR_0:78;
then CurInstr ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,((LifeSpan ((P +* (stop I)),s)) + 2)))) = (a,i) >=0_goto ((card I) + 2) by A16, SCMPDS_6:11;
then LifeSpan ((P +* (stop (while<0 (a,i,I)))),s) > (LifeSpan ((P +* (stop I)),s)) + 2 by A4, EXTPRO_1:36, SCMPDS_6:18;
then consider nn being Nat such that
A35: LifeSpan ((P +* (stop (while<0 (a,i,I)))),s) = ((LifeSpan ((P +* (stop I)),s)) + 2) + nn by NAT_1:10;
reconsider nn = nn as Nat ;
Comput ((P +* (stop (while<0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))))))) = Comput ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by A34, EXTPRO_1:4;
then CurInstr ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),s,(((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))))))))) = halt SCMPDS by A14, EXTPRO_1:def 15;
then ((LifeSpan ((P +* (stop I)),s)) + 2) + (LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))))) >= LifeSpan ((P +* (stop (while<0 (a,i,I)))),s) by A4, EXTPRO_1:def 15;
then A36: LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s)))) >= nn by A35, XREAL_1:6;
A37: Comput ((P +* (stop (while<0 (a,i,I)))),s,(LifeSpan ((P +* (stop (while<0 (a,i,I)))),s))) = Comput ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))),nn) by A34, A35, EXTPRO_1:4;
then CurInstr ((P +* (stop (while<0 (a,i,I)))),(Comput ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))),nn))) = halt SCMPDS by A4, EXTPRO_1:def 15;
then nn >= LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A14, EXTPRO_1:def 15;
then nn = LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A36, XXREAL_0:1;
then Result ((P +* (stop (while<0 (a,i,I)))),s) = Comput ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by A4, A37, EXTPRO_1:23;
hence IExec ((while<0 (a,i,I)),P,s) = Comput ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s))),(LifeSpan ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s)))))) by SCMPDS_4:def 5
.= Result ((P +* (stop (while<0 (a,i,I)))),(Initialize (IExec (I,P,s)))) by A14, EXTPRO_1:23
.= IExec ((while<0 (a,i,I)),P,(Initialize (IExec (I,P,s)))) by SCMPDS_4:def 5 ;
:: thesis: