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 ) )
assume A1: 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 ) )
assume A2: 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 )
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 IsJ = Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)));
set pI = stop I;
set IsI = Initialized (stop I);
set s1 = s +* (Initialized (stop I));
set s2 = s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))));
set m = LifeSpan (s +* (Initialized (stop I)));
set SS = Stop SCMPDS ;
set s3 = Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))));
set s4 = Computation (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;
A4: s +* (Initialized (stop I)) is halting by A2, Def3;
A5: IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) in dom (stop I) by A1, Def2;
reconsider n = IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) as Element of NAT by ORDINAL1:def 13;
card (stop I) = (card I) + 1 by SCMPDS_5:7;
then n < (card I) + 1 by A5, SCMPDS_4:1;
then A7: n <= card I by INT_1:20;
A8: 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 );
A9: 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 ;
A10: Initialized (stop I) c= s +* (Initialized (stop I)) by FUNCT_4:26;
stop I c= Initialized (stop I) by SCMPDS_4:9;
then A11: stop I c= s +* (Initialized (stop I)) by A10, XBOOLE_1:1;
I c= I ';' (Stop SCMPDS ) by SCMPDS_4:40;
then I c= stop I by SCMPDS_4:def 7;
then I c= s +* (Initialized (stop I)) by A11, XBOOLE_1:1;
then A12: I c= Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:81;
A13: Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))) c= s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) by FUNCT_4:26;
stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by SCMPDS_4:9;
then A14: stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) by A13, XBOOLE_1:1;
I c= stop (I ';' ((Goto ((card J) + 1)) ';' J)) by A9, SCMPDS_4:40;
then I c= s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) by A14, XBOOLE_1:1;
then A15: I c= Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I)))) by AMI_1:81;

per cases ( IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) <> inspos (card I) or IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) ) ;

suppose IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) <> inspos (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 A16: IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) in dom I by SCMPDS_4:1;
A17: halt SCMPDS = CurInstr (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) by A4, AMI_1:def 46
.= I . (IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) by A12, A16, GRFUNC_1:8
.= (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I))))) . (IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))) by A15, A16, GRFUNC_1:8
.= CurInstr (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I))))) by A1, A2, Th39 ;
then A18: s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) is halting by AMI_1:def 20;
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 (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),b₁) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set C1k = IC (Computation (s +* (Initialized (stop I))),k);
set C2k = IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k);

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

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

IC (Computation (s +* (Initialized (stop I))),k) in dom (stop I) by A1, Def2;
then IC (Computation (s +* (Initialized (stop I))),k) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A8;
hence IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A1, A2, A19, Th39; :: thesis: verum

end;

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

set m2 = LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))));
A21: LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) <= LifeSpan (s +* (Initialized (stop I))) by A17, A18, AMI_1:def 46;
then IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) = IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))))) by A18, A20, Th3, XXREAL_0:2
.= IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))))) by A1, A2, A21, Th39 ;
then IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) in dom (stop I) by A1, Def2;
hence IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A8; :: thesis: verum

end;

end;

end;

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

end;

suppose A22: IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) ; :: thesis: ( (I ';' (Goto ((card J) + 1))) ';' J is_halting_on s & (I ';' (Goto ((card J) + 1))) ';' J is_closed_on s )

then A23: IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I) by A1, A2, Th39;
A24: card ((Goto ((card J) + 1)) ';' J) = (card (Goto ((card J) + 1))) + (card J) by SCMPDS_4:45
.= 1 + (card J) by SCMPDS_5:6 ;
A25: card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) = (card I) + (card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) by A9, SCMPDS_4:45;
A26: ((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ) = (Goto ((card J) + 1)) ';' (J ';' (Stop SCMPDS )) by SCMPDS_4:46;
then A27: card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) = (card (Goto ((card J) + 1))) + (card (J ';' (Stop SCMPDS ))) by SCMPDS_4:45
.= 1 + (card (J ';' (Stop SCMPDS ))) by SCMPDS_5:6
.= ((card J) + 1) + 1 by SCMPDS_4:45, SCMPDS_4:74 ;
then (card I) + 0 < card (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A25, XREAL_1:8;
then A28: inspos (card I) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by SCMPDS_4:1;
A29: inspos 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by A27, SCMPDS_4:1;
A30: inspos 0 in dom (Goto ((card J) + 1)) by Th33;
A31: CurInstr (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I))))) = (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I))))) . (inspos (card I)) by A1, A2, A22, Th39
.= (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) . (inspos (card I)) by AMI_1:54
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . (inspos (0 + (card I))) by A9, A14, A28, GRFUNC_1:8
.= (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (inspos 0 ) by A29, SCMPDS_4:38
.= (Goto ((card J) + 1)) . (inspos 0 ) by A26, A30, SCMPDS_4:37
.= goto ((card J) + 1) by Th33 ;
(card J) + 1 < card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) by A27, NAT_1:13;
then A32: inspos ((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 A9, A27, SCMPDS_4:45
.= (((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: inspos (((card I) + (card J)) + 1) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by SCMPDS_4:1;
A35: (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (inspos ((card J) + 1)) = (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (inspos (0 + (card ((Goto ((card J) + 1)) ';' J)))) by A24
.= halt SCMPDS by SCMPDS_4:38, SCMPDS_4:73 ;
A36: IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = IC (Following (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I)))))) by AMI_1:14
.= ICplusConst (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I))))),((card J) + 1) by A31, SCMPDS_2:66
.= inspos ((card I) + ((card J) + 1)) by A23, Th23
.= inspos (((card I) + (card J)) + 1) ;
then A37: CurInstr (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((LifeSpan (s +* (Initialized (stop I)))) + 1)) = (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) . (inspos (((card I) + (card J)) + 1)) by AMI_1:54
.= (I ';' (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))) . (inspos ((card I) + ((card J) + 1))) by A9, A14, A34, GRFUNC_1:8
.= halt SCMPDS by A32, A35, SCMPDS_4:38 ;
then A38: s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) is halting by AMI_1:def 20;
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 (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),b₁) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
set C1k = IC (Computation (s +* (Initialized (stop I))),k);
set C2k = IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k);

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

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

IC (Computation (s +* (Initialized (stop I))),k) in dom (stop I) by A1, Def2;
then IC (Computation (s +* (Initialized (stop I))),k) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A8;
hence IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A1, A2, A39, Th39; :: thesis: verum

end;

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

then A40: k >= (LifeSpan (s +* (Initialized (stop I)))) + 1 by INT_1:20;
set m2 = LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))));
A41: LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) <= (LifeSpan (s +* (Initialized (stop I)))) + 1 by A37, A38, AMI_1:def 46;
then IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) = IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))))) by A38, A40, Th3, XXREAL_0:2
.= inspos (((card I) + (card J)) + 1) by A36, A38, A41, Th3 ;
hence IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J))) by A33, SCMPDS_4:1; :: thesis: verum

end;

end;

end;

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

end;

end;