let I, J be Program of SCMPDS ; 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 ; ( 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 SCMPDS_4:5;
I2:
s +* (Initialize (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) = (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
by SCMPDS_4:5;
A1:
(I ';' (Goto ((card J) + 1))) ';' J = I ';' ((Goto ((card J) + 1)) ';' J)
by SCMPDS_4:46;
I c= I ';' (Stop SCMPDS )
by SCMPDS_4:40;
then A2:
I c= stop I
;
( Initialize (stop I) c= (Initialize s) +* (stop I) & stop I c= Initialize (stop I) )
by I1, FUNCT_4:26, SCMPDS_4:9;
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
; ( 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, FUNCT_4:26, SCMPDS_4:9;
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 SCMPDS_4:46
;
then
I c= stop (I ';' ((Goto ((card J) + 1)) ';' J))
by SCMPDS_4:40;
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
; ( (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
;
( (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, AMI_1:def 46
.=
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, AMI_1:146;
hence
(I ';' (Goto ((card J) + 1))) ';' J is_halting_on s
by A1, Def3;
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on snow let k be
Element of
NAT ;
IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b1) 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))
;
IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b1) 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;
verum end; suppose A17:
k > 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)))),b1) 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, AMI_1:def 46;
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;
verum end; end; hence
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on s
by A1, Def2;
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
;
( (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 SCMPDS_4:46;
then A23:
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 LL, SCMPDS_4:45
;
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, SCMPDS_4:45
.=
(((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, SCMPDS_4:45;
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, SCMPDS_4:38
.=
(Goto ((card J) + 1)) . 0
by A22, A21, SCMPDS_4:37
.=
goto ((card J) + 1)
by Th33
;
card ((Goto ((card J) + 1)) ';' J) =
(card (Goto ((card J) + 1))) + (card J)
by SCMPDS_4:45
.=
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, SCMPDS_4:38
;
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 AMI_1:14
.=
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, SCMPDS_4:38
;
then A33:
ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) halts_on (Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
by AMI_1:146;
hence
(I ';' (Goto ((card J) + 1))) ';' J is_halting_on s
by A1, Def3;
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on snow let k be
Element of
NAT ;
IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b1) 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))
;
IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),((Initialize s) +* (stop (I ';' ((Goto ((card J) + 1)) ';' J)))),b1) 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;
verum end; suppose A35:
k > 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)))),b1) 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, AMI_1:def 46;
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;
verum end; end; hence
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on s
by A1, Def2;
verum end;