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 = Initialize (stop (while>0 a,i,I));
set IsI = Initialize (stop I);
set i1 = a,i <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
set s2 = (Initialize s) +* (stop I);
set s3 = (Initialize s) +* (stop (while>0 a,i,I));
set s4 = Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1;
I1: (Initialize s) +* (stop (while>0 a,i,I)) = s +* (Initialize (stop (while>0 a,i,I))) by SCMPDS_4:5;
I2: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by SCMPDS_4:5;
assume that
A1: card I > 0 and
A2: I is_closed_on s and
A3: I is_halting_on s and
A4: s . (DataLoc (s . a),i) > 0 and
A5: m = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 2 and
A6: sm = Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),m ; :: thesis:
A7: Initialize (stop I) c= (Initialize s) +* (stop I) by I2, FUNCT_4:26;
A8: Initialize (stop (while>0 a,i,I)) c= (Initialize s) +* (stop (while>0 a,i,I)) by I1, FUNCT_4:26;
while>0 a,i,I c= Initialize (stop (while>0 a,i,I)) by SCMPDS_6:17;
then A9: while>0 a,i,I c= (Initialize s) +* (stop (while>0 a,i,I)) by A8, XBOOLE_1:1;
Shift I,1 c= while>0 a,i,I by Lm3;
then Shift I,1 c= (Initialize s) +* (stop (while>0 a,i,I)) by A9, XBOOLE_1:1;
then A10: Shift I,1 c= Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1 by AMI_1:81;
B11: while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by Lm2;
A12: Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),(0 + 1) = Following (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),0 ) by AMI_1:14
.= Following (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))) by AMI_1:13
.= Exec (a,i <=0_goto ((card I) + 2)),((Initialize s) +* (stop (while>0 a,i,I))) by B11, I1, SCMPDS_6:22 ;
set m2 = LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I));
set s5 = Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
set l1 = (card I) + 1;
A13: IC ((Initialize s) +* (stop (while>0 a,i,I))) = 0 by SCMPDS_6:21;
A14: ((Initialize s) +* (stop (while>0 a,i,I))) . (DataLoc (((Initialize s) +* (stop (while>0 a,i,I))) . a),i) = ((Initialize s) +* (stop (while>0 a,i,I))) . (DataLoc (s . a),i) by SCMPDS_5:19
.= s . (DataLoc (s . a),i) by SCMPDS_5:19 ;
set m3 = (LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1;
set s6 = Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1);
ProgramPart ((Initialize s) +* (stop (while>0 a,i,I))) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1) by AMI_1:123;
then A15: Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) = Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by AMI_1:51;
set s7 = Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1);
(card I) + 1 < (card I) + 2 by XREAL_1:8;
then A16: (card I) + 1 in dom (while>0 a,i,I) by SCMPDS_8:18;
A17: dom (ProgramPart s) = NAT by COMPOS_1:34;
A18: I is_closed_on (Initialize s) +* (stop I) by A2, SCMPDS_6:38;
A19: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (while>0 a,i,I))) by FUNCT_7:134, SCMPDS_4:24;

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

end;

then A20: DataPart ((Initialize s) +* (stop I)) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1) by SCMPDS_4:23;
A21: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A3, SCMPDS_6:def 3;
I5: ((Initialize s) +* (stop I)) +* (Initialize (stop I)) = (Initialize ((Initialize s) +* (stop I))) +* (stop I) by SCMPDS_4:5;
(Initialize s) +* (stop I) = (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A7, I5, FUNCT_4:79;
then ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop I)) halts_on (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A3, SCMPDS_6:def 3;
then A22: I is_halting_on (Initialize s) +* (stop I) by SCMPDS_6:def 3;
A23: IC (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1) = (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1) . (IC SCMPDS )
.= succ 0 by A4, A13, A12, A14, SCMPDS_2:68
.= 0 + 1 ;
then DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) by A1, A7, A22, A18, A20, A10, SCMPDS_7:36;
then A24: DataPart (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by A21, AMI_1:122
.= DataPart ((Result (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) +* (s | NAT )) by A17, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= DataPart (IExec I,s) by SCMPDS_4:def 8 ;
A25: IC (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = (card I) + 1 by A1, A7, A22, A18, A23, A20, A10, SCMPDS_7:36;
then A26: CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1))),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) = (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . ((card I) + 1) by A15, COMPOS_1:38
.= (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1) . ((card I) + 1) by AMI_1:54
.= ((Initialize s) +* (stop (while>0 a,i,I))) . ((card I) + 1) by AMI_1:54
.= (while>0 a,i,I) . ((card I) + 1) by A16, A9, GRFUNC_1:8
.= goto (- ((card I) + 1)) by SCMPDS_8:19 ;
A27: Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1) = Following (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by AMI_1:14
.= Exec (goto (- ((card I) + 1))),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) by A26, AMI_1:123 ;

let x be Int_position ; :: thesis:
s: ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1) = ProgramPart ((Initialize s) +* (stop (while>0 a,i,I))) by AMI_1:123;
thus sm . x = (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)) . x by A5, A6, A27, SCMPDS_2:66
.= (Comput (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1)),(Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),1),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) . x by s, AMI_1:51 ; :: thesis:

end;

hence DataPart sm = DataPart (IExec I,s) by A24, SCMPDS_4:23; :: thesis:
IC (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) = (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),(((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1) + 1)) . (IC SCMPDS )
.= ICplusConst (Comput (ProgramPart ((Initialize s) +* (stop (while>0 a,i,I)))),((Initialize s) +* (stop (while>0 a,i,I))),((LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) + 1)),(0 - ((card I) + 1)) by A27, SCMPDS_2:66
.= 0 by A25, A15, SCMPDS_7:1 ;
hence (Initialize sm) +* (stop (while>0 a,i,I)) = sm by A5, A6, SCMPDS_7:37; :: thesis: