let I, J be Program of SCMPDS; :: thesis: for s being State of SCMPDS st I is_closed_on s & I is_halting_on s holds
( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s )
let s be State of SCMPDS; :: thesis: ( I is_closed_on s & I is_halting_on s implies ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s ) )
set G = Goto ((card J) + 1);
set IJ = (I ';' (Goto ((card J) + 1))) ';' J;
set J2 = I ';' ((Goto ((card J) + 1)) ';' J);
set pJ = stop (I ';' ((Goto ((card J) + 1)) ';' J));
set pI = stop I;
set s1 = (Initialize s) +* (stop I);
set s2 = (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)));
set m = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));
set SS = Stop SCMPDS;
set s3 = Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
set s4 = Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))));
A1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by COMPOS_1:125;
A2: s +* (Initialize (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) = (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by COMPOS_1:125;
A3: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by AFINSQ_1:30;
I c= I ';' (Stop SCMPDS) by AFINSQ_1:78;
then A4: I c= stop I ;
( Initialize (stop I) c= (Initialize s) +* (stop I) & stop I c= Initialize (stop I) ) by A1, COMPOS_1:126, FUNCT_4:26;
then stop I c= (Initialize s) +* (stop I) by XBOOLE_1:1;
then I c= (Initialize s) +* (stop I) by A4, XBOOLE_1:1;
then A5: I c= Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by AMI_1:81;
A6: dom (stop I) c= dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by SCMPDS_5:16;
set JS = ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS);
reconsider n = IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) as Element of NAT ;
A7: card (stop I) = (card I) + 1 by SCMPDS_5:7;
assume A8: I is_closed_on s ; :: thesis: ( not I is_halting_on s or ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s ) )
then IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in dom (stop I) by Def2;
then n < (card I) + 1 by A7, AFINSQ_1:70;
then A9: n <= card I by INT_1:20;
( Initialize (stop (I ';' ((Goto ((card J) + 1)) ';' J))) c= (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) & stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= Initialize (stop (I ';' ((Goto ((card J) + 1)) ';' J))) ) by A2, COMPOS_1:126, FUNCT_4:26;
then A10: stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by XBOOLE_1:1;
A11: stop (I ';' ((Goto ((card J) + 1)) ';' J)) = (I ';' ((Goto ((card J) + 1)) ';' J)) ';' (Stop SCMPDS)
.= I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:30 ;
then I c= stop (I ';' ((Goto ((card J) + 1)) ';' J)) by AFINSQ_1:78;
then I c= (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A10, XBOOLE_1:1;
then A12: I c= Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))) by AMI_1:81;
assume A13: I is_halting_on s ; :: thesis: ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s )
then A14: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by Def3;
A15: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by COMPOS_1:38;
A16: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by COMPOS_1:38;

per cases ( IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) <> card I or IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I ) ;

suppose IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) <> card I ; :: thesis: ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s )

then n < card I by A9, XXREAL_0:1;
then A17: IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) in dom I by AFINSQ_1:70;
A18: ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) by AMI_1:123;
A19: ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) by AMI_1:123;
A20: halt SCMPDS = CurInstr ((ProgramPart ((Initialize s) +* (stop I))),(Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by A14, EXTPRO_1:def 14
.= I . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by A5, A17, A15, A18, GRFUNC_1:8
.= (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by A12, A17, GRFUNC_1:8
.= CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by A8, A13, Th39, A16 ;
then A21: ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) halts_on (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A19, EXTPRO_1:30;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s by A3, Def3; :: thesis: (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s

now

let k be Element of NAT ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set C1k = IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k));
set C2k = IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k));

per cases ( k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) or k > LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ) ;

suppose A22: k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))

IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop I) by A8, Def2;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A6;
hence IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A8, A13, A22, Th39; :: thesis: verum

end;

suppose A23: k > LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))

