let s, sm be State of SCMPDS; :: thesis: for I being halt-free shiftable Program of SCMPDS
for a being Int_position
for i being Integer
for m being Element of NAT st card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2 & sm = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),m) holds
( DataPart sm = DataPart (IExec (I,s)) & (Initialize sm) +* (stop (while>0 (a,i,I))) = sm )
let I be halt-free shiftable Program of SCMPDS; :: thesis: for a being Int_position
for i being Integer
for m being Element of NAT st card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2 & sm = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),m) holds
( DataPart sm = DataPart (IExec (I,s)) & (Initialize sm) +* (stop (while>0 (a,i,I))) = sm )
let a be Int_position ; :: thesis: for i being Integer
for m being Element of NAT st card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2 & sm = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),m) holds
( DataPart sm = DataPart (IExec (I,s)) & (Initialize sm) +* (stop (while>0 (a,i,I))) = sm )
let i be Integer; :: thesis: for m being Element of NAT st card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2 & sm = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),m) holds
( DataPart sm = DataPart (IExec (I,s)) & (Initialize sm) +* (stop (while>0 (a,i,I))) = sm )
let m be Element of NAT ; :: thesis: ( card I > 0 & I is_closed_on s & I is_halting_on s & s . (DataLoc ((s . a),i)) > 0 & m = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2 & sm = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),m) implies ( DataPart sm = DataPart (IExec (I,s)) & (Initialize sm) +* (stop (while>0 (a,i,I))) = sm ) )
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);
A1: (Initialize s) +* (stop (while>0 (a,i,I))) = s +* (Initialize (stop (while>0 (a,i,I)))) by COMPOS_1:125;
A2: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by COMPOS_1:125;
assume that
A3: card I > 0 and
A4: I is_closed_on s and
A5: I is_halting_on s and
A6: s . (DataLoc ((s . a),i)) > 0 and
A7: m = (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 2 and
A8: sm = Comput ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I)))),m) ; :: thesis: ( DataPart sm = DataPart (IExec (I,s)) & (Initialize sm) +* (stop (while>0 (a,i,I))) = sm )
A9: Initialize (stop I) c= (Initialize s) +* (stop I) by A2, FUNCT_4:26;
A10: Initialize (stop (while>0 (a,i,I))) c= (Initialize s) +* (stop (while>0 (a,i,I))) by A1, FUNCT_4:26;
while>0 (a,i,I) c= Initialize (stop (while>0 (a,i,I))) by SCMPDS_6:17;
then A11: while>0 (a,i,I) c= (Initialize s) +* (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= (Initialize s) +* (stop (while>0 (a,i,I))) by A11, XBOOLE_1:1;
then A12: 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;
A13: while>0 (a,i,I) = ((a,i) <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by Lm2;
A14: 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 EXTPRO_1:4
.= Following ((ProgramPart ((Initialize s) +* (stop (while>0 (a,i,I))))),((Initialize s) +* (stop (while>0 (a,i,I))))) by EXTPRO_1:3
.= Exec (((a,i) <=0_goto ((card I) + 2)),((Initialize s) +* (stop (while>0 (a,i,I))))) by A13, A1, 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;
A15: IC ((Initialize s) +* (stop (while>0 (a,i,I)))) = 0 by SCMPDS_6:21;
A16: ((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 A17: 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 EXTPRO_1:5;
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 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) +* (stop I) by A4, SCMPDS_6:38;
A21: DataPart ((Initialize s) +* (stop I)) = DataPart ((Initialize s) +* (stop (while>0 (a,i,I)))) by COMPOS_1:138, FUNCT_7:134;

now

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

end;

then A22: 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;
A23: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by A5, SCMPDS_6:def 3;
A24: ((Initialize s) +* (stop I)) +* (Initialize (stop I)) = (Initialize ((Initialize s) +* (stop I))) +* (stop I) by COMPOS_1:125;
(Initialize s) +* (stop I) = (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A9, A24, FUNCT_4:79;
then ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop I)) halts_on (Initialize ((Initialize s) +* (stop I))) +* (stop I) by A5, SCMPDS_6:def 3;
then A25: I is_halting_on (Initialize s) +* (stop I) by SCMPDS_6:def 3;
A26: 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 )
.= succ 0 by A6, A15, A14, A16, 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 A3, A9, A25, A20, A22, A12, SCMPDS_7:36;
then A27: 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 A23, EXTPRO_1:23
.= DataPart ((Result ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) +* (s | NAT)) by A19, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= DataPart (IExec (I,s)) ;
A28: 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 A3, A9, A25, A20, A26, A22, A12, SCMPDS_7:36;
then A29: 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 A17, 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 A18, A11, GRFUNC_1:8
.= goto (- ((card I) + 1)) by SCMPDS_8:19 ;
A30: 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 EXTPRO_1:4
.= 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 A29, AMI_1:123 ;

now

let x be Int_position ; :: thesis: sm . x = (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
A31: 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 A7, A8, A30, 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 A31, EXTPRO_1:5 ; :: thesis: verum

end;

hence DataPart sm = DataPart (IExec (I,s)) by A27, SCMPDS_4:23; :: thesis: (Initialize sm) +* (stop (while>0 (a,i,I))) = sm
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 )
.= 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 A30, SCMPDS_2:66
.= 0 by A28, A17, SCMPDS_7:1 ;
hence (Initialize sm) +* (stop (while>0 (a,i,I))) = sm by A7, A8, SCMPDS_7:37; :: thesis: verum