let s be State of SCMPDS ; :: thesis: for I being shiftable No-StopCode Program of SCMPDS
for a being Int_position
for i being Integer
for X being set st s . (DataLoc (s . a),i) < 0 & card I > 0 & ( 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 ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
let I be shiftable No-StopCode Program of SCMPDS ; :: thesis: for a being Int_position
for i being Integer
for X being set st s . (DataLoc (s . a),i) < 0 & card I > 0 & ( 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 ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
let a be Int_position ; :: thesis: for i being Integer
for X being set st s . (DataLoc (s . a),i) < 0 & card I > 0 & ( 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 ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
let i be Integer; :: thesis: for X being set st s . (DataLoc (s . a),i) < 0 & card I > 0 & ( 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 ) ) ) holds
IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
let X be set ; :: thesis: ( s . (DataLoc (s . a),i) < 0 & card I > 0 & ( 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 ) ) ) implies IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s) )
set b = DataLoc (s . a),i;
set WHL = while<0 a,i,I;
set iWHL = Initialized (stop (while<0 a,i,I));
set iI = Initialized (stop I);
set s1 = s +* (Initialized (stop (while<0 a,i,I)));
set ps = s | NAT ;
set i1 = a,i >=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
assume A1: s . (DataLoc (s . a),i) < 0 ; :: thesis: ( not card I > 0 or ex 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 & not ( (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 ) ) ) or IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s) )
set Es = IExec I,s;
set bj = DataLoc ((IExec I,s) . a),i;
set sI = s +* (Initialized (stop I));
set m1 = (LifeSpan (s +* (Initialized (stop I)))) + 2;
set s2 = (IExec I,s) +* (Initialized (stop (while<0 a,i,I)));
set m2 = LifeSpan ((IExec I,s) +* (Initialized (stop (while<0 a,i,I))));
assume A2: card I > 0 ; :: thesis: ( ex 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 & not ( (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 ) ) ) or IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s) )
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: IExec (while<0 a,i,I),s = IExec (while<0 a,i,I),(IExec I,s)
then while<0 a,i,I is_halting_on s by A2, Th15;
then A4: ProgramPart (s +* (Initialized (stop (while<0 a,i,I)))) halts_on s +* (Initialized (stop (while<0 a,i,I))) by SCMPDS_6:def 3;
A5: Initialized (stop I) c= s +* (Initialized (stop I)) by 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 (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by SCMPDS_6:def 3;
s +* (Initialized (stop I)) = (s +* (Initialized (stop I))) +* (Initialized (stop I)) by A5, FUNCT_4:79;
then ProgramPart ((s +* (Initialized (stop I))) +* (Initialized (stop I))) halts_on (s +* (Initialized (stop I))) +* (Initialized (stop I)) by A7;
then A8: I is_halting_on s +* (Initialized (stop I)) by SCMPDS_6:def 3;
A9: (IExec I,s) . a = s . a by A1, A3, A6;

now

let t be State of SCMPDS ; :: thesis: ( ( for x being Int_position st x in X holds
t . x = (IExec I,s) . x ) & t . a = (IExec I,s) . a & t . (DataLoc ((IExec I,s) . a),i) < 0 implies ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc ((IExec I,s) . a),i) > t . (DataLoc ((IExec I,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 ) ) )
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: ( (IExec I,t) . a = t . a & (IExec I,t) . (DataLoc ((IExec I,s) . a),i) > t . (DataLoc ((IExec I,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 ) )

A12: now

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

end;

hence (IExec I,t) . a = t . a by A3, A9, A11; :: thesis: ( (IExec I,t) . (DataLoc ((IExec I,s) . a),i) > t . (DataLoc ((IExec I,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 ) )
thus (IExec I,t) . (DataLoc ((IExec I,s) . a),i) > t . (DataLoc ((IExec I,s) . a),i) by A3, A9, A11, A12; :: thesis: ( 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 ) )
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: verum

end;

then while<0 a,i,I is_halting_on IExec I,s by A2, Th15;
then A14: ProgramPart ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) halts_on (IExec I,s) +* (Initialized (stop (while<0 a,i,I))) by SCMPDS_6:def 3;
set m0 = LifeSpan (s +* (Initialized (stop (while<0 a,i,I))));
A15: dom (s | NAT ) = NAT by SCMPDS_6:1;
A16: dom (s | NAT ) = (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 (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1;
A17: IC (s +* (Initialized (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 (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),(0 + 1) = Following (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),0 ) by AMI_1:14
.= Following (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))) by AMI_1:13
.= Exec (a,i >=0_goto ((card I) + 2)),(s +* (Initialized (stop (while<0 a,i,I)))) by A18, SCMPDS_6:22 ;
A20: (IExec I,s) | NAT = ((Result (s +* (Initialized (stop I)))) +* (s | NAT )) | NAT by SCMPDS_4:def 8
.= s | NAT by A16, FUNCT_4:24 ;
A21: not DataLoc (s . a),i in dom (Initialized (stop (while<0 a,i,I))) by SCMPDS_4:31;
not a in dom (Initialized (stop (while<0 a,i,I))) by SCMPDS_4:31;
then (s +* (Initialized (stop (while<0 a,i,I)))) . (DataLoc ((s +* (Initialized (stop (while<0 a,i,I)))) . a),i) = (s +* (Initialized (stop (while<0 a,i,I)))) . (DataLoc (s . a),i) by FUNCT_4:12
.= s . (DataLoc (s . a),i) by A21, FUNCT_4:12 ;
then A22: IC (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1) = succ (IC (s +* (Initialized (stop (while<0 a,i,I))))) by A1, A19, SCMPDS_2:69
.= 0 + 1 by A17 ;
set mI = LifeSpan (s +* (Initialized (stop I)));
set s5 = Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))));
set l1 = (card I) + 1;
A23: DataPart (s +* (Initialized (stop I))) = DataPart (s +* (Initialized (stop (while<0 a,i,I)))) by SCMPDS_4:24, SCMPDS_4:36;

now

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

end;

then A24: DataPart (s +* (Initialized (stop I))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1) by SCMPDS_4:23;
set m3 = (LifeSpan (s +* (Initialized (stop I)))) + 1;
set s6 = Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (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 (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1);
A26: IExec I,s = (Result (s +* (Initialized (stop I)))) +* (s | NAT ) by SCMPDS_4:def 8;
( while<0 a,i,I c= Initialized (stop (while<0 a,i,I)) & Initialized (stop (while<0 a,i,I)) c= s +* (Initialized (stop (while<0 a,i,I))) ) by FUNCT_4:26, SCMPDS_6:17;
then A27: while<0 a,i,I c= s +* (Initialized (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= s +* (Initialized (stop (while<0 a,i,I))) by A27, XBOOLE_1:1;
then A28: Shift I,1 c= Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (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 s +* (Initialized (stop I)) by SCMPDS_6:38;
then A30: IC (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) = (card I) + 1 by A2, A5, A8, A22, A24, A28, SCMPDS_7:36;
Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) /. (IC (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) = (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . (IC (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) by AMI_1:150;
ProgramPart (s +* (Initialized (stop (while<0 a,i,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1) by AMI_1:144;
then A31: Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) = Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:51;
then A32: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . ((card I) + 1) by A2, A5, A8, A29, A22, A24, A28, SCMPDS_7:36, Y
.= (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1) . ((card I) + 1) by AMI_1:54
.= (s +* (Initialized (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 (s +* (Initialized (stop (while<0 a,i,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:144;
A33: Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) = Following (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:14
.= Exec (goto (- ((card I) + 1))),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by A32, T ;
then IC (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) = ICplusConst (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)),(0 - ((card I) + 1)) by SCMPDS_2:66
.= 0 by A30, A31, SCMPDS_7:1 ;
then A34: IC ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) = IC (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 2)) by SCMPDS_6:21;
A35: DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) by A2, A5, A8, A29, A22, A24, A28, SCMPDS_7:36;

now

let x be Int_position ; :: thesis: (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . x = ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) . x
A36: not x in dom (Initialized (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 (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . x = (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) . x by A35, SCMPDS_4:23
.= (Result (s +* (Initialized (stop I)))) . x by A7, AMI_1:122
.= (IExec I,s) . x by A26, A37, FUNCT_4:12 ;
hence (Comput (ProgramPart (s +* (Initialized (stop (while<0 a,i,I))))),(s +* (Initialized (stop (while<0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1)) . x = (IExec I,s) . x by A31, A33, SCMPDS_2:66
.= ((IExec I,s) +* (Initialized (stop (while<0 a,i,I)))) . x by A36, FUNCT_4:12 ;
:: thesis: verum

end;

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