set m2 = LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))));
A24: LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) by A20, A21, A19, EXTPRO_1:def 14;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k)) = IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))))))) by A21, A23, Th3, XXREAL_0:2
.= IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))))))) by A8, A13, A24, Th39 ;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k)) in dom (stop I) by A8, Def2;
hence IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A6; :: thesis: verum

end;

end;

end;

hence (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s by A3, Def2; :: thesis: verum

end;

suppose A25: IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I ; :: thesis: ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s )

then A26: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) = card I by A8, A13, Th39;
A27: 0 in dom (Goto ((card J) + 1)) by Th33;
A28: card (Stop SCMPDS) = 1 by COMPOS_1:46;
A29: ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS) = (Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30;
then A30: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS))) by AFINSQ_1:20
.= 1 + (card (J ';' (Stop SCMPDS))) by SCMPDS_5:6
.= ((card J) + 1) + 1 by A28, AFINSQ_1:20 ;
then A31: 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:70;
(card J) + 1 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by A30, NAT_1:13;
then A32: (card J) + 1 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:70;
card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) = (card I) + ((card J) + (1 + 1)) by A11, A30, AFINSQ_1:20
.= (((card I) + (card J)) + 1) + 1 ;
then A33: ((card I) + (card J)) + 1 < card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by NAT_1:13;
then A34: ((card I) + (card J)) + 1 in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by AFINSQ_1:70;
A35: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) by COMPOS_1:38;
card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) by A11, AFINSQ_1:20;
then (card I) + 0 < card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A30, XREAL_1:8;
then A36: card I in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by AFINSQ_1:70;
A37: CurInstr ((ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))))) = (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) . (card I) by A8, A13, A25, Th39, A35
.= ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (card I) by AMI_1:54
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . (0 + (card I)) by A11, A10, A36, GRFUNC_1:8
.= (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . 0 by A31, AFINSQ_1:def 4
.= (Goto ((card J) + 1)) . 0 by A29, A27, AFINSQ_1:def 4
.= goto ((card J) + 1) by Th33 ;
card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by AFINSQ_1:20
.= 1 + (card J) by SCMPDS_5:6 ;
then A38: (((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 Lm1, Lm2, AFINSQ_1:def 4 ;
A39: (ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) /. (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) = (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) by COMPOS_1:38;
A40: ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))) by AMI_1:123;
A41: ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))) by AMI_1:123;
A42: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1))) = IC (Following ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))))) by EXTPRO_1:4
.= ICplusConst ((Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))))),((card J) + 1)) by A37, A40, SCMPDS_2:66
.= (card I) + ((card J) + 1) by A26, Th23
.= ((card I) + (card J)) + 1 ;
then A43: CurInstr ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),((LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1)))) = ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (((card I) + (card J)) + 1) by A39, A41, AMI_1:54
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . ((card I) + ((card J) + 1)) by A11, A10, A34, GRFUNC_1:8
.= halt SCMPDS by A32, A38, AFINSQ_1:def 4 ;
then A44: ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) halts_on (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by EXTPRO_1:30;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s by A3, Def3; :: thesis: (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s

now

let k be Element of NAT ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set C1k = IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k));
set C2k = IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k));

per cases ( k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) or k > LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ) ;

suppose A45: k <= LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))

IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop I) by A8, Def2;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A6;
hence IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A8, A13, A45, Th39; :: thesis: verum

end;

suppose A46: k > LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))) ; :: thesis: IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))

set m2 = LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))));
A47: LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) <= (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1 by A43, A44, EXTPRO_1:def 14;
k >= (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1 by A46, INT_1:20;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k)) = IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(LifeSpan ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))))))) by A44, A47, Th3, XXREAL_0:2
.= ((card I) + (card J)) + 1 by A42, A44, A47, Th3 ;
hence IC (Comput ((ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A33, AFINSQ_1:70; :: thesis: verum

end;

end;

end;

hence (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s by A3, Def2; :: thesis: verum

end;

end;