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, c be Integer; :: thesis:
let X, Y be set ; :: thesis:
let f be Function of (product the Object-Kind of SCMPDS ),NAT ; :: 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;
set i1 = a,i <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
I1: (Initialize s) +* (stop (while>0 a,i,I)) = s +* (Initialize (stop (while>0 a,i,I))) by SCMPDS_4:5;
assume A1: s . (DataLoc (s . a),i) > 0 ; :: thesis:
set s4 = Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1;
A2: IC ((Initialize s) +* (stop (while>0 a,i,I))) = 0 by SCMPDS_6:21;
A3: while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by SCMPDS_4:51;
A4: 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 A3, I1, SCMPDS_6:22 ;
set m0 = LifeSpan (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I)));
A5: dom (ProgramPart s) = NAT by COMPOS_1:34;
A6: 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 Es = IExec I,s;
set bj = DataLoc ((IExec I,s) . a),i;
assume A7: card I > 0 ; :: thesis:
assume A8: for t being State of SCMPDS st f . (Dstate t) = 0 holds
t . (DataLoc (s . a),i) <= 0 ; :: thesis:
assume A9: for x being Int_position st x in X holds
s . x >= c + (s . (DataLoc (s . a),i)) ; :: thesis:
assume A10: for t being State of SCMPDS st ( for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in Y holds
t . x = s . x ) & t . a = s . a & t . (DataLoc (s . a),i) > 0 holds
( (IExec I,t) . a = t . a & I is_closed_on t & I is_halting_on t & f . (Dstate (IExec I,t)) < f . (Dstate t) & ( for x being Int_position st x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc (s . a),i)) ) & ( for x being Int_position st x in Y holds
(IExec I,t) . x = t . x ) ) ; :: thesis:
then while>0 a,i,I is_halting_on s by A7, A8, A9, Th24;
then A11: ProgramPart ((Initialize s) +* (stop (while>0 a,i,I))) halts_on (Initialize s) +* (stop (while>0 a,i,I)) by SCMPDS_6:def 3;
A12: for x being Int_position st x in Y holds
s . x = s . x ;
then A13: DataLoc ((IExec I,s) . a),i = DataLoc (s . a),i by A1, A9, A10;
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;
A14: Initialize (stop I) c= (Initialize s) +* (stop I) by I2, FUNCT_4:26;
A15: (IExec I,s) . a = s . a by A1, A9, A10, A12;

A16: now

let t be State of SCMPDS ; :: thesis:
assume that
A17: for x being Int_position st x in X holds
t . x >= c + (t . (DataLoc ((IExec I,s) . a),i)) and
A18: for x being Int_position st x in Y holds
t . x = (IExec I,s) . x and
A19: t . a = (IExec I,s) . a and
A20: t . (DataLoc ((IExec I,s) . a),i) > 0 ; :: thesis:

A21: now

let x be Int_position ; :: thesis:
assume A22: x in Y ; :: thesis:
hence t . x = (IExec I,s) . x by A18
.= s . x by A1, A9, A10, A12, A22 ;
:: thesis:

end;

hence (IExec I,t) . a = t . a by A10, A15, A17, A19, A20; :: thesis:
A23: t . a = s . a by A1, A9, A10, A12, A19;
hence ( I is_closed_on t & I is_halting_on t ) by A10, A17, A19, A20, A21; :: thesis:
thus f . (Dstate (IExec I,t)) < f . (Dstate t) by A10, A17, A19, A20, A21, A23; :: thesis:
thus for x being Int_position st x in X holds
(IExec I,t) . x >= c + ((IExec I,t) . (DataLoc ((IExec I,s) . a),i)) by A10, A15, A17, A19, A20, A21; :: thesis:
thus for x being Int_position st x in Y holds
(IExec I,t) . x = t . x by A10, A17, A19, A20, A21, A23; :: thesis:

end;

for x being Int_position st x in X holds
(IExec I,s) . x >= c + ((IExec I,s) . (DataLoc ((IExec I,s) . a),i)) by A1, A9, A10, A12, A15;
then while>0 a,i,I is_halting_on IExec I,s by A7, A8, A13, A16, Th24;
then A24: 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;
A25: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (while>0 a,i,I))) by FUNCT_7:134, SCMPDS_4:24;

now

let a be Int_position ; :: thesis:
thus ((Initialize s) +* (stop I)) . a = ((Initialize s) +* (stop (while>0 a,i,I))) . a by A25, SCMPDS_4:23
.= (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1) . a by A4, SCMPDS_2:68 ; :: thesis:

end;

then A26: 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 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;
( 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;
set m3 = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1;
A28: IExec I,s = (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (s | NAT ) by SCMPDS_4:def 8;
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);
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 Th18;
Shift I,1 c= while>0 a,i,I by Lm4;
then Shift I,1 c= (Initialize s) +* (stop (while>0 a,i,I)) by A27, XBOOLE_1:1;
then A30: 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_halting_on s by A1, A9, A10, A12;
then A31: 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 A14, I4, FUNCT_4:79;
then ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop I)) halts_on (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A31;
then A32: I is_halting_on (Initialize s) +* (stop I) by SCMPDS_6:def 3;
A33: ProgramPart (IExec I,s) = ProgramPart ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (ProgramPart s)) by SCMPDS_4:def 8
.= ProgramPart s by A6, FUNCT_4:24 ;
A34: 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 A34, I1, FUNCT_4:12 ;
then A35: 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, A4, SCMPDS_2:68
.= 0 + 1 by A2 ;
I is_closed_on s by A1, A9, A10, A12;
then A36: I is_closed_on (Initialize s) +* (stop I) by SCMPDS_6:38;
then A37: 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 A7, A14, A32, A35, A26, A30, 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 A38: 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 A39: 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 A7, A14, A32, A36, A35, A26, A30, 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 A29, A27, GRFUNC_1:8
.= goto (- ((card I) + 1)) by Th19 ;
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;
A40: 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 A39, 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 A37, A38, SCMPDS_7:1 ;
then A41: 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;
A42: 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 A7, A14, A32, A36, A35, A26, A30, SCMPDS_7:36;

now

let x be Int_position ; :: thesis:
A43: not x in dom (Initialize (stop (while>0 a,i,I))) by SCMPDS_4:31;
A44: not x in dom (s | NAT ) by A5, 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 A42, SCMPDS_4:23
.= (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) . x by A31, AMI_1:122
.= (IExec I,s) . x by A28, A44, 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 A38, A40, SCMPDS_2:66
.= ((Initialize (IExec I,s)) +* (stop (while>0 a,i,I))) . x by A43, I3, FUNCT_4:12 ;
:: thesis:

end;

then A45: 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 A6, 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 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 A45, A41, 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 A3, 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 A11, SCMPDS_6:2, SCMPDS_6:30;
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;
T: 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, 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 A24, 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 A11, AMI_1:def 46;
then A48: 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;
A49: 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, 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 A11, 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 A24, 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 A48, 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 A11, A49, 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 A24, A33, AMI_1:122
.= IExec (while>0 a,i,I),(IExec I,s) by SCMPDS_4:def 8 ;
:: thesis: