let I be No-StopCode Program of SCMPDS ; :: thesis: for J being Program of SCMPDS
for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
( IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = ((card I) + (card J)) + 1 & DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )
let J be Program of SCMPDS ; :: thesis: for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
( IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = ((card I) + (card J)) + 1 & DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )
let s be State of SCMPDS ; :: thesis: ( I is_closed_on s & I is_halting_on s implies ( IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = ((card I) + (card J)) + 1 & DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 ) )
assume A1: I is_closed_on s ; :: thesis: ( not I is_halting_on s or ( IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = ((card I) + (card J)) + 1 & DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 ) )
set G1 = Goto ((card J) + 1);
set SS = Stop SCMPDS ;
set J2 = ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS );
set IJ = (I ';' (Goto ((card J) + 1))) ';' J;
set pJ = stop ((I ';' (Goto ((card J) + 1))) ';' J);
set IsJ = Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J));
set s1 = s +* (Initialized (stop I));
set s2 = s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)));
assume A2: I is_halting_on s ; :: thesis: ( IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = ((card I) + (card J)) + 1 & DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )
set sm = Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))));
A3: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by SCMPDS_4:46;
then A4: IC (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) by A1, A2, Th39;
then A5: IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I by A1, A2, Th43;
A6: 0 in dom (Goto ((card J) + 1)) by Th33;
A7: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . 0 = ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS ))) . 0 by SCMPDS_4:46
.= (Goto ((card J) + 1)) . 0 by A6, SCMPDS_4:37
.= goto ((card J) + 1) by Th33 ;
stop ((I ';' (Goto ((card J) + 1))) ';' J) c= Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:9;
then A8: dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) c= dom (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by GRFUNC_1:8;
card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by SCMPDS_4:45
.= 1 + (card J) by SCMPDS_5:6 ;
then A9: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . ((card J) + 1) = (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (0 + (card ((Goto ((card J) + 1)) ';' J)))
.= halt SCMPDS by SCMPDS_4:38, JJ, KK ;
A10: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) = card ((Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS ))) by SCMPDS_4:46
.= (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS ))) by SCMPDS_4:45
.= 1 + (card (J ';' (Stop SCMPDS ))) by SCMPDS_5:6 ;
then A11: 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by SCMPDS_4:1;
A12: stop ((I ';' (Goto ((card J) + 1))) ';' J) = ((I ';' (Goto ((card J) + 1))) ';' J) ';' (Stop SCMPDS ) by SCMPDS_4:def 7
.= (I ';' ((Goto ((card J) + 1)) ';' J)) ';' (Stop SCMPDS ) by SCMPDS_4:46
.= I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by SCMPDS_4:46 ;
then A13: card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) by SCMPDS_4:45;
then (card I) + 0 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by A10, XREAL_1:8;
then A14: card I in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:1;
X: card (Stop SCMPDS ) = 1 by SCMNORM:3;
A15: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) = 1 + ((card J) + (card (Stop SCMPDS ))) by A10, SCMPDS_4:45
.= (card J) + (1 + (card (Stop SCMPDS ))) ;
then (card J) + 1 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by X, XREAL_1:8;
then A16: (card J) + 1 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by SCMPDS_4:1;
card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) = (((card I) + (card J)) + 1) + 1 by A13, A15, X;
then ((card I) + (card J)) + 1 < card (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by NAT_1:13;
then A17: ((card I) + (card J)) + 1 in dom (stop ((I ';' (Goto ((card J) + 1))) ';' J)) by SCMPDS_4:1;
Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))) /. (IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))) = (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) . (IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))) by AMI_1:150;
A18: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) . (card I) by A1, A2, A4, Th43, Y
.= (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) . (card I) by AMI_1:54
.= (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . (card I) by A8, A14, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . (0 + (card I)) by A12, A14, SCMPDS_4:33
.= goto ((card J) + 1) by A11, A7, SCMPDS_4:38 ;

A19: now

let a be Int_position ; :: thesis: (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . a = (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) . a
T: ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) by AMI_1:144;
thus (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . a = (Following (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))) . a by AMI_1:14
.= (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) . a by A18, SCMPDS_2:66, T ; :: thesis: verum

end;

Y: (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) /. (IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) = (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) . (IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))) by AMI_1:150;
T: ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) by AMI_1:144;
thus IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = IC (Following (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I)))))) by AMI_1:14
.= ICplusConst (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))),((card J) + 1) by A18, SCMPDS_2:66, T
.= (card I) + ((card J) + 1) by A5, Th23
.= ((card I) + (card J)) + 1 ; :: thesis: ( DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) & ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )
then A20: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1))),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) . (((card I) + (card J)) + 1) by AMI_1:54, Y
.= (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) . (((card I) + (card J)) + 1) by A8, A17, FUNCT_4:14
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . ((card I) + ((card J) + 1)) by A12, A17, SCMPDS_4:33
.= halt SCMPDS by A16, A9, SCMPDS_4:38 ;
DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) by A1, A2, A3, Th39;
hence DataPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = DataPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) by A19, SCMPDS_4:23; :: thesis: ( ( for k being Element of NAT st k <= LifeSpan (s +* (Initialized (stop I))) holds
CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS ) & IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )

hereby :: thesis: ( IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I & ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )

let k be Element of NAT ; :: thesis: ( k <= LifeSpan (s +* (Initialized (stop I))) implies CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),b₁)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),b₁) <> halt SCMPDS )
assume A22: k <= LifeSpan (s +* (Initialized (stop I))) ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),b₁)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),b₁) <> halt SCMPDS

per cases ( k < LifeSpan (s +* (Initialized (stop I))) or LifeSpan (s +* (Initialized (stop I))) <= k ) ;

suppose A23: k < LifeSpan (s +* (Initialized (stop I))) ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),b₁)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),b₁) <> halt SCMPDS

then CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k)),(Comput (ProgramPart (s +* (Initialized (stop I)))),(s +* (Initialized (stop I))),k) <> halt SCMPDS by A1, A2, Th42;
hence CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS by A1, A2, A3, A23, Th41; :: thesis: verum

end;

suppose LifeSpan (s +* (Initialized (stop I))) <= k ; :: thesis: CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),b₁)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),b₁) <> halt SCMPDS

then k = LifeSpan (s +* (Initialized (stop I))) by A22, XXREAL_0:1;
hence CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) <> halt SCMPDS by A18, SCMPDS_2:85; :: thesis: verum

end;

end;

end;

thus IC (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),(LifeSpan (s +* (Initialized (stop I))))) = card I by A1, A2, A4, Th43; :: thesis: ( ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) & LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 )
thus A24: ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) halts_on s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))) by A20, AMI_1:146; :: thesis: LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1

now

let k be Element of NAT ; :: thesis: ( CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) = halt SCMPDS implies (LifeSpan (s +* (Initialized (stop I)))) + 1 <= k )
assume CurInstr (ProgramPart (Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k)),(Comput (ProgramPart (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J))))),(s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))),k) = halt SCMPDS ; :: thesis: (LifeSpan (s +* (Initialized (stop I)))) + 1 <= k
then LifeSpan (s +* (Initialized (stop I))) < k by A21;
hence (LifeSpan (s +* (Initialized (stop I)))) + 1 <= k by INT_1:20; :: thesis: verum

end;

hence LifeSpan (s +* (Initialized (stop ((I ';' (Goto ((card J) + 1))) ';' J)))) = (LifeSpan (s +* (Initialized (stop I)))) + 1 by A20, A24, AMI_1:def 46; :: thesis: verum