let P be the Instructions of SCMPDS -valued ManySortedSet of NAT ; :: thesis: for I, J being Program of SCMPDS
for s being 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 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 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 s1 = Initialize s;
set s2 = Initialize s;
set P1 = P +* (stop I);
set P2 = P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)));
set m = LifeSpan ((P +* (stop I)),(Initialize s));
set SS = Stop SCMPDS;
set s3 = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set s4 = Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set P3 = P +* (stop I);
set P4 = P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)));
A3: (I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J) by AFINSQ_1:30;
XX: I c= stop I by AFINSQ_1:78;
stop I c= P +* (stop I) by FUNCT_4:26;
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:16;
set JS = ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS);
reconsider n = IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) as Element of NAT ;
A7: card (stop I) = (card I) + 1 by SCMPDS_5:7;
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)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) 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;
A10: stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by FUNCT_4:26;
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= 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 Initialize s by Def3;
A15: (P +* (stop I)) /. (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = (P +* (stop I)) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:158;
A16: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:158;

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

suppose IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize 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)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom I by AFINSQ_1:70;
A20: halt SCMPDS = CurInstr ((P +* (stop I)),(Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A14, EXTPRO_1:def 14
.= I . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A5, A17, A15, GRFUNC_1:8
.= (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A12, A17, GRFUNC_1:8
.= CurInstr ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by A8, A13, Th39, A16 ;
then A21: P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) halts_on Initialize s by EXTPRO_1:30;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P by A3, Def3; :: 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)))),(Initialize s),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set C1k = IC (Comput ((P +* (stop I)),(Initialize s),k));
set C2k = IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),k));

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

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

IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) by A8, Def2;
then IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A6;
hence IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize 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)),(Initialize s)) ; :: thesis: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))

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

end;

suppose A25: IC (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize 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)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = 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: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) by PBOOLE:158;
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 XREAL_1:8;
then A36: card I in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by AFINSQ_1:70;
A37: CurInstr ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize 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: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: (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) /. (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) = (P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) . (IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1)))) by PBOOLE:158;
A42: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + 1))) = IC (Following ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))) by EXTPRO_1:4
.= ICplusConst ((Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))),((card J) + 1)) by A37, SCMPDS_2:66
.= (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)))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize 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:8
.= halt SCMPDS by A32, A38, AFINSQ_1:def 4 ;
then A44: P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))) halts_on Initialize s by EXTPRO_1:30;
hence (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s,P by A3, Def3; :: 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)))),(Initialize s),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set C1k = IC (Comput ((P +* (stop I)),(Initialize s),k));
set C2k = IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),k));

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

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

IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop I) by A8, Def2;
then IC (Comput ((P +* (stop I)),(Initialize s),k)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A6;
hence IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize 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)),(Initialize s)) ; :: thesis: IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),b₁)) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))

set m2 = LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s));
A47: LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s)) <= (LifeSpan ((P +* (stop I)),(Initialize s))) + 1 by A43, A44, EXTPRO_1:def 14;
k >= (LifeSpan ((P +* (stop I)),(Initialize s))) + 1 by A46, INT_1:20;
then IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),k)) = IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),(LifeSpan ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s))))) by A44, A47, Th3, XXREAL_0:2
.= ((card I) + (card J)) + 1 by A42, A44, A47, Th3 ;
hence IC (Comput ((P +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),(Initialize s),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,P by A3, Def2; :: thesis: verum

end;

end;