let I, J be Program of ; for s being State of 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 ; ( 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 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))));
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
by SCMPDS_4:def 7;
( Initialized (stop I) c= s +* (Initialized (stop I)) & stop I c= Initialized (stop I) )
by FUNCT_4:26, SCMPDS_4:9;
then
stop I c= s +* (Initialized (stop I))
by XBOOLE_1:1;
then
I c= s +* (Initialized (stop I))
by A2, XBOOLE_1:1;
then A3:
I c= Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (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 (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) as Element of NAT by ORDINAL1:def 13;
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 (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) in dom (stop I)
by Def2;
then
n < (card I) + 1
by A5, SCMPDS_4:1;
then A7:
n <= card I
by INT_1:20;
( Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))) c= s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))) & stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))) )
by FUNCT_4:26, SCMPDS_4:9;
then A8:
stop (I ';' ((Goto ((card J) + 1)) ';' J)) c= s +* (Initialized (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 )
by SCMPDS_4:def 7
.=
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= s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))
by A8, XBOOLE_1:1;
then A10:
I c= Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (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 (s +* (Initialized (stop I))) halts_on s +* (Initialized (stop I))
by Def3;
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)
;
( (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 (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) in dom I
by SCMPDS_4:1;
A14:
halt SCMPDS =
CurInstr (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I)))))
by A12, AMI_1:def 46
.=
I . (IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))))
by A3, A13, 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 A10, A13, GRFUNC_1:8
.=
CurInstr (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I)))))
by A6, A11, Th39
;
then A15:
ProgramPart (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) halts_on s +* (Initialized (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 (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),b1) 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 A17:
k > LifeSpan (s +* (Initialized (stop I)))
;
IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),b1) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))set m2 =
LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))));
A18:
LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) <= LifeSpan (s +* (Initialized (stop I)))
by A14, A15, 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 A15, A17, Th3, XXREAL_0:2
.=
IC (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))))))
by A6, A11, A18, Th39
;
then
IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) in dom (stop I)
by A6, Def2;
hence
IC (Computation (s +* (Initialized (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 (Computation (s +* (Initialized (stop I))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (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 (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),(LifeSpan (s +* (Initialized (stop I))))) = inspos (card I)
by A6, A11, Th39;
A21:
inspos 0 in dom (Goto ((card J) + 1))
by Th33;
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 SCMPDS_4:45, SCMPDS_4:74
;
then A24:
inspos 0 in dom (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))
by SCMPDS_4:1;
(card J) + 1
< card (((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS ))
by A23, NAT_1:13;
then A25:
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, 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:
inspos (((card I) + (card J)) + 1) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
by SCMPDS_4:1;
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:
inspos (card I) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
by SCMPDS_4:1;
A29:
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 A6, A11, A19, 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, A8, A28, GRFUNC_1:8
.=
(((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (inspos 0 )
by A24, SCMPDS_4:38
.=
(Goto ((card J) + 1)) . (inspos 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 )) . (inspos ((card J) + 1)) =
(((Goto ((card J) + 1)) ';' J) ';' (Stop SCMPDS )) . (inspos (0 + (card ((Goto ((card J) + 1)) ';' J))))
.=
halt SCMPDS
by SCMPDS_4:38, SCMPDS_4:73
;
A31:
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 A29, SCMPDS_2:66
.=
inspos ((card I) + ((card J) + 1))
by A20, Th23
.=
inspos (((card I) + (card J)) + 1)
;
then A32:
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, A8, A27, GRFUNC_1:8
.=
halt SCMPDS
by A25, A30, SCMPDS_4:38
;
then A33:
ProgramPart (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) halts_on s +* (Initialized (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 (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),b1) 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 A35:
k > LifeSpan (s +* (Initialized (stop I)))
;
IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),b1) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))set m2 =
LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J)))));
A36:
LifeSpan (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))) <= (LifeSpan (s +* (Initialized (stop I)))) + 1
by A32, A33, AMI_1:def 46;
k >= (LifeSpan (s +* (Initialized (stop I)))) + 1
by A35, INT_1:20;
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 A33, A36, Th3, XXREAL_0:2
.=
inspos (((card I) + (card J)) + 1)
by A31, A33, A36, Th3
;
hence
IC (Computation (s +* (Initialized (stop (I ';' ((Goto ((card J) + 1)) ';' J))))),k) in dom (stop (I ';' ((Goto ((card J) + 1)) ';' J)))
by A26, SCMPDS_4:1;
verum end; end; hence
(I ';' (Goto ((card J) + 1))) ';' J is_closed_on s
by A1, Def2;
verum end;