let s be State of SCM+FSA; for I being Program of SCM+FSA st I is_closed_onInit s & I is_halting_onInit s holds
for m being Element of NAT st m <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m), Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m) equal_outside NAT
let I be Program of SCM+FSA; ( I is_closed_onInit s & I is_halting_onInit s implies for m being Element of NAT st m <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m), Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m) equal_outside NAT )
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (loop I));
assume A1:
I is_closed_onInit s
; ( not I is_halting_onInit s or for m being Element of NAT st m <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m), Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m) equal_outside NAT )
defpred S1[ Nat] means ( $1 <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) implies Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),$1), Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),$1) equal_outside NAT );
assume
I is_halting_onInit s
; for m being Element of NAT st m <= LifeSpan ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I))) holds
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m), Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m) equal_outside NAT
then A2:
ProgramPart (s +* (Initialized I)) halts_on s +* (Initialized I)
by Def5;
A3:
for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be
Element of
NAT ;
( S1[m] implies S1[m + 1] )
assume A4:
(
m <= LifeSpan (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I))) implies
Comput (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)),
m),
Comput (
(ProgramPart (s +* (Initialized (loop I)))),
(s +* (Initialized (loop I))),
m)
equal_outside NAT )
;
S1[m + 1]
A5:
IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)) in dom I
by A1, Def4;
then A6:
IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)) in dom (loop I)
by FUNCT_4:105;
T:
ProgramPart (s +* (Initialized I)) = ProgramPart (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m))
by AMI_1:123;
Y:
(ProgramPart (s +* (Initialized I))) /. (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m))) = (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)))
by T, COMPOS_1:38;
I c= Comput (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)),
m)
by Th67, AMI_1:81;
then A7:
CurInstr (
(ProgramPart (s +* (Initialized I))),
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)))
= I . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)))
by A5, Y, GRFUNC_1:8;
S:
ProgramPart (s +* (Initialized (loop I))) = ProgramPart (Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m))
by AMI_1:123;
A8:
Comput (
(ProgramPart (s +* (Initialized (loop I)))),
(s +* (Initialized (loop I))),
(m + 1)) =
Following (
(ProgramPart (s +* (Initialized (loop I)))),
(Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)))
by EXTPRO_1:4
.=
Exec (
(CurInstr ((ProgramPart (s +* (Initialized (loop I)))),(Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)))),
(Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)))
;
A9:
loop I c= Comput (
(ProgramPart (s +* (Initialized (loop I)))),
(s +* (Initialized (loop I))),
m)
by Th67, AMI_1:81;
A10:
Comput (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)),
(m + 1)) =
Following (
(ProgramPart (s +* (Initialized I))),
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)))
by EXTPRO_1:4
.=
Exec (
(CurInstr ((ProgramPart (s +* (Initialized I))),(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)))),
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)))
;
assume A11:
m + 1
<= LifeSpan (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)))
;
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),(m + 1)), Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),(m + 1)) equal_outside NAT
then
m < LifeSpan (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)))
by NAT_1:13;
then
I . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m))) <> halt SCM+FSA
by A2, A7, EXTPRO_1:def 14;
then A12:
I . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m))) = (loop I) . (IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)))
by FUNCT_4:111;
Z:
(ProgramPart (s +* (Initialized (loop I)))) /. (IC (Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m))) = (Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)) . (IC (Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)))
by S, COMPOS_1:38;
IC (Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)) = IC (Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m))
by A4, A11, COMPOS_1:24, NAT_1:13;
then
CurInstr (
(ProgramPart (s +* (Initialized I))),
(Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),m)))
= CurInstr (
(ProgramPart (s +* (Initialized (loop I)))),
(Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),m)))
by A9, A6, A7, Z, A12, GRFUNC_1:8;
hence
Comput (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)),
(m + 1)),
Comput (
(ProgramPart (s +* (Initialized (loop I)))),
(s +* (Initialized (loop I))),
(m + 1))
equal_outside NAT
by A4, A11, A10, A8, NAT_1:13, SCMFSA6A:32;
verum
end;
A13:
S1[ 0 ]
proof
assume
0 <= LifeSpan (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)))
;
Comput ((ProgramPart (s +* (Initialized I))),(s +* (Initialized I)),0), Comput ((ProgramPart (s +* (Initialized (loop I)))),(s +* (Initialized (loop I))),0) equal_outside NAT
(
s +* I,
s equal_outside NAT &
s,
s +* (loop I) equal_outside NAT )
by FUNCT_7:28, FUNCT_7:132;
then
s +* I,
s +* (loop I) equal_outside NAT
by FUNCT_7:29;
then
(s +* I) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))),
(s +* (loop I)) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) equal_outside NAT
by FUNCT_7:106;
then
s +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))),
(s +* (loop I)) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA))) equal_outside NAT
by FUNCT_4:15;
then
s +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))),
s +* ((loop I) +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))) equal_outside NAT
by FUNCT_4:15;
then
s +* (I +* (((intloc 0) .--> 1) +* (Start-At (0,SCM+FSA)))),
s +* (Initialized (loop I)) equal_outside NAT
by FUNCT_4:15;
then
s +* (Initialized I),
s +* (Initialized (loop I)) equal_outside NAT
by FUNCT_4:15;
then
s +* (Initialized I),
Comput (
(ProgramPart (s +* (Initialized (loop I)))),
(s +* (Initialized (loop I))),
0)
equal_outside NAT
by EXTPRO_1:3;
hence
Comput (
(ProgramPart (s +* (Initialized I))),
(s +* (Initialized I)),
0),
Comput (
(ProgramPart (s +* (Initialized (loop I)))),
(s +* (Initialized (loop I))),
0)
equal_outside NAT
by EXTPRO_1:3;
verum
end;
thus
for m being Element of NAT holds S1[m]
from NAT_1:sch 1(A13, A3); verum