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
( ( for k being Element of NAT st k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) ) & DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) )
let s be State of SCMPDS ; ( I is_closed_on s & I is_halting_on s implies ( ( for k being Element of NAT st k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) ) & DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) ) )
assume A1:
I is_closed_on s
; ( not I is_halting_on s or ( ( for k being Element of NAT st k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) ) & DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) ) )
set pI = stop I;
set pIJ = stop (I ';' J);
set s1 = (Initialize s) +* (stop I);
set IL = NAT ;
I1:
s +* (Initialize (stop I)) = (Initialize s) +* (stop I)
by SCMPDS_4:5;
A2:
(Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)) = ((Initialize s) +* (stop I)) +* (stop (I ';' J))
by I1, FUNCT_4:26, SCMPDS_4:34;
defpred S1[ Element of NAT ] means ( $1 <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) implies Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),$1, Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),$1 equal_outside NAT );
assume
I is_halting_on s
; ( ( for k being Element of NAT st k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k) ) & DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) )
then A3:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by Def3;
A4:
( Initialize (stop I) = (stop I) +* (Start-At 0 ,SCMPDS ) & Initialize (stop I) c= (Initialize s) +* (stop I) )
by I1, FUNCT_4:26;
A5:
for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
set JS =
J ';' (Stop SCMPDS );
set S1 =
(Initialize s) +* (stop I);
set S2 =
(Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J));
let m be
Element of
NAT ;
( S1[m] implies S1[m + 1] )
assume A6:
(
m <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I)) implies
Comput (ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I)),
m,
Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),
((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),
m equal_outside NAT )
;
S1[m + 1]
A7:
stop (I ';' J) c= Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),
((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),
m
by AMI_1:81, FUNCT_4:26;
T:
ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)
by AMI_1:123;
A8:
Comput (ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I)),
(m + 1) =
Following (ProgramPart ((Initialize s) +* (stop I))),
(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)),(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)),
(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)
by T
;
A9:
stop (I ';' J) =
(I ';' J) ';' (Stop SCMPDS )
.=
I ';' (J ';' (Stop SCMPDS ))
by SCMPDS_4:46
;
dom (I ';' (J ';' (Stop SCMPDS ))) =
dom (I +* (Shift (J ';' (Stop SCMPDS )),(card I)))
.=
(dom I) \/ (dom (Shift (J ';' (Stop SCMPDS )),(card I)))
by FUNCT_4:def 1
;
then A10:
dom I c= dom (I ';' (J ';' (Stop SCMPDS )))
by XBOOLE_1:7;
T:
ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))) = ProgramPart (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)
by AMI_1:123;
A11:
Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),
((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),
(m + 1) =
Following (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),
(Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)
by AMI_1:14
.=
Exec (CurInstr (ProgramPart (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)),(Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)),
(Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)
by T
;
A12:
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m) in dom (stop I)
by A1, Def2;
Y:
(ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) /. (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) = (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))
by COMPOS_1:38;
TX1:
ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)
by AMI_1:123;
dom (stop I) misses dom (Start-At 0 ,SCMPDS )
by SCMPDS_4:54;
then
stop I c= (stop I) +* (Start-At 0 ,SCMPDS )
by FUNCT_4:33;
then
stop I c= (Initialize s) +* (stop I)
by A4, XBOOLE_1:1;
then
stop I c= Comput (ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I)),
m
by AMI_1:81;
then A13:
CurInstr (ProgramPart ((Initialize s) +* (stop I))),
(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m) = (stop I) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))
by A12, Y, TX1, GRFUNC_1:8;
assume A14:
m + 1
<= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I))
;
Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(m + 1), Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),(m + 1) equal_outside NAT
then
m < LifeSpan (ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I))
by NAT_1:13;
then
(stop I) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) <> halt SCMPDS
by A3, A13, AMI_1:def 46;
then A15:
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m) in dom I
by A12, SCMPDS_5:3;
Y:
(ProgramPart (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)) /. (IC (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)) = (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m) . (IC (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m))
by COMPOS_1:38;
CurInstr (ProgramPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)),
(Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m) =
(I ';' (Stop SCMPDS )) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))
by A13, TX1
.=
I . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))
by A15, SCMPDS_4:37
.=
(stop (I ';' J)) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))
by A15, A9, SCMPDS_4:37
.=
(Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m) . (IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))
by A7, A15, A9, A10, GRFUNC_1:8
.=
CurInstr (ProgramPart (Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)),
(Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),m)
by A6, A14, Y, COMPOS_1:24, NAT_1:13
;
hence
Comput (ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I)),
(m + 1),
Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),
((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))),
(m + 1) equal_outside NAT
by A6, A14, A8, A11, NAT_1:13, SCMPDS_4:15;
verum
end;
I2:
((Initialize s) +* (stop I)) +* (Initialize (stop (I ';' J))) = (Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J))
by SCMPDS_4:5;
( Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),0 = (Initialize s) +* (stop I) & Comput (ProgramPart ((Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)))),(((Initialize s) +* (stop I)) +* (Initialize (stop (I ';' J)))),0 = (Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)) )
by I2, AMI_1:13;
then A16:
S1[ 0 ]
by A2, I2, FUNCT_7:132;
A17:
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A16, A5);
A18: (Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)) =
s +* ((Initialize (stop I)) +* (Initialize (stop (I ';' J))))
by I1, I2, FUNCT_4:15
.=
s +* (Initialize (stop (I ';' J)))
by SCMPDS_5:17
.=
(Initialize s) +* (stop (I ';' J))
by SCMPDS_4:5
;
hence
for k being Element of NAT st k <= LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)) holds
IC (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),k) = IC (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),k)
by A17, COMPOS_1:24; DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))
thus
DataPart (Comput (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)))) = DataPart (Comput (ProgramPart ((Initialize s) +* (stop (I ';' J)))),((Initialize s) +* (stop (I ';' J))),(LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I))))
by A18, A17, SCMPDS_4:24; verum
set m = LifeSpan (ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I));