let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis:
let s, sm 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 m be Element of NAT ; :: thesis:
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)))),(Initialize s),1);
set P4 = P +* (stop (while>0 (a,i,I)));
assume that
A3: card I > 0 and
A4: I is_closed_on s,P and
A5: I is_halting_on s,P and
A6: s . (DataLoc ((s . a),i)) > 0 and
A7: m = (LifeSpan ((P +* (stop I)),(Initialize s))) + 2 and
A8: sm = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),m) ; :: thesis:
A9: stop I c= P +* (stop I) by FUNCT_4:26;
B9: Start-At (0,SCMPDS) c= Initialize s by FUNCT_4:26;
A10: stop (while>0 (a,i,I)) c= P +* (stop (while>0 (a,i,I))) by FUNCT_4:26;
while>0 (a,i,I) c= stop (while>0 (a,i,I)) by AFINSQ_1:78;
then A11: while>0 (a,i,I) c= P +* (stop (while>0 (a,i,I))) by A10, XBOOLE_1:1;
Shift (I,1) c= while>0 (a,i,I) by Lm3;
then Shift (I,1) c= P +* (stop (while>0 (a,i,I))) by A11, XBOOLE_1:1;
then A12: Shift (I,1) c= P +* (stop (while>0 (a,i,I))) ;
A13: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by Lm2;
A14: Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),(0 + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),0))) by EXTPRO_1:4
.= Following ((P +* (stop (while>0 (a,i,I)))),(Initialize s)) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 2)),(Initialize s)) by A13, SCMPDS_6:22 ;
set m2 = LifeSpan ((P +* (stop I)),(Initialize s));
set s5 = Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))));
set P5 = P +* (stop (while>0 (a,i,I)));
set l1 = (card I) + 1;
A15: IC (Initialize s) = 0 by COMPOS_1:def 16;
TT: not DataLoc ((s . a),i) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:59;
then A16: (Initialize s) . (DataLoc (((Initialize s) . a),i)) = (Initialize s) . (DataLoc ((s . a),i)) by FUNCT_4:12
.= s . (DataLoc ((s . a),i)) by TT, FUNCT_4:12 ;
set m3 = (LifeSpan ((P +* (stop I)),(Initialize s))) + 1;
set s6 = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1));
set P6 = P +* (stop (while>0 (a,i,I)));
A17: Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)) = Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s)))) by EXTPRO_1:5;
set s7 = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1));
(card I) + 1 < (card I) + 2 by XREAL_1:8;
then A18: (card I) + 1 in dom (while>0 (a,i,I)) by SCMPDS_8:18;
A19: dom (ProgramPart s) = NAT by COMPOS_1:34;
A20: I is_closed_on Initialize s,P +* (stop I) by A4, SCMPDS_6:38;

now

let x be Int_position ; :: thesis:
thus (Initialize s) . x = (Initialize s) . x
.= (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)) . x by A14, SCMPDS_2:68 ; :: thesis:

end;

now

let x be Int_position ; :: thesis:
thus sm . x = (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) . x by A7, A8, A30, SCMPDS_2:66
.= (Comput ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)),(LifeSpan ((P +* (stop I)),(Initialize s))))) . x by EXTPRO_1:5 ; :: thesis:

end;

hence DataPart sm = DataPart (IExec (I,P,s)) by A27, SCMPDS_4:23; :: thesis:
IC (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1))) = (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1))) . (IC )
.= ICplusConst ((Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))),(0 - ((card I) + 1))) by A30, SCMPDS_2:66
.= 0 by A28, A17, SCMPDS_7:1 ;
hence Initialize sm = sm by A7, A8, COMPOS_1:84; :: thesis: