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);
I1: (Initialize s) +* (stop (while>0 (a,i,I))) = s +* (Initialize (stop (while>0 (a,i,I)))) by COMPOS_1:125;
I2: (Initialize s) +* (stop I) = s +* (Initialize (stop I)) by COMPOS_1:125;
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: ( DataPart sm = DataPart (IExec (I,s)) & (Initialize sm) +* (stop (while>0 (a,i,I))) = sm )
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 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 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 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 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 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 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: verum

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 COMPOS_1:125;
(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 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, EXTPRO_1:23
.= 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)) ;
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 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 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 A26, 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
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, EXTPRO_1:5 ; :: thesis: verum

end;

hence DataPart sm = DataPart (IExec (I,s)) by A24, 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 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: verum