let s be 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:
set b = DataLoc (s . a),i;
set WHL = while<0 a,i,I;
set pWHL = stop (while<0 a,i,I);
set s1 = (Initialize s) +* (stop (while<0 a,i,I));
set ps = ProgramPart s;
I1: (Initialize s) +* (stop (while<0 a,i,I)) = s +* (Initialize (stop (while<0 a,i,I))) by SCMPDS_4:5;
set i1 = a,i >=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
assume A1: s . (DataLoc (s . a),i) < 0 ; :: thesis:
set Es = IExec I,s;
set bj = DataLoc ((IExec I,s) . a),i;
set sI = (Initialize s) +* (stop I);
set m1 = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2;
set s2 = (Initialize (IExec I,s)) +* (stop (while<0 a,i,I));
set m2 = LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)));
I2: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by SCMPDS_4:5;
I3: (Initialize (IExec I,s)) +* (stop (while<0 a,i,I)) = (IExec I,s) +* (Initialize (stop (while<0 a,i,I))) by SCMPDS_4:5;
assume A2: card I > 0 ; :: thesis:
assume A3: for t being State 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,t) . a = t . a & (IExec I,t) . (DataLoc (s . a),i) > t . (DataLoc (s . a),i) & I is_closed_on t & I is_halting_on t & ( for x being Int_position st x in X holds
(IExec I,t) . x = t . x ) ) ; :: thesis:
then while<0 a,i,I is_halting_on s by A2, Th15;
then A4: ProgramPart ((Initialize s) +* (stop (while<0 a,i,I))) halts_on (Initialize s) +* (stop (while<0 a,i,I)) by SCMPDS_6:def 3;
A5: Initialize (stop I) c= (Initialize s) +* (stop I) by I2, FUNCT_4:26;
A6: for x being Int_position st x in X holds
s . x = s . x ;
then I is_halting_on s by A1, A3;
then A7: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by SCMPDS_6:def 3;
I4: (Initialize ((Initialize s) +* (stop I))) +* (stop I) = ((Initialize s) +* (stop I)) +* (Initialize (stop I)) by SCMPDS_4:5;
(Initialize s) +* (stop I) = (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A5, I4, FUNCT_4:79;
then ProgramPart (((Initialize s) +* (stop I)) +* (Initialize (stop I))) halts_on (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A7, I4;
then A8: I is_halting_on (Initialize s) +* (stop I) by I4, SCMPDS_6:def 3;
A9: (IExec I,s) . a = s . a by A1, A3, A6;

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

A12: now

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

end;

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

end;

then while<0 a,i,I is_halting_on IExec I,s by A2, Th15;
then A14: ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) halts_on (Initialize (IExec I,s)) +* (stop (while<0 a,i,I)) by SCMPDS_6:def 3;
set m0 = LifeSpan (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I)));
A15: dom (ProgramPart s) = NAT by COMPOS_1:34;
A16: dom (ProgramPart s) = (dom s) /\ NAT by RELAT_1:90
.= (({(IC SCMPDS )} \/ SCM-Data-Loc ) \/ NAT ) /\ NAT by SCMPDS_4:19
.= NAT by XBOOLE_1:21 ;
set s4 = Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1;
A17: IC ((Initialize s) +* (stop (while<0 a,i,I))) = 0 by SCMPDS_6:21;
A18: while<0 a,i,I = (a,i >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
A19: Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(0 + 1) = Following (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),0 ) by AMI_1:14
.= Following (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))) by AMI_1:13
.= Exec (a,i >=0_goto ((card I) + 2)),((Initialize s) +* (stop (while<0 a,i,I))) by A18, I1, SCMPDS_6:22 ;
A20: (IExec I,s) | NAT = ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (ProgramPart s)) | NAT by SCMPDS_4:def 8
.= ProgramPart s by A16, FUNCT_4:24 ;
A21: not DataLoc (s . a),i in dom (Initialize (stop (while<0 a,i,I))) by SCMPDS_4:31;
not a in dom (Initialize (stop (while<0 a,i,I))) by SCMPDS_4:31;
then ((Initialize s) +* (stop (while<0 a,i,I))) . (DataLoc (((Initialize s) +* (stop (while<0 a,i,I))) . a),i) = ((Initialize s) +* (stop (while<0 a,i,I))) . (DataLoc (s . a),i) by I1, FUNCT_4:12
.= s . (DataLoc (s . a),i) by A21, I1, FUNCT_4:12 ;
then A22: IC (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1) = succ (IC ((Initialize s) +* (stop (while<0 a,i,I)))) by A1, A19, SCMPDS_2:69
.= 0 + 1 by A17 ;
set mI = LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I));
set s5 = Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
set l1 = (card I) + 1;
A23: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (while<0 a,i,I))) by FUNCT_7:134, SCMPDS_4:24;

let a be Int_position ; :: thesis:
thus ((Initialize s) +* (stop I)) . a = ((Initialize s) +* (stop (while<0 a,i,I))) . a by A23, SCMPDS_4:23
.= (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1) . a by A19, SCMPDS_2:69 ; :: thesis:

end;

then A24: DataPart ((Initialize s) +* (stop I)) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1) by SCMPDS_4:23;
set m3 = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1;
set s6 = Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1);
(card I) + 1 < (card I) + 2 by XREAL_1:8;
then A25: (card I) + 1 in dom (while<0 a,i,I) by Th7;
set s7 = Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1);
A26: IExec I,s = (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (s | NAT ) by SCMPDS_4:def 8;
( while<0 a,i,I c= Initialize (stop (while<0 a,i,I)) & Initialize (stop (while<0 a,i,I)) c= (Initialize s) +* (stop (while<0 a,i,I)) ) by I1, FUNCT_4:26, SCMPDS_6:17;
then A27: while<0 a,i,I c= (Initialize s) +* (stop (while<0 a,i,I)) by XBOOLE_1:1;
Shift I,1 c= while<0 a,i,I by Lm2;
then Shift I,1 c= (Initialize s) +* (stop (while<0 a,i,I)) by A27, XBOOLE_1:1;
then A28: Shift I,1 c= Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1 by AMI_1:81;
I is_closed_on s by A1, A3, A6;
then A29: I is_closed_on (Initialize s) +* (stop I) by SCMPDS_6:38;
then A30: IC (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = (card I) + 1 by A2, A5, A8, A22, A24, A28, SCMPDS_7:36;
Y: (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) = (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) . (IC (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))) by COMPOS_1:38;
ProgramPart ((Initialize s) +* (stop (while<0 a,i,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1) by AMI_1:123;
then A31: Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) = Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by AMI_1:51;
then A32: CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) = (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . ((card I) + 1) by A2, A5, A8, A29, A22, A24, A28, Y, SCMPDS_7:36
.= (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1) . ((card I) + 1) by AMI_1:54
.= ((Initialize s) +* (stop (while<0 a,i,I))) . ((card I) + 1) by AMI_1:54
.= (while<0 a,i,I) . ((card I) + 1) by A25, A27, GRFUNC_1:8
.= goto (- ((card I) + 1)) by Th8 ;
T: ProgramPart ((Initialize s) +* (stop (while<0 a,i,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by AMI_1:123;
A33: Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1) = Following (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by AMI_1:14
.= Exec (goto (- ((card I) + 1))),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by A32, T ;
then IC (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) = ICplusConst (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)),(0 - ((card I) + 1)) by SCMPDS_2:66
.= 0 by A30, A31, SCMPDS_7:1 ;
then A34: IC ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) = IC (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2)) by SCMPDS_6:21;
A35: DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A2, A5, A8, A29, A22, A24, A28, SCMPDS_7:36;

let x be Int_position ; :: thesis:
A36: not x in dom (Initialize (stop (while<0 a,i,I))) by SCMPDS_4:31;
A37: not x in dom (s | NAT ) by A15, SCMPDS_2:53;
(Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . x = (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . x by A35, SCMPDS_4:23
.= (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) . x by A7, AMI_1:122
.= (IExec I,s) . x by A26, A37, FUNCT_4:12 ;
hence (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) . x = (IExec I,s) . x by A31, A33, SCMPDS_2:66
.= ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) . x by A36, I3, FUNCT_4:12 ;
:: thesis:

end;

then A38: DataPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) = DataPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) by SCMPDS_4:23;
TX: ProgramPart ((Initialize s) +* (stop (while<0 a,i,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2)) by AMI_1:123;
ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) = ProgramPart (((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (ProgramPart s)) +* (Initialize (stop (while<0 a,i,I)))) by I3, SCMPDS_4:def 8
.= (ProgramPart ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (ProgramPart s))) +* (ProgramPart (Initialize (stop (while<0 a,i,I)))) by FUNCT_4:75
.= (ProgramPart s) +* (ProgramPart (Initialize (stop (while<0 a,i,I)))) by A16, FUNCT_4:24
.= ProgramPart ((Initialize s) +* (stop (while<0 a,i,I))) by I1, FUNCT_4:75
.= ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2)) by AMI_1:123 ;
then A39: Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2) = (Initialize (IExec I,s)) +* (stop (while<0 a,i,I)) by A38, A34, SCMPDS_7:7;
then CurInstr (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2)) = a,i >=0_goto ((card I) + 2) by A18, TX, I3, SCMPDS_6:22;
then LifeSpan (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))) > (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2 by A4, SCMPDS_6:2, SCMPDS_6:31;
then consider nn being Nat such that
A40: LifeSpan (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))) = ((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2) + nn by NAT_1:10;
reconsider nn = nn as Element of NAT by ORDINAL1:def 13;
T: ProgramPart ((Initialize s) +* (stop (while<0 a,i,I))) = ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) by A39, AMI_1:123;
Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2) + (LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))))) = Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))),(LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))) by A39, AMI_1:51;
then CurInstr (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2) + (LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))))) = halt SCMPDS by A14, T, AMI_1:def 46;
then ((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2) + (LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))) >= LifeSpan (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))) by A4, AMI_1:def 46;
then A41: LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) >= nn by A40, XREAL_1:8;
A42: Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))),(LifeSpan (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I)))) = Comput (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))),nn by A39, A40, AMI_1:51;
then CurInstr (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),(Comput (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))),nn) = halt SCMPDS by A4, T, AMI_1:def 46;
then nn >= LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) by A14, AMI_1:def 46;
then nn = LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))) by A41, XXREAL_0:1;
then Result (ProgramPart ((Initialize s) +* (stop (while<0 a,i,I)))),((Initialize s) +* (stop (while<0 a,i,I))) = Comput (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))),(LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))) by A4, A42, T, AMI_1:122;
hence IExec (while<0 a,i,I),s = (Comput (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))),(LifeSpan (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I))))) +* (ProgramPart s) by SCMPDS_4:def 8
.= (Result (ProgramPart ((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))),((Initialize (IExec I,s)) +* (stop (while<0 a,i,I)))) +* ((IExec I,s) | NAT ) by A14, A20, AMI_1:122
.= IExec (while<0 a,i,I),(IExec I,s) by SCMPDS_4:def 8 ;
:: thesis: