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;
A1: (Initialize s) +* (stop (while<0 (a,i,I))) = s +* (Initialize (stop (while<0 (a,i,I)))) by COMPOS_1:125;
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,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)))));
A3: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by COMPOS_1:125;
A4: (Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))) = (IExec (I,s)) +* (Initialize (stop (while<0 (a,i,I)))) by COMPOS_1:125;
assume A5: card I > 0 ; :: thesis:
assume A6: 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 A5, Th15;
then A7: ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I)))) halts_on (Initialize s) +* (stop (while<0 (a,i,I))) by SCMPDS_6:def 3;
A8: Initialize (stop I) c= (Initialize s) +* (stop I) by A3, FUNCT_4:26;
A9: for x being Int_position st x in X holds
s . x = s . x ;
then I is_halting_on s by A2, A6;
then A10: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by SCMPDS_6:def 3;
A11: (Initialize ((Initialize s) +* (stop I))) +* (stop I) = ((Initialize s) +* (stop I)) +* (Initialize (stop I)) by COMPOS_1:125;
(Initialize s) +* (stop I) = (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A8, A11, FUNCT_4:79;
then ProgramPart (((Initialize s) +* (stop I)) +* (Initialize (stop I))) halts_on (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A10, A11;
then A12: I is_halting_on (Initialize s) +* (stop I) by A11, SCMPDS_6:def 3;
A13: (IExec (I,s)) . a = s . a by A2, A6, A9;

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

A16: now

let x be Int_position ; :: thesis:
assume A17: x in X ; :: thesis:
hence t . x = (IExec (I,s)) . x by A14
.= s . x by A2, A6, A9, A17 ;
:: thesis:

end;

hence (IExec (I,t)) . a = t . a by A6, A13, A15; :: thesis:
thus (IExec (I,t)) . (DataLoc (((IExec (I,s)) . a),i)) > t . (DataLoc (((IExec (I,s)) . a),i)) by A6, A13, A15, A16; :: 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 A6, A13, A15, A16; :: thesis:

end;

then while<0 (a,i,I) is_halting_on IExec (I,s) by A5, Th15;
then A18: 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)))));
A19: dom (ProgramPart s) = NAT by COMPOS_1:34;
A20: dom (ProgramPart s) = (dom s) /\ NAT by RELAT_1:90
.= (({(IC )} \/ 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);
A21: IC ((Initialize s) +* (stop (while<0 (a,i,I)))) = 0 by SCMPDS_6:21;
A22: while<0 (a,i,I) = ((a,i) >=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
A23: 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 EXTPRO_1:4
.= Following ((ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I))))),((Initialize s) +* (stop (while<0 (a,i,I))))) by EXTPRO_1:3
.= Exec (((a,i) >=0_goto ((card I) + 2)),((Initialize s) +* (stop (while<0 (a,i,I))))) by A22, A1, SCMPDS_6:22 ;
A24: (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 A20, FUNCT_4:24 ;
A25: 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 A1, FUNCT_4:12
.= s . (DataLoc ((s . a),i)) by A25, A1, FUNCT_4:12 ;
then A26: 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 A2, A23, SCMPDS_2:69
.= 0 + 1 by A21 ;
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;
A27: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (while<0 (a,i,I)))) by COMPOS_1:138, FUNCT_7:134;

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

end;

then A28: 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 A29: (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));
A30: 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 A1, FUNCT_4:26, SCMPDS_6:17;
then A31: 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 A31, XBOOLE_1:1;
then A32: 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 A2, A6, A9;
then A33: I is_closed_on (Initialize s) +* (stop I) by SCMPDS_6:38;
then A34: 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 A5, A8, A12, A26, A28, A32, SCMPDS_7:36;
A35: (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 A36: 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 EXTPRO_1:5;
then A37: 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 A5, A8, A12, A33, A26, A28, A32, A35, 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 A29, A31, GRFUNC_1:8
.= goto (- ((card I) + 1)) by Th8 ;
A38: 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;
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)))) + 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 EXTPRO_1:4
.= 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 A37, A38 ;
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 A34, A36, SCMPDS_7:1 ;
then A40: 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;
A41: 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 A5, A8, A12, A33, A26, A28, A32, SCMPDS_7:36;

let x be Int_position ; :: thesis:
A42: not x in dom (Initialize (stop (while<0 (a,i,I)))) by SCMPDS_4:31;
A43: not x in dom (s | NAT) by A19, 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 A41, SCMPDS_4:23
.= (Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . x by A10, EXTPRO_1:23
.= (IExec (I,s)) . x by A30, A43, 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 A36, A39, SCMPDS_2:66
.= ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))) . x by A42, A4, FUNCT_4:12 ;
:: thesis:

end;

then A44: 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;
A45: 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 A4, 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 A20, FUNCT_4:24
.= ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I)))) by A1, 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 A46: 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 A44, A40, 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 A22, A45, A4, 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 A7, SCMPDS_6:2, SCMPDS_6:31;
then consider nn being Nat such that
A47: 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;
A48: ProgramPart ((Initialize s) +* (stop (while<0 (a,i,I)))) = ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I)))) by A46, 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 A46, EXTPRO_1:5;
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 A18, A48, EXTPRO_1:def 14;
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 A7, EXTPRO_1:def 14;
then A49: LifeSpan ((ProgramPart ((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))),((Initialize (IExec (I,s))) +* (stop (while<0 (a,i,I))))) >= nn by A47, XREAL_1:8;
A50: 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 A46, A47, EXTPRO_1:5;
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 A7, A48, EXTPRO_1:def 14;
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 A18, EXTPRO_1:def 14;
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 A49, 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 A7, A50, A48, EXTPRO_1:23;
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 A18, A24, EXTPRO_1:23
.= IExec ((while<0 (a,i,I)),(IExec (I,s))) by SCMPDS_4:def 8 ;
:: thesis: