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)))));
I1: s +* (Initialize (stop I)) = (Initialize s) +* (stop I) by COMPOS_1:125;
I2: s +* (Initialize (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) = (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by COMPOS_1:125;
A1: (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 A2: I c= stop I ;
( Initialize (stop I) c= (Initialize s) +* (stop I) & stop I c= Initialize (stop I) ) by I1, 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 A2, XBOOLE_1:1;
then A3: 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;
A4: 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 ;
A5: card (stop I) = (card I) + 1 by SCMPDS_5:7;
assume A6: 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 A5, AFINSQ_1:70;
then A7: 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 I2, COMPOS_1:126, FUNCT_4:26;
then A8: stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by XBOOLE_1:1;
A9: 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 A8, XBOOLE_1:1;
then A10: 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 A11: 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 A12: ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I) by Def3;
Y: (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;
Z: (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 A7, XXREAL_0:1;
then A13: 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;
TX1: 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;
TX2: 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;
A14: 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 A12, 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 A3, A13, Y, TX1, 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 A10, A13, 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 A6, A11, Th39, Z ;
then A15: ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) halts_on (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by TX2, EXTPRO_1:30;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s by A1, 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 A16: 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 A6, Def2;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A4;
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, A11, A16, Th39; :: thesis: verum

end;

suppose A17: 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)))));
A18: 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 A14, A15, TX2, 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 A15, A17, 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 A6, A11, A18, 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 A6, 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 A4; :: thesis: verum

end;

end;

end;

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

end;

suppose A19: 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 A20: 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 A6, A11, Th39;
A21: 0 in dom (Goto ((card J) + 1)) by Th33;
LL: card (Stop SCMPDS) = 1 by COMPOS_1:46;
A22: ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS) = (Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:30;
then A23: 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 LL, AFINSQ_1:20 ;
then A24: 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 A23, NAT_1:13;
then A25: (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 A9, A23, AFINSQ_1:20
.= (((card I) + (card J)) + 1) + 1 ;
then A26: ((card I) + (card J)) + 1 < card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by NAT_1:13;
then A27: ((card I) + (card J)) + 1 in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by AFINSQ_1:70;
Y: (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 A9, AFINSQ_1:20;
then (card I) + 0 < card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A23, XREAL_1:8;
then A28: card I in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by AFINSQ_1:70;
A29: 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 A6, A11, A19, Th39, Y
.= ((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 A9, A8, A28, GRFUNC_1:8
.= (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . 0 by A24, AFINSQ_1:def 4
.= (Goto ((card J) + 1)) . 0 by A22, A21, 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 A30: (((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 JJ, KK, AFINSQ_1:def 4 ;
Y: (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;
T: 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;
TX2: 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;
A31: 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 A29, T, SCMPDS_2:66
.= (card I) + ((card J) + 1) by A20, Th23
.= ((card I) + (card J)) + 1 ;
then A32: 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 Y, TX2, AMI_1:54
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . ((card I) + ((card J) + 1)) by A9, A8, A27, GRFUNC_1:8
.= halt SCMPDS by A25, A30, AFINSQ_1:def 4 ;
then A33: 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 A1, 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 A34: 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 A6, Def2;
then IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A4;
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, A11, A34, Th39; :: thesis: verum

end;

suppose A35: 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)))));
A36: 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 A32, A33, EXTPRO_1:def 14;
k >= (LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) + 1 by A35, 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 A33, A36, Th3, XXREAL_0:2
.= ((card I) + (card J)) + 1 by A31, A33, A36, 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 A26, AFINSQ_1:70; :: thesis: verum

end;

end;

end;

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

end;

end;