let P be Instruction-Sequence of SCMPDS; :: thesis:
let s, sm be State of SCMPDS; :: thesis:
let I be halt-free shiftable Program of ; :: thesis:
let a be Int_position; :: thesis:
let i be Integer; :: thesis:
let m be 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
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)),(Initialize s))) + 2 and
A5: sm = Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),m) ; :: thesis:
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 A7, XBOOLE_1:1;
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 A8, XBOOLE_1:1;
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)))),(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:3
.= Exec (((a,i) <=0_goto ((card I) + 2)),(Initialize s)) by A10, SCMPDS_6:11 ;
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;
A12: IC (Initialize s) = 0 by MEMSTR_0:def 11;
A13: not DataLoc ((s . a),i) in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
not a in dom (Start-At (0,SCMPDS)) by SCMPDS_4:18;
then A14: (Initialize s) . (DataLoc (((Initialize s) . a),i)) = (Initialize s) . (DataLoc ((s . a),i)) by FUNCT_4:11
.= s . (DataLoc ((s . a),i)) by A13, FUNCT_4:11 ;
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)));
A15: 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:4;
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: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 A1, SCMPDS_6:24;
for x being Int_position holds (Initialize s) . x = (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)) . x by A11, SCMPDS_2:56;
then A18: DataPart (Initialize s) = DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)) by SCMPDS_4:8;
A19: P +* (stop I) halts_on Initialize s by A2, SCMPDS_6:def 3;
(P +* (stop I)) +* (stop I) halts_on Initialize (Initialize s) by A2, SCMPDS_6:def 3;
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)))),(Initialize s),1)) = 0 + 1 by A3, A12, A11, A14, SCMPDS_2:56;
then DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (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 A6, A20, A17, A18, A9, SCMPDS_7:18;
then A22: DataPart (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))))) = DataPart (Result ((P +* (stop I)),(Initialize s))) by A19, EXTPRO_1:23
.= DataPart (IExec (I,P,(Initialize s))) by SCMPDS_4:def 5 ;
A23: IC (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))))) = (card I) + 1 by A6, A20, A17, A21, A18, A9, SCMPDS_7:18;
then A24: CurInstr ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) = (P +* (stop (while>0 (a,i,I)))) . ((card I) + 1) by A15, PBOOLE:143
.= (while>0 (a,i,I)) . ((card I) + 1) by A16, A8, GRFUNC_1:2
.= goto (- ((card I) + 1)) by SCMPDS_8:19 ;
A25: Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1)) = Following ((P +* (stop (while>0 (a,i,I)))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) by EXTPRO_1:3
.= Exec ((goto (- ((card I) + 1))),(Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) by A24 ;

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 A4, A5, A25, SCMPDS_2:54
.= (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:4 ; :: thesis:

end;

hence DataPart sm = DataPart (IExec (I,P,(Initialize s))) by A22, SCMPDS_4:8; :: thesis:
IC (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),(((LifeSpan ((P +* (stop I)),(Initialize s))) + 1) + 1))) = ICplusConst ((Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))),(0 - ((card I) + 1))) by A25, SCMPDS_2:54
.= 0 by A23, A15, SCMPDS_7:1 ;
hence Initialize sm = sm by A4, A5, MEMSTR_0:46; :: thesis: