let P be Instruction-Sequence of SCMPDS; :: thesis: for s, sm being State of SCMPDS
for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for m being Nat st I is_closed_on s,P & I is_halting_on s,P & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((P +* (stop I)),())) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(),m) holds
( DataPart sm = DataPart (IExec (I,P,())) & Initialize sm = sm )

let s, sm be State of SCMPDS; :: thesis: for I being halt-free shiftable Program of
for a being Int_position
for i being Integer
for m being Nat st I is_closed_on s,P & I is_halting_on s,P & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((P +* (stop I)),())) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(),m) holds
( DataPart sm = DataPart (IExec (I,P,())) & Initialize sm = sm )

let I be halt-free shiftable Program of ; :: thesis: for a being Int_position
for i being Integer
for m being Nat st I is_closed_on s,P & I is_halting_on s,P & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((P +* (stop I)),())) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(),m) holds
( DataPart sm = DataPart (IExec (I,P,())) & Initialize sm = sm )

let a be Int_position; :: thesis: for i being Integer
for m being Nat st I is_closed_on s,P & I is_halting_on s,P & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((P +* (stop I)),())) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(),m) holds
( DataPart sm = DataPart (IExec (I,P,())) & Initialize sm = sm )

let i be Integer; :: thesis: for m being Nat st I is_closed_on s,P & I is_halting_on s,P & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((P +* (stop I)),())) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(),m) holds
( DataPart sm = DataPart (IExec (I,P,())) & Initialize sm = sm )

let m be Nat; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((P +* (stop I)),())) + 2 & sm = Comput ((P +* (stop (while>0 (a,i,I)))),(),m) implies ( DataPart sm = DataPart (IExec (I,P,())) & Initialize sm = sm ) )
set b = DataLoc ((s . a),i);
set WH = while>0 (a,i,I);
set iWH = stop (while>0 (a,i,I));
set IsI = stop I;
set i1 = (a,i) <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
set s2 = Initialize s;
set P2 = P +* (stop I);
set s3 = Initialize s;
set P3 = P +* (stop (while>0 (a,i,I)));
set s4 = Comput ((P +* (stop (while>0 (a,i,I)))),(),1);
set P4 = P +* (stop (while>0 (a,i,I)));
assume that
A1: I is_closed_on s,P and
A2: I is_halting_on s,P and
A3: s . (DataLoc ((s . a),i)) > 0 and
A4: m = (LifeSpan ((P +* (stop I)),())) + 2 and
A5: sm = Comput ((P +* (stop (while>0 (a,i,I)))),(),m) ; :: thesis: ( DataPart sm = DataPart (IExec (I,P,())) & Initialize sm = sm )
A6: stop I c= P +* (stop I) by FUNCT_4:25;
A7: stop (while>0 (a,i,I)) c= P +* (stop (while>0 (a,i,I))) by FUNCT_4:25;
while>0 (a,i,I) c= stop (while>0 (a,i,I)) by AFINSQ_1:74;
then A8: while>0 (a,i,I) c= P +* (stop (while>0 (a,i,I))) by ;
Shift (I,1) c= while>0 (a,i,I) by Lm2;
then A9: Shift (I,1) c= P +* (stop (while>0 (a,i,I))) by ;
A10: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by Lm1;
A11: Comput ((P +* (stop (while>0 (a,i,I)))),(),(0 + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),0))) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 2)),()) by ;
set m2 = LifeSpan ((P +* (stop I)),());
set s5 = Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),1)),(LifeSpan ((P +* (stop I)),())));
set P5 = P +* (stop (while>0 (a,i,I)));
set l1 = (card I) + 1;
A12: IC () = 0 by MEMSTR_0:def 11;
A13: not DataLoc ((s . a),i) in dom () by SCMPDS_4:18;
not a in dom () by SCMPDS_4:18;
then A14: () . (DataLoc ((() . a),i)) = () . (DataLoc ((s . a),i)) by FUNCT_4:11
.= s . (DataLoc ((s . a),i)) by ;
set m3 = (LifeSpan ((P +* (stop I)),())) + 1;
set s6 = Comput ((P +* (stop (while>0 (a,i,I)))),(),((LifeSpan ((P +* (stop I)),())) + 1));
set P6 = P +* (stop (while>0 (a,i,I)));
A15: Comput ((P +* (stop (while>0 (a,i,I)))),(),((LifeSpan ((P +* (stop I)),())) + 1)) = Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),1)),(LifeSpan ((P +* (stop I)),()))) by EXTPRO_1:4;
set s7 = Comput ((P +* (stop (while>0 (a,i,I)))),(),(((LifeSpan ((P +* (stop I)),())) + 1) + 1));
(card I) + 1 < (card I) + 2 by XREAL_1:6;
then A16: (card I) + 1 in dom (while>0 (a,i,I)) by SCMPDS_8:18;
A17: I is_closed_on Initialize s,P +* (stop I) by ;
for x being Int_position holds () . x = (Comput ((P +* (stop (while>0 (a,i,I)))),(),1)) . x by ;
then A18: DataPart () = DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),(),1)) by SCMPDS_4:8;
A19: P +* (stop I) halts_on Initialize s by ;
(P +* (stop I)) +* (stop I) halts_on Initialize () by ;
then A20: I is_halting_on Initialize s,P +* (stop I) by SCMPDS_6:def 3;
A21: IC (Comput ((P +* (stop (while>0 (a,i,I)))),(),1)) = 0 + 1 by ;
then DataPart (Comput ((P +* (stop I)),(),(LifeSpan ((P +* (stop I)),())))) = DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),1)),(LifeSpan ((P +* (stop I)),())))) by ;
then A22: DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),1)),(LifeSpan ((P +* (stop I)),())))) = DataPart (Result ((P +* (stop I)),())) by
.= DataPart (IExec (I,P,())) by SCMPDS_4:def 5 ;
A23: IC (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),1)),(LifeSpan ((P +* (stop I)),())))) = (card I) + 1 by ;
then A24: CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),((LifeSpan ((P +* (stop I)),())) + 1)))) = (P +* (stop (while>0 (a,i,I)))) . ((card I) + 1) by
.= (while>0 (a,i,I)) . ((card I) + 1) by
.= goto (- ((card I) + 1)) by SCMPDS_8:19 ;
A25: Comput ((P +* (stop (while>0 (a,i,I)))),(),(((LifeSpan ((P +* (stop I)),())) + 1) + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),((LifeSpan ((P +* (stop I)),())) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card I) + 1))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),((LifeSpan ((P +* (stop I)),())) + 1)))) by A24 ;
now :: thesis: for x being Int_position holds sm . x = (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),1)),(LifeSpan ((P +* (stop I)),())))) . x
let x be Int_position; :: thesis: sm . x = (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),1)),(LifeSpan ((P +* (stop I)),())))) . x
thus sm . x = (Comput ((P +* (stop (while>0 (a,i,I)))),(),((LifeSpan ((P +* (stop I)),())) + 1))) . x by
.= (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(),1)),(LifeSpan ((P +* (stop I)),())))) . x by EXTPRO_1:4 ; :: thesis: verum
end;
hence DataPart sm = DataPart (IExec (I,P,())) by ; :: thesis: Initialize sm = sm
IC (Comput ((P +* (stop (while>0 (a,i,I)))),(),(((LifeSpan ((P +* (stop I)),())) + 1) + 1))) = ICplusConst ((Comput ((P +* (stop (while>0 (a,i,I)))),(),((LifeSpan ((P +* (stop I)),())) + 1))),(0 - ((card I) + 1))) by
.= 0 by ;
hence Initialize sm = sm by ; :: thesis: verum