let P be Instruction-Sequence of SCMPDS; :: 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
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:25;
A10: 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 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 A12: Shift (I,1) c= P +* (stop (while>0 (a,i,I))) by A11, XBOOLE_1:1;
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:3
.= Following ((P +* (stop (while>0 (a,i,I)))),(Initialize s)) by EXTPRO_1:2
.= Exec (((a,i) <=0_goto ((card I) + 2)),(Initialize s)) by A13, 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;
A15: IC (Initialize s) = 0 by MEMSTR_0:def 8;
TT: 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 A16: (Initialize s) . (DataLoc (((Initialize s) . a),i)) = (Initialize s) . (DataLoc ((s . a),i)) by FUNCT_4:11
.= s . (DataLoc ((s . a),i)) by TT, 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)));
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: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 A18: (card I) + 1 in dom (while>0 (a,i,I)) by SCMPDS_8:18;
A20: I is_closed_on Initialize s,P +* (stop I) by A4, 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 A14, SCMPDS_2:56;
then A22: DataPart (Initialize s) = DataPart (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)) by SCMPDS_4:8;
A23: P +* (stop I) halts_on Initialize s by A5, SCMPDS_6:def 3;
P +* (stop I) = (P +* (stop I)) +* (stop I) by FUNCT_4:25, FUNCT_4:98;
then (P +* (stop I)) +* (stop I) halts_on Initialize (Initialize s) by A5, SCMPDS_6:def 3;
then A25: I is_halting_on Initialize s,P +* (stop I) by SCMPDS_6:def 3;
A26: IC (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)) = (Comput ((P +* (stop (while>0 (a,i,I)))),(Initialize s),1)) . (IC )
.= succ 0 by A6, A15, A14, A16, SCMPDS_2:56
.= 0 + 1 ;
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 A9, A25, A20, A22, A12, SCMPDS_7:18;
then A27: 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 A23, EXTPRO_1:23
.= DataPart (Result ((P +* (stop I)),(Initialize s)))
.= DataPart (IExec (I,P,(Initialize s))) by SCMPDS_4:def 5 ;
A28: 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 A9, A25, A20, A26, A22, A12, SCMPDS_7:18;
then A29: 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 A17, PBOOLE:143
.= (P +* (stop (while>0 (a,i,I)))) . ((card I) + 1)
.= (P +* (stop (while>0 (a,i,I)))) . ((card I) + 1)
.= (while>0 (a,i,I)) . ((card I) + 1) by A18, A11, GRFUNC_1:2
.= goto (- ((card I) + 1)) by SCMPDS_8:19 ;
A30: 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 A29 ;

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: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 A27, SCMPDS_4:8; :: 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:54
.= 0 by A28, A17, SCMPDS_7:1 ;
hence Initialize sm = sm by A7, A8, MEMSTR_0:46; :: thesis: