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 ;
A2:
s +* (Initialize (stop I)) = (Initialize s) +* (stop I)
by COMPOS_1:125;
A3:
(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 A4:
ProgramPart ((Initialize s) +* (stop I)) halts_on (Initialize s) +* (stop I)
by Def3;
A5:
( Initialize (stop I) = Initialize (stop I) & Initialize (stop I) c= (Initialize s) +* (stop I) )
by A2, FUNCT_4:26;
A6:
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 A7:
(
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]
A8:
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;
A9:
ProgramPart ((Initialize s) +* (stop I)) = ProgramPart (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m))
by AMI_1:123;
A10:
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 A9
;
A11:
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 A12:
dom I c= dom (I ';' (J ';' (Stop SCMPDS)))
by XBOOLE_1:7;
A13:
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;
A14:
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 A13
;
A15:
IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) in dom (stop I)
by A1, Def2;
A16:
(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;
A17:
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= Initialize (stop I)
by FUNCT_4:33;
then
stop I c= (Initialize s) +* (stop I)
by A5, XBOOLE_1:1;
then
stop I c= Comput (
(ProgramPart ((Initialize s) +* (stop I))),
((Initialize s) +* (stop I)),
m)
by AMI_1:81;
then A18:
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 A15, A16, A17, GRFUNC_1:8;
assume A19:
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 A4, A18, EXTPRO_1:def 14;
then A20:
IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)) in dom I
by A15, SCMPDS_5:3;
A21:
(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 A18, A17
.=
I . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)))
by A20, AFINSQ_1:def 4
.=
(stop (I ';' J)) . (IC (Comput ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)),m)))
by A20, A11, 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 A8, A20, A11, A12, 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 A7, A19, A21, 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 A7, A19, A10, A14, NAT_1:13, SCMPDS_4:15;
verum
end;
A22:
((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 A22, EXTPRO_1:3;
then A23:
S1[ 0 ]
by A3, A22, FUNCT_7:132;
A24:
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A23, A6);
A25: (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 A2, A22, 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 A24, 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 A25, A24, COMPOS_1:138; verum
set m = LifeSpan ((ProgramPart ((Initialize s) +* (stop I))),((Initialize s) +* (stop I)));