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 COMPOS_1:125;
A2:
(Initialize ((Initialize s) +* (stop I))) +* (stop (I ';' J)) = ((Initialize s) +* (stop I)) +* (stop (I ';' J))
by COMPOS_1:78;
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 EXTPRO_1:4
.=
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 AFINSQ_1:30
;
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 EXTPRO_1:4
.=
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 COMPOS_1:130;
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, EXTPRO_1:def 14;
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, AFINSQ_1:def 4
.=
(stop (I ';' J)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)))
by A15, A9, AFINSQ_1:def 4
.=
(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 COMPOS_1:125;
( 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, EXTPRO_1:3;
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)) =
((Initialize (Initialize s)) +* (stop I)) +* (stop (I ';' J))
by COMPOS_1:83
.=
(Initialize s) +* ((stop I) +* (stop (I ';' J)))
by I1, I2, FUNCT_4:15
.=
(Initialize s) +* (stop (I ';' J))
by SCMPDS_5:17
.=
(Initialize s) +* (stop (I ';' J))
by COMPOS_1:125
;
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, COMPOS_1:138; verum
set m = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));