let s be State of SCM+FSA ; :: thesis: for I being InitClosed Program of SCM+FSA st s +* (Initialized I) is halting holds
for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (I ';' J))),k equal_outside NAT
let I be InitClosed Program of SCM+FSA ; :: thesis: ( s +* (Initialized I) is halting implies for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (I ';' J))),k equal_outside NAT )
assume A1:
s +* (Initialized I) is halting
; :: thesis: for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (I ';' J))),k equal_outside NAT
let J be Program of SCM+FSA ; :: thesis: for k being Element of NAT st k <= LifeSpan (s +* (Initialized I)) holds
Computation (s +* (Initialized I)),k, Computation (s +* (Initialized (I ';' J))),k equal_outside NAT
set s1 = s +* (Initialized I);
set s2 = s +* (Initialized (I ';' J));
A2:
Initialized I c= s +* (Initialized I)
by FUNCT_4:26;
A3:
Initialized (I ';' J) c= s +* (Initialized (I ';' J))
by FUNCT_4:26;
A4: s +* (Initialized I) =
s +* (I +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))))
by FUNCT_4:15
.=
(s +* I) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))
by FUNCT_4:15
.=
(s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* I
by Th19
;
A5: s +* (Initialized (I ';' J)) =
s +* ((I ';' J) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))))
by FUNCT_4:15
.=
(s +* (I ';' J)) +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))
by FUNCT_4:15
.=
(s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* (I ';' J)
by Th19
;
defpred S1[ Element of NAT ] means ( $1 <= LifeSpan (s +* (Initialized I)) implies Computation (s +* (Initialized I)),$1, Computation (s +* (Initialized (I ';' J))),$1 equal_outside NAT );
A6:
(s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* I,s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))) equal_outside NAT
by AMI_1:120, FUNCT_7:28;
A7:
s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 ))),(s +* (((intloc 0 ) .--> 1) +* (Start-At (insloc 0 )))) +* (I ';' J) equal_outside NAT
by AMI_1:120;
( Computation (s +* (Initialized I)),0 = s +* (Initialized I) & Computation (s +* (Initialized (I ';' J))),0 = s +* (Initialized (I ';' J)) )
by AMI_1:13;
then A8:
S1[ 0 ]
by A4, A5, A6, A7, FUNCT_7:29;
A9:
for m being Element of NAT st S1[m] holds
S1[m + 1]
proof
let m be
Element of
NAT ;
:: thesis: ( S1[m] implies S1[m + 1] )
assume A10:
(
m <= LifeSpan (s +* (Initialized I)) implies
Computation (s +* (Initialized I)),
m,
Computation (s +* (Initialized (I ';' J))),
m equal_outside NAT )
;
:: thesis: S1[m + 1]
assume A11:
m + 1
<= LifeSpan (s +* (Initialized I))
;
:: thesis: Computation (s +* (Initialized I)),(m + 1), Computation (s +* (Initialized (I ';' J))),(m + 1) equal_outside NAT
then A12:
m < LifeSpan (s +* (Initialized I))
by NAT_1:13;
set sx =
s +* (Initialized (I ';' J));
A13:
Computation (s +* (Initialized I)),
(m + 1) =
Following (Computation (s +* (Initialized I)),m)
by AMI_1:14
.=
Exec (CurInstr (Computation (s +* (Initialized I)),m)),
(Computation (s +* (Initialized I)),m)
;
A14:
Computation (s +* (Initialized (I ';' J))),
(m + 1) =
Following (Computation (s +* (Initialized (I ';' J))),m)
by AMI_1:14
.=
Exec (CurInstr (Computation (s +* (Initialized (I ';' J))),m)),
(Computation (s +* (Initialized (I ';' J))),m)
;
A15:
IC (Computation (s +* (Initialized I)),m) = IC (Computation (s +* (Initialized (I ';' J))),m)
by A10, A11, AMI_1:121, NAT_1:13;
A16:
IC (Computation (s +* (Initialized I)),m) in dom I
by A2, Def1;
A17:
I c= Computation (s +* (Initialized I)),
m
by A2, Th13, AMI_1:81;
A18:
I ';' J c= Computation (s +* (Initialized (I ';' J))),
m
by A3, Th13, AMI_1:81;
dom (I ';' J) =
(dom (Directed I)) \/ (dom (ProgramPart (Relocated J,(card I))))
by FUNCT_4:def 1
.=
(dom I) \/ (dom (ProgramPart (Relocated J,(card I))))
by FUNCT_4:105
;
then A19:
dom I c= dom (I ';' J)
by XBOOLE_1:7;
A20:
CurInstr (Computation (s +* (Initialized I)),m) = I . (IC (Computation (s +* (Initialized I)),m))
by A16, A17, GRFUNC_1:8;
then
I . (IC (Computation (s +* (Initialized I)),m)) <> halt SCM+FSA
by A1, A12, AMI_1:def 46;
then CurInstr (Computation (s +* (Initialized I)),m) =
(I ';' J) . (IC (Computation (s +* (Initialized I)),m))
by A16, A20, SCMFSA6A:54
.=
CurInstr (Computation (s +* (Initialized (I ';' J))),m)
by A15, A16, A18, A19, GRFUNC_1:8
;
hence
Computation (s +* (Initialized I)),
(m + 1),
Computation (s +* (Initialized (I ';' J))),
(m + 1) equal_outside NAT
by A10, A11, A13, A14, NAT_1:13, SCMFSA6A:32;
:: thesis: verum
end;
thus
for k being Element of NAT holds S1[k]
from NAT_1:sch 1(A8, A9); :: thesis: verum