let s, sm be State of SCMPDS ; :: thesis:
let I be shiftable No-StopCode 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 = Initialized (stop (while>0 a,i,I));
set IsI = Initialized (stop I);
set i1 = a,i <=0_goto ((card I) + 2);
set i2 = goto (- ((card I) + 1));
set s2 = s +* (Initialized (stop I));
set s3 = s +* (Initialized (stop (while>0 a,i,I)));
set s4 = Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1;
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 (s +* (Initialized (stop I)))) + 2 and
A6: sm = Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),m ; :: thesis:
A7: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
A8: Initialized (stop (while>0 a,i,I)) c= s +* (Initialized (stop (while>0 a,i,I))) by FUNCT_4:26;
while>0 a,i,I c= Initialized (stop (while>0 a,i,I)) by SCMPDS_6:17;
then A9: while>0 a,i,I c= s +* (Initialized (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= s +* (Initialized (stop (while>0 a,i,I))) by A9, XBOOLE_1:1;
then A10: Shift I,1 c= Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1 by AMI_1:81;
while>0 a,i,I = (a,i <=0_goto ((card I) + 2)) ';' (I ';' (goto (- ((card I) + 1)))) by Lm2;
then A11: CurInstr (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))) = a,i <=0_goto ((card I) + 2) by SCMPDS_6:22;
A12: Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),(0 + 1) = Following (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),0 ) by AMI_1:14
.= Following (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))) by AMI_1:13
.= Exec (a,i <=0_goto ((card I) + 2)),(s +* (Initialized (stop (while>0 a,i,I)))) by A11, AMI_1:def 18 ;
set m2 = LifeSpan (s +* (Initialized (stop I)));
set s5 = Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))));
set l1 = (card I) + 1;
A13: IC (s +* (Initialized (stop (while>0 a,i,I)))) = 0 by SCMPDS_6:21;
A14: (s +* (Initialized (stop (while>0 a,i,I)))) . (DataLoc ((s +* (Initialized (stop (while>0 a,i,I)))) . a),i) = (s +* (Initialized (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 (s +* (Initialized (stop I)))) + 1;
set s6 = Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1);
ProgramPart (s +* (Initialized (stop (while>0 a,i,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1) by AMI_1:144;
then A15: Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1) = Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:51;
set s7 = Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),(((LifeSpan (s +* (Initialized (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 (s | NAT ) = NAT by SCMPDS_6:1;
A18: I is_closed_on s +* (Initialized (stop I)) by A2, SCMPDS_6:38;
A19: DataPart (s +* (Initialized (stop I))) = DataPart (s +* (Initialized (stop (while>0 a,i,I)))) by SCMPDS_4:24, SCMPDS_4:36;

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

end;

then A20: DataPart (s +* (Initialized (stop I))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1) by SCMPDS_4:23;
A21: ProgramPart (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I)) by A3, SCMPDS_6:def 3;
s +* (Initialized (stop I)) = (s +* (Initialized (stop I))) +* (Initialized (stop I)) by A7, FUNCT_4:79;
then ProgramPart ((s +* (Initialized (stop I))) +* (Initialized (stop I))) halts_on (s +* (Initialized (stop I))) +* (Initialized (stop I)) by A21;
then A22: I is_halting_on s +* (Initialized (stop I)) by SCMPDS_6:def 3;
A23: IC (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1) = (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1) . (IC SCMPDS ) by AMI_1:def 15
.= succ 0 by A4, A13, A12, A14, SCMPDS_2:68
.= 0 + 1 ;
then DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) by A1, A7, A22, A18, A20, A10, SCMPDS_7:36;
then A24: DataPart (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Result (s +* (Initialized (stop I)))) by A21, AMI_1:122
.= DataPart ((Result (s +* (Initialized (stop I)))) +* (s | NAT )) by A17, AMI_2:29, FUNCT_4:76, SCMPDS_2:100
.= DataPart (IExec I,s) by SCMPDS_4:def 8 ;
Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) /. (IC (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) = (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . (IC (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) by AMI_1:150;
A25: IC (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) = (card I) + 1 by A1, A7, A22, A18, A23, A20, A10, SCMPDS_7:36;
then A26: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = (Comput (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1)),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1),(LifeSpan (s +* (Initialized (stop I))))) . ((card I) + 1) by A15, AMI_1:def 16, Y
.= (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),1) . ((card I) + 1) by AMI_1:54
.= (s +* (Initialized (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 ;
T: ProgramPart (s +* (Initialized (stop (while>0 a,i,I)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:144;
A27: Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),(((LifeSpan (s +* (Initialized (stop I)))) + 1) + 1) = Following (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by AMI_1:14
.= Exec (goto (- ((card I) + 1))),(Comput (ProgramPart (s +* (Initialized (stop (while>0 a,i,I))))),(s +* (Initialized (stop (while>0 a,i,I)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by A26, AMI_1:def 18, T ;

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

end;

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