let P be Instruction-Sequence of SCMPDS; :: thesis: for I, J being Program of SCMPDS
for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )
let I, J be Program of SCMPDS; :: thesis: for s being 0 -started State of SCMPDS st I is_closed_on s,P & I is_halting_on s,P holds
( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )
let s be 0 -started State of SCMPDS; :: thesis: ( I is_closed_on s,P & I is_halting_on s,P implies ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P ) )
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 P1 = P +* (stop I);
set P2 = P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)));
set m = LifeSpan ((P +* (stop I)),s);
set SS = Stop SCMPDS;
set s3 = Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)));
set s4 = Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s)));
set P3 = P +* (stop I);
set P4 = P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)));
I: Initialize s = s by MEMSTR_0:44;
A3: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by AFINSQ_1:27;
XX: I c= stop I by AFINSQ_1:74;
stop I c= P +* (stop I) by FUNCT_4:25;
then A5: I c= P +* (stop I) by XX, XBOOLE_1:1;
A6: dom (stop I) c= dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by SCMPDS_5:13;
set JS = ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS);
reconsider n = IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) as Element of NAT ;
A7: card (stop I) = (card I) + 1 by COMPOS_1:55;
assume A8: I is_closed_on s,P ; :: thesis: ( not I is_halting_on s,P or ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P ) )
then IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) in dom (stop I) by Def2, I;
then n < (card I) + 1 by A7, AFINSQ_1:66;
then A9: n <= card I by INT_1:7;
A10: stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by FUNCT_4:25;
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:27 ;
then I c= stop (I ';' ((Goto ((card J) + 1)) ';' J)) by AFINSQ_1:74;
then I c= P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A10, XBOOLE_1:1;
then A12: I c= P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) ;
assume A13: I is_halting_on s,P ; :: thesis: ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P )
then A14: P +* (stop I) halts_on s by Def3, I;
A15: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143;
A16: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143;

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

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

then n < card I by A9, XXREAL_0:1;
then A17: IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s)))) in dom I by AFINSQ_1:66;
A20: halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A14, EXTPRO_1:def 15
.= I . (IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A5, A17, A15, GRFUNC_1:2
.= (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop I)),s))))) by A12, A17, GRFUNC_1:2
.= CurInstr ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) by A8, A13, Th39, A16 ;
then A21: P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) halts_on s by EXTPRO_1:29;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P by A3, Def3, I; :: thesis: (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P

now

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

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

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

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

end;

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

set m2 = LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s);
A24: LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s) <= LifeSpan ((P +* (stop I)),s) by A20, A21, EXTPRO_1:def 15;
then IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) = IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s)))) by A21, A23, EXTPRO_1:25, XXREAL_0:2
.= IC (Comput ((P +* (stop I)),s,(LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s)))) by A8, A13, A24, Th39 ;
then IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,k)) in dom (stop I) by A8, Def2, I;
hence IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,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,P by A3, Def2, I; :: thesis: verum

end;

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

then A26: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s)))) = card I by A8, A13, Th39;
A27: 0 in dom (Goto ((card J) + 1)) by Th33;
A28: card (Stop SCMPDS) = 1 by AFINSQ_1:33;
A29: ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS) = (Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS)) by AFINSQ_1:27;
then A30: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) = (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS))) by AFINSQ_1:17
.= 1 + (card (J ';' (Stop SCMPDS))) by COMPOS_1:54
.= ((card J) + 1) + 1 by A28, AFINSQ_1:17 ;
then A31: 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) by AFINSQ_1:66;
(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:66;
card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) = (card I) + ((card J) + (1 + 1)) by A11, A30, AFINSQ_1:17
.= (((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:66;
A35: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) by PBOOLE:143;
card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) by A11, AFINSQ_1:17;
then (card I) + 0 < card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by XREAL_1:6;
then A36: card I in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by AFINSQ_1:66;
A37: CurInstr ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s))))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (card I) by A8, A13, A25, Th39, A35
.= (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (card I)
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . (0 + (card I)) by A11, A10, A36, GRFUNC_1:2
.= (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS)) . 0 by A31, AFINSQ_1:def 3
.= (Goto ((card J) + 1)) . 0 by A29, A27, AFINSQ_1:def 3
.= goto ((card J) + 1) by Th33 ;
card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by AFINSQ_1:17
.= 1 + (card J) by COMPOS_1:54 ;
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 3 ;
A39: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) by PBOOLE:143;
A42: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,((LifeSpan ((P +* (stop I)),s)) + 1))) = IC (Following ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s)))))) by EXTPRO_1:3
.= ICplusConst ((Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,(LifeSpan ((P +* (stop I)),s)))),((card J) + 1)) by A37, SCMPDS_2:54
.= (card I) + ((card J) + 1) by A26, Th23
.= ((card I) + (card J)) + 1 ;
then A43: CurInstr ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),s,((LifeSpan ((P +* (stop I)),s)) + 1)))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (((card I) + (card J)) + 1) by A39
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS))) . ((card I) + ((card J) + 1)) by A11, A10, A34, GRFUNC_1:2
.= halt SCMPDS by A32, A38, AFINSQ_1:def 3 ;
then A44: P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) halts_on s by EXTPRO_1:29;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P by A3, Def3, I; :: thesis: (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s,P

now

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

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

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

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

end;

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

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

end;

end;

end;

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

end;

end;