let s be State of SCMPDS; for P being Instruction-Sequence of SCMPDS
for I being Program of
for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
let P be Instruction-Sequence of SCMPDS; for I being Program of
for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
let I be Program of ; for J being shiftable Program of st I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P holds
( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
let J be shiftable Program of ; ( I is_closed_on s,P & I is_halting_on s,P & J is_closed_on IExec (I,P,(Initialize s)),P & J is_halting_on IExec (I,P,(Initialize s)),P implies ( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P ) )
set sE = IExec (I,P,(Initialize s));
assume that
A1:
I is_closed_on s,P
and
A2:
I is_halting_on s,P
and
A3:
J is_closed_on IExec (I,P,(Initialize s)),P
and
A4:
J is_halting_on IExec (I,P,(Initialize s)),P
; ( I ';' J is_closed_on s,P & I ';' J is_halting_on s,P )
set IJ = I ';' J;
set sIJ = stop (I ';' J);
set spI = stop I;
set ss = Initialize s;
set PP = P +* (stop (I ';' J));
set spJ = stop J;
set s1 = Initialize s;
set P1 = P +* (stop I);
set m1 = LifeSpan ((P +* (stop I)),(Initialize s));
set sm = Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set s3 = Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))));
set P3 = (P +* (stop I)) +* (stop J);
set m3 = LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))));
J is_halting_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I)
by A2, A3, A4, Th21;
then A5:
(P +* (stop I)) +* (stop J) halts_on Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))
by SCMPDS_6:def 3;
A6:
J is_closed_on Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))),P +* (stop I)
by A2, A3, A4, Th21;
then A7:
J is_closed_on Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))),(P +* (stop I)) +* (stop J)
by SCMPDS_6:24;
set s4 = Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))));
set P4 = P +* (stop (I ';' J));
A8:
stop J c= (P +* (stop I)) +* (stop J)
by FUNCT_4:25;
A9:
DataPart (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = DataPart (Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))))
by MEMSTR_0:45;
A10:
I ';' (J ';' (Stop SCMPDS)) = stop (I ';' J)
by AFINSQ_1:27;
A11:
Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))) = Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))
by A1, A2, Th17, A10;
stop (I ';' J) =
I ';' (J ';' (Stop SCMPDS))
by AFINSQ_1:27
.=
I +* (Shift ((stop J),(card I)))
;
then A12:
Shift ((stop J),(card I)) c= stop (I ';' J)
by FUNCT_4:25;
stop (I ';' J) c= P +* (stop (I ';' J))
by FUNCT_4:25;
then A13:
Shift ((stop J),(card I)) c= P +* (stop (I ';' J))
by A12, XBOOLE_1:1;
A14:
dom (stop I) c= dom (stop (I ';' J))
by SCMPDS_5:13;
now for k being Nat holds IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) in dom (stop (I ';' J))let k be
Nat;
IC (Comput ((P +* (stop (I ';' J))),(Initialize s),b1)) in dom (stop (I ';' J))per cases
( k <= LifeSpan ((P +* (stop I)),(Initialize s)) or k > LifeSpan ((P +* (stop I)),(Initialize s)) )
;
suppose A15:
k > LifeSpan (
(P +* (stop I)),
(Initialize s))
;
IC (Comput ((P +* (stop (I ';' J))),(Initialize s),b1)) in dom (stop (I ';' J))A16:
IC (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) in dom (stop I)
by A1, A2, Th4, Th19;
hereby verum
per cases
( IC (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I or CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS )
by A1, A2, Th4, Th20;
suppose A17:
IC (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
;
IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) in dom (stop (I ';' J))consider ii being
Nat such that A18:
k = (LifeSpan ((P +* (stop I)),(Initialize s))) + ii
by A15, NAT_1:10;
reconsider ii =
ii as
Nat ;
reconsider nn =
IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),ii)) as
Nat ;
(IC (Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),ii))) + (card I) = IC (Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))),ii))
by A8, A11, A9, A7, A13, A17, SCMPDS_6:31;
then A19:
IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) = nn + (card I)
by A18, EXTPRO_1:4;
nn in dom (stop J)
by A6, SCMPDS_6:def 2;
then
nn < card (stop J)
by AFINSQ_1:66;
then
nn < (card J) + 1
by COMPOS_1:55;
then A20:
(card I) + nn < (card I) + ((card J) + 1)
by XREAL_1:6;
card (stop (I ';' J)) =
(card (I ';' J)) + 1
by COMPOS_1:55
.=
((card I) + (card J)) + 1
by AFINSQ_1:17
;
hence
IC (Comput ((P +* (stop (I ';' J))),(Initialize s),k)) in dom (stop (I ';' J))
by A20, A19, AFINSQ_1:66;
verum end; end;
end; end; end; end;
hence
I ';' J is_closed_on s,P
by SCMPDS_6:def 2; I ';' J is_halting_on s,P
A21:
Comput ((P +* (stop (I ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))) = Comput ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))
by EXTPRO_1:4;
per cases
( CurInstr ((P +* (stop (I ';' J))),(Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))) = halt SCMPDS or IC (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I )
by A1, A2, Th4, Th20;
suppose
IC (Comput ((P +* (stop (I ';' J))),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s))))) = card I
;
I ';' J is_halting_on s,Pthen CurInstr (
(P +* (stop (I ';' J))),
(Comput ((P +* (stop (I ';' J))),(Initialize s),((LifeSpan ((P +* (stop I)),(Initialize s))) + (LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))))) =
CurInstr (
((P +* (stop I)) +* (stop J)),
(Comput (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))),(LifeSpan (((P +* (stop I)) +* (stop J)),(Initialize (Comput ((P +* (stop I)),(Initialize s),(LifeSpan ((P +* (stop I)),(Initialize s)))))))))))
by A21, A8, A11, A9, A7, A13, SCMPDS_6:31
.=
halt SCMPDS
by A5, EXTPRO_1:def 15
;
then
P +* (stop (I ';' J)) halts_on Initialize s
by EXTPRO_1:29;
hence
I ';' J is_halting_on s,
P
by SCMPDS_6:def 3;
verum end; end;