let s be State of SCM+FSA ; :: thesis: for I being paraclosed Program of SCM+FSA st s +* (I +* (Start-At (insloc 0 ))) is halting holds
for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
Computation (s +* (I +* (Start-At (insloc 0 )))),k, Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k equal_outside NAT
set SA0 = Start-At (insloc 0 );
let I be paraclosed Program of SCM+FSA ; :: thesis: ( s +* (I +* (Start-At (insloc 0 ))) is halting implies for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
Computation (s +* (I +* (Start-At (insloc 0 )))),k, Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k equal_outside NAT )
assume A1:
s +* (I +* (Start-At (insloc 0 ))) is halting
; :: thesis: for J being Program of SCM+FSA
for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
Computation (s +* (I +* (Start-At (insloc 0 )))),k, Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k equal_outside NAT
let J be Program of SCM+FSA ; :: thesis: for k being Element of NAT st k <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) holds
Computation (s +* (I +* (Start-At (insloc 0 )))),k, Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),k equal_outside NAT
set s1 = s +* (I +* (Start-At (insloc 0 )));
A2:
I +* (Start-At (insloc 0 )) c= s +* (I +* (Start-At (insloc 0 )))
by FUNCT_4:26;
set s2 = s +* ((I ';' J) +* (Start-At (insloc 0 )));
A3:
(I ';' J) +* (Start-At (insloc 0 )) c= s +* ((I ';' J) +* (Start-At (insloc 0 )))
by FUNCT_4:26;
A4: s +* (I +* (Start-At (insloc 0 ))) =
(s +* I) +* (Start-At (insloc 0 ))
by FUNCT_4:15
.=
(s +* (Start-At (insloc 0 ))) +* I
by Th14
;
A5: s +* ((I ';' J) +* (Start-At (insloc 0 ))) =
(s +* (I ';' J)) +* (Start-At (insloc 0 ))
by FUNCT_4:15
.=
(s +* (Start-At (insloc 0 ))) +* (I ';' J)
by Th14
;
A6:
(s +* (Start-At (insloc 0 ))) +* I,s +* (Start-At (insloc 0 )) equal_outside NAT
by AMI_1:120, FUNCT_7:28;
defpred S1[ Element of NAT ] means ( $1 <= LifeSpan (s +* (I +* (Start-At (insloc 0 )))) implies Computation (s +* (I +* (Start-At (insloc 0 )))),$1, Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),$1 equal_outside NAT );
A7:
s +* (Start-At (insloc 0 )),(s +* (Start-At (insloc 0 ))) +* (I ';' J) equal_outside NAT
by AMI_1:120;
( Computation (s +* (I +* (Start-At (insloc 0 )))),0 = s +* (I +* (Start-At (insloc 0 ))) & Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),0 = s +* ((I ';' J) +* (Start-At (insloc 0 ))) )
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 +* (I +* (Start-At (insloc 0 )))) implies
Computation (s +* (I +* (Start-At (insloc 0 )))),
m,
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
m equal_outside NAT )
;
:: thesis: S1[m + 1]
assume A11:
m + 1
<= LifeSpan (s +* (I +* (Start-At (insloc 0 ))))
;
:: thesis: Computation (s +* (I +* (Start-At (insloc 0 )))),(m + 1), Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),(m + 1) equal_outside NAT
then A12:
m < LifeSpan (s +* (I +* (Start-At (insloc 0 ))))
by NAT_1:13;
A13:
Computation (s +* (I +* (Start-At (insloc 0 )))),
(m + 1) =
Following (Computation (s +* (I +* (Start-At (insloc 0 )))),m)
by AMI_1:14
.=
Exec (CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m)),
(Computation (s +* (I +* (Start-At (insloc 0 )))),m)
;
A14:
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(m + 1) =
Following (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),m)
by AMI_1:14
.=
Exec (CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),m)),
(Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),m)
;
A15:
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m) = IC (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),m)
by A10, A11, AMI_1:121, NAT_1:13;
A16:
IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m) in dom I
by A2, Def2;
dom I misses dom (Start-At (insloc 0 ))
by SF_MASTR:64;
then
I c= I +* (Start-At (insloc 0 ))
by FUNCT_4:33;
then
I c= s +* (I +* (Start-At (insloc 0 )))
by A2, XBOOLE_1:1;
then A17:
I c= Computation (s +* (I +* (Start-At (insloc 0 )))),
m
by AMI_1:81;
dom (I ';' J) misses dom (Start-At (insloc 0 ))
by SF_MASTR:64;
then
I ';' J c= (I ';' J) +* (Start-At (insloc 0 ))
by FUNCT_4:33;
then
I ';' J c= s +* ((I ';' J) +* (Start-At (insloc 0 )))
by A3, XBOOLE_1:1;
then A18:
I ';' J c= Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
m
by 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 +* (I +* (Start-At (insloc 0 )))),m) = I . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m))
by A16, A17, GRFUNC_1:8;
then
I . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m)) <> halt SCM+FSA
by A1, A12, AMI_1:def 46;
then CurInstr (Computation (s +* (I +* (Start-At (insloc 0 )))),m) =
(I ';' J) . (IC (Computation (s +* (I +* (Start-At (insloc 0 )))),m))
by A16, A20, SCMFSA6A:54
.=
CurInstr (Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),m)
by A15, A16, A18, A19, GRFUNC_1:8
;
hence
Computation (s +* (I +* (Start-At (insloc 0 )))),
(m + 1),
Computation (s +* ((I ';' J) +* (Start-At (insloc 0 )))),
(